[mult_poly] down case folder, add dependency graphs

nasa · Jan 13, 2023 · fd2e9f3 · fd2e9f3
1 parent 1254e0e
commit fd2e9f3
Show file tree

Hide file tree

Showing 63 changed files with 613 additions and 1 deletion.
diff --git a/Mult_Poly/Mult_Poly.summary → mult_poly/Mult_Poly.summary b/Mult_Poly/Mult_Poly.summary → mult_poly/Mult_Poly.summary
diff --git a/Mult_Poly/PolySafe.summary → mult_poly/PolySafe.summary b/Mult_Poly/PolySafe.summary → mult_poly/PolySafe.summary
diff --git a/Mult_Poly/README.md → mult_poly/README.md b/Mult_Poly/README.md → mult_poly/README.md
@@ -1,7 +1,11 @@
 # Multivariate Polynomials
 
 This library contains a formalization of multivariate polynomials
-and semi-algebriac sets  For full descriptioon see: "Formal Verification of the  Interaction Between Semi-Algebraic Sets and Real Analytic Functions." 
+and semi-algebriac sets. For full descriptioon see: "Formal Verification of the  Interaction Between Semi-Algebraic Sets and Real Analytic Functions." 
+
+## External Dependencies
+
+![dependency graph](./mult_poly.svg "Dependency Graph")
 
 ## Internal Summary
 
@@ -25,6 +29,8 @@ and semi-algebriac sets  For full descriptioon see: "Formal Verification of the
   | [`smooth_not_analytic`](smooth_not_analytic.pvs)| This introduces a function that is smooth and not analytic, and shows that it does not interact with an SA set in a `nice' way, like real analytic functions do. |
   | [`poly_comp_analytic`](poly_comp_analytic.pvs)| The composition of a real analytic function with a multi-variate polynomial is still real analytic. Also shows the favorable properties of real analytic functions interacting with semi-algebraic sets. |
 
+![zoomed dependency graph](./mult_poly-zoomed.svg "Zoomed Dependency Graph")
+
 # Contributors
 * Lauren White, NASA, USA 
 * J Tanner Slagel, NASA, USA

diff --git a/Mult_Poly/analytic_def.prf → mult_poly/analytic_def.prf b/Mult_Poly/analytic_def.prf → mult_poly/analytic_def.prf
diff --git a/Mult_Poly/analytic_def.pvs → mult_poly/analytic_def.pvs b/Mult_Poly/analytic_def.pvs → mult_poly/analytic_def.pvs
diff --git a/Mult_Poly/arithmetic_MultPoly.prf → mult_poly/arithmetic_MultPoly.prf b/Mult_Poly/arithmetic_MultPoly.prf → mult_poly/arithmetic_MultPoly.prf
diff --git a/Mult_Poly/arithmetic_MultPoly.pvs → mult_poly/arithmetic_MultPoly.pvs b/Mult_Poly/arithmetic_MultPoly.pvs → mult_poly/arithmetic_MultPoly.pvs
diff --git a/Mult_Poly/arithmetic_poly.prf → mult_poly/arithmetic_poly.prf b/Mult_Poly/arithmetic_poly.prf → mult_poly/arithmetic_poly.prf
diff --git a/Mult_Poly/arithmetic_poly.pvs → mult_poly/arithmetic_poly.pvs b/Mult_Poly/arithmetic_poly.pvs → mult_poly/arithmetic_poly.pvs
diff --git a/Mult_Poly/continuous_ball_props.prf → mult_poly/continuous_ball_props.prf b/Mult_Poly/continuous_ball_props.prf → mult_poly/continuous_ball_props.prf
diff --git a/Mult_Poly/continuous_ball_props.pvs → mult_poly/continuous_ball_props.pvs b/Mult_Poly/continuous_ball_props.pvs → mult_poly/continuous_ball_props.pvs
diff --git a/Mult_Poly/derivatives_subtype.prf → mult_poly/derivatives_subtype.prf b/Mult_Poly/derivatives_subtype.prf → mult_poly/derivatives_subtype.prf
diff --git a/Mult_Poly/dimension_induction.prf → mult_poly/dimension_induction.prf b/Mult_Poly/dimension_induction.prf → mult_poly/dimension_induction.prf
diff --git a/Mult_Poly/dimension_induction.pvs → mult_poly/dimension_induction.pvs b/Mult_Poly/dimension_induction.pvs → mult_poly/dimension_induction.pvs
diff --git a/Mult_Poly/e_lims.pvs → mult_poly/e_lims.pvs b/Mult_Poly/e_lims.pvs → mult_poly/e_lims.pvs
diff --git a/Mult_Poly/eval_MultPoly.prf → mult_poly/eval_MultPoly.prf b/Mult_Poly/eval_MultPoly.prf → mult_poly/eval_MultPoly.prf
diff --git a/Mult_Poly/eval_MultPoly.pvs → mult_poly/eval_MultPoly.pvs b/Mult_Poly/eval_MultPoly.pvs → mult_poly/eval_MultPoly.pvs
diff --git a/Mult_Poly/eval_poly.prf → mult_poly/eval_poly.prf b/Mult_Poly/eval_poly.prf → mult_poly/eval_poly.prf
diff --git a/Mult_Poly/eval_poly.pvs → mult_poly/eval_poly.pvs b/Mult_Poly/eval_poly.pvs → mult_poly/eval_poly.pvs
diff --git a/Mult_Poly/eval_properties.prf → mult_poly/eval_properties.prf b/Mult_Poly/eval_properties.prf → mult_poly/eval_properties.prf
diff --git a/Mult_Poly/eval_properties.pvs → mult_poly/eval_properties.pvs b/Mult_Poly/eval_properties.pvs → mult_poly/eval_properties.pvs
diff --git a/Mult_Poly/list_lemmas.prf → mult_poly/list_lemmas.prf b/Mult_Poly/list_lemmas.prf → mult_poly/list_lemmas.prf
diff --git a/Mult_Poly/list_lemmas.pvs → mult_poly/list_lemmas.pvs b/Mult_Poly/list_lemmas.pvs → mult_poly/list_lemmas.pvs
diff --git a/Mult_Poly/map_perm.prf → mult_poly/map_perm.prf b/Mult_Poly/map_perm.prf → mult_poly/map_perm.prf
diff --git a/Mult_Poly/map_perm.pvs → mult_poly/map_perm.pvs b/Mult_Poly/map_perm.pvs → mult_poly/map_perm.pvs
diff --git a/mult_poly/mult_poly-zoomed.svg b/mult_poly/mult_poly-zoomed.svg
diff --git a/mult_poly/mult_poly.svg b/mult_poly/mult_poly.svg
diff --git a/Mult_Poly/mult_poly_ex.prf → mult_poly/mult_poly_ex.prf b/Mult_Poly/mult_poly_ex.prf → mult_poly/mult_poly_ex.prf
diff --git a/Mult_Poly/mult_poly_ex.pvs → mult_poly/mult_poly_ex.pvs b/Mult_Poly/mult_poly_ex.pvs → mult_poly/mult_poly_ex.pvs
diff --git a/Mult_Poly/mv_poly_more.pvs → mult_poly/mv_poly_more.pvs b/Mult_Poly/mv_poly_more.pvs → mult_poly/mv_poly_more.pvs
diff --git a/Mult_Poly/nth_derivative_props.prf → mult_poly/nth_derivative_props.prf b/Mult_Poly/nth_derivative_props.prf → mult_poly/nth_derivative_props.prf
diff --git a/Mult_Poly/nth_derivative_props.pvs → mult_poly/nth_derivative_props.pvs b/Mult_Poly/nth_derivative_props.pvs → mult_poly/nth_derivative_props.pvs
diff --git a/Mult_Poly/nth_derivative_subtype.prf → mult_poly/nth_derivative_subtype.prf b/Mult_Poly/nth_derivative_subtype.prf → mult_poly/nth_derivative_subtype.prf
diff --git a/Mult_Poly/nth_derivative_subtype.pvs → mult_poly/nth_derivative_subtype.pvs b/Mult_Poly/nth_derivative_subtype.pvs → mult_poly/nth_derivative_subtype.pvs
diff --git a/Mult_Poly/perm_props.prf → mult_poly/perm_props.prf b/Mult_Poly/perm_props.prf → mult_poly/perm_props.prf
diff --git a/Mult_Poly/perm_props.pvs → mult_poly/perm_props.pvs b/Mult_Poly/perm_props.pvs → mult_poly/perm_props.pvs
diff --git a/Mult_Poly/poly_comp_analytic.prf → mult_poly/poly_comp_analytic.prf b/Mult_Poly/poly_comp_analytic.prf → mult_poly/poly_comp_analytic.prf
diff --git a/Mult_Poly/poly_comp_analytic.pvs → mult_poly/poly_comp_analytic.pvs b/Mult_Poly/poly_comp_analytic.pvs → mult_poly/poly_comp_analytic.pvs
diff --git a/Mult_Poly/polyplus_props.prf → mult_poly/polyplus_props.prf b/Mult_Poly/polyplus_props.prf → mult_poly/polyplus_props.prf
diff --git a/Mult_Poly/polyplus_props.pvs → mult_poly/polyplus_props.pvs b/Mult_Poly/polyplus_props.pvs → mult_poly/polyplus_props.pvs
diff --git a/Mult_Poly/pvsbin/top.dep → mult_poly/pvsbin/top.dep b/Mult_Poly/pvsbin/top.dep → mult_poly/pvsbin/top.dep
diff --git a/Mult_Poly/semi_algebraic.prf → mult_poly/semi_algebraic.prf b/Mult_Poly/semi_algebraic.prf → mult_poly/semi_algebraic.prf
diff --git a/Mult_Poly/semi_algebraic.pvs → mult_poly/semi_algebraic.pvs b/Mult_Poly/semi_algebraic.pvs → mult_poly/semi_algebraic.pvs
diff --git a/Mult_Poly/semi_algebraic.summary → mult_poly/semi_algebraic.summary b/Mult_Poly/semi_algebraic.summary → mult_poly/semi_algebraic.summary
diff --git a/...Poly/semi_algebraic_non_standard_form.prf → ...poly/semi_algebraic_non_standard_form.prf b/...Poly/semi_algebraic_non_standard_form.prf → ...poly/semi_algebraic_non_standard_form.prf
diff --git a/...Poly/semi_algebraic_non_standard_form.pvs → ...poly/semi_algebraic_non_standard_form.pvs b/...Poly/semi_algebraic_non_standard_form.pvs → ...poly/semi_algebraic_non_standard_form.pvs
diff --git a/Mult_Poly/simplified.prlite → mult_poly/simplified.prlite b/Mult_Poly/simplified.prlite → mult_poly/simplified.prlite
diff --git a/Mult_Poly/smooth_not_analytic.prf → mult_poly/smooth_not_analytic.prf b/Mult_Poly/smooth_not_analytic.prf → mult_poly/smooth_not_analytic.prf
diff --git a/Mult_Poly/smooth_not_analytic.pvs → mult_poly/smooth_not_analytic.pvs b/Mult_Poly/smooth_not_analytic.pvs → mult_poly/smooth_not_analytic.pvs
diff --git a/Mult_Poly/sorted_list_ops.prf → mult_poly/sorted_list_ops.prf b/Mult_Poly/sorted_list_ops.prf → mult_poly/sorted_list_ops.prf
diff --git a/Mult_Poly/sorted_list_ops.pvs → mult_poly/sorted_list_ops.pvs b/Mult_Poly/sorted_list_ops.pvs → mult_poly/sorted_list_ops.pvs
diff --git a/Mult_Poly/standard_form_example.pvs → mult_poly/standard_form_example.pvs b/Mult_Poly/standard_form_example.pvs → mult_poly/standard_form_example.pvs
diff --git a/Mult_Poly/standard_form_extras.prf → mult_poly/standard_form_extras.prf b/Mult_Poly/standard_form_extras.prf → mult_poly/standard_form_extras.prf
diff --git a/Mult_Poly/standard_form_extras.pvs → mult_poly/standard_form_extras.pvs b/Mult_Poly/standard_form_extras.pvs → mult_poly/standard_form_extras.pvs
diff --git a/Mult_Poly/standard_form_mult_poly.prf → mult_poly/standard_form_mult_poly.prf b/Mult_Poly/standard_form_mult_poly.prf → mult_poly/standard_form_mult_poly.prf
diff --git a/Mult_Poly/standard_form_mult_poly.prl → mult_poly/standard_form_mult_poly.prl b/Mult_Poly/standard_form_mult_poly.prl → mult_poly/standard_form_mult_poly.prl
diff --git a/Mult_Poly/standard_form_mult_poly.pvs → mult_poly/standard_form_mult_poly.pvs b/Mult_Poly/standard_form_mult_poly.pvs → mult_poly/standard_form_mult_poly.pvs
diff --git a/Mult_Poly/standard_form_poly.prf → mult_poly/standard_form_poly.prf b/Mult_Poly/standard_form_poly.prf → mult_poly/standard_form_poly.prf
diff --git a/Mult_Poly/standard_form_poly.pvs → mult_poly/standard_form_poly.pvs b/Mult_Poly/standard_form_poly.pvs → mult_poly/standard_form_poly.pvs
diff --git a/Mult_Poly/standard_form_unique.prf → mult_poly/standard_form_unique.prf b/Mult_Poly/standard_form_unique.prf → mult_poly/standard_form_unique.prf
diff --git a/Mult_Poly/standard_form_unique.pvs → mult_poly/standard_form_unique.pvs b/Mult_Poly/standard_form_unique.pvs → mult_poly/standard_form_unique.pvs
diff --git a/Mult_Poly/top.pvs → mult_poly/top.pvs b/Mult_Poly/top.pvs → mult_poly/top.pvs
diff --git a/nasalib.all b/nasalib.all
@@ -64,6 +64,7 @@ ASP                 # Denotational semantics of Answer Set Programming. Contribu
 mv_analysis
 ODEs
 dL
+mult_poly
 #
 # Deprecated libraries
 #
-Original file line number
+Diff line change
@@ Expand Up @@
     mv_analysis
     ODEs
     dL
+    mult_poly
     #
     # Deprecated libraries
     #
@@ Expand Down @@