158 develop introductory jupyter notebook that shows pactis use cases (…

…#174) * minor * minor * rename * minor * rename * rename * hide edit button from webpage * Many edits * minor * minor * base64 * saving outputs * now saving ALL outputs * typo * header change * minor
pacti-org · Feb 20, 2023 · 1d1718e · 1d1718e
1 parent fa7cc18
commit 1d1718e
Show file tree

Hide file tree

Showing 13 changed files with 3,571 additions and 47 deletions.
diff --git a/docs/command-line-interface.md b/docs/command-line-interface.md
@@ -0,0 +1,45 @@
+## Examples
+
+
+### Composition
+
+
+Suppose we have the following system:
+
+<img src="source/_static/exports/circuit_series_composition_black.svg" width="350" alt="Buffers connected in series">
+
+
+Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \le 2, o \le i \le 2o + 2)$ and $C' = (-1 \le o \le 1/5, o' \le o)$. We can use Pacti to obtain the specification of the system by executing the command
+
+`pacti examples/example.json result.json`
+
+Pacti places the result of composition in the file result.json. The output is
+
+```
+  Composed contract:      
+  InVars: [<Var i>]       
+  OutVars:[<Var o_p>]     
+  A: 5*i <= 1, -1/2*i <= 0
+  G: -1*i + 1*o_p <= 0
+```
+
+### Quotient
+
+
+Now we consider an example of quotient. Consider the following circuits:
+
+<img src="source/_static/exports/circuit_series_quotient_black.svg" width="350" alt="Buffers connected in series">
+
+We wish to implement a system $M$ with specification $C = (|i| \le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing so that the resulting object meets the specification $C$. We run the command
+
+`pacti examples/example_quotient.json result.json`
+
+And Pacti outputs
+
+```
+  Contract quotient:
+  InVars: [<Var o>]
+  OutVars:[<Var o_p>]
+  A: 1*o <= 2, -1*o <= 2
+  G: -1*o + 1*o_p <= 1, 1*o + -1*o_p <= -1
+```
diff --git a/docs/css/material.css b/docs/css/material.css
@@ -2,3 +2,8 @@
 .md-main__inner {
   margin-bottom: 1.5rem;
 }
+
+
+.md-content__button {
+  display: none;
+}
diff --git a/docs/getting_started.ipynb b/docs/getting_started.ipynb
diff --git a/docs/index.md b/docs/index.md
@@ -10,48 +10,4 @@ system using assume-guarantee specifications, or contracts. Pacti's capabilities
 - Computing specifications of subsystems that need to be added to a design in order to meet an objective.
 - Verifying whether a component meets a specification.
 
-## Examples
 
-
-### Composition
-
-
-Suppose we have the following system:
-
-<img src="source/_static/exports/circuit_series_composition_black.svg" width="350" alt="Buffers connected in series">
-
-
-Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \le 2, o \le i \le 2o + 2)$ and $C' = (-1 \le o \le 1/5, o' \le o)$. We can use Pacti to obtain the specification of the system by executing the command
-
-`pacti examples/example.json result.json`
-
-Pacti places the result of composition in the file result.json. The output is
-
-```
-  Composed contract:      
-  InVars: [<Var i>]       
-  OutVars:[<Var o_p>]     
-  A: 5*i <= 1, -1/2*i <= 0
-  G: -1*i + 1*o_p <= 0
-```
-
-### Quotient
-
-
-Now we consider an example of quotient. Consider the following circuits:
-
-<img src="source/_static/exports/circuit_series_quotient_black.svg" width="350" alt="Buffers connected in series">
-
-We wish to implement a system $M$ with specification $C = (|i| \le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing so that the resulting object meets the specification $C$. We run the command
-
-`pacti examples/example_quotient.json result.json`
-
-And Pacti outputs
-
-```
-  Contract quotient:
-  InVars: [<Var o>]
-  OutVars:[<Var o_p>]
-  A: 1*o <= 2, -1*o <= 2
-  G: -1*o + 1*o_p <= 1, 1*o + -1*o_p <= -1
-```
diff --git a/docs/getting_started.md → docs/installing.md b/docs/getting_started.md → docs/installing.md
diff --git a/docs/source/_static/circuit_series_composition_background.ai b/docs/source/_static/circuit_series_composition_background.ai
diff --git a/docs/source/_static/circuit_series_quotient_background.ai b/docs/source/_static/circuit_series_quotient_background.ai
diff --git a/docs/source/_static/exports/circuit_series_composition_background.png b/docs/source/_static/exports/circuit_series_composition_background.png
diff --git a/docs/source/_static/exports/circuit_series_composition_background.svg b/docs/source/_static/exports/circuit_series_composition_background.svg
diff --git a/docs/source/_static/exports/circuit_series_quotient_background.png b/docs/source/_static/exports/circuit_series_quotient_background.png
diff --git a/docs/source/_static/exports/circuit_series_quotient_background.svg b/docs/source/_static/exports/circuit_series_quotient_background.svg
diff --git a/examples/wip/contract_satisfaction.py b/examples/wip/contract_satisfaction.py
@@ -0,0 +1,29 @@
+
+from pacti.terms.polyhedra import PolyhedralContract, PolyhedralTermList, PolyhedralTerm
+from pacti.iocontract import Var
+
+
+contract = PolyhedralContract.from_string(
+    InputVars=["x"],
+    OutputVars=["y"],
+    assumptions=["x <= 2"],
+    guarantees=["2x + 3y <= 7", "2y - 3x <= 8"])
+print(contract)
+
+x = Var("x")
+y = Var("y")
+print(contract.a.contains_behavior({x:5}))
+print(contract.a.contains_behavior({x:0}))
+print(contract.g.contains_behavior({x:0, y:2}))
+print(contract.g.contains_behavior({x:0, y:5}))
+
+
+# now verify component
+t1 = PolyhedralTerm(variables={x:1},constant=3)
+t2 = PolyhedralTerm(variables={x:-1},constant=-3)
+t3 = PolyhedralTerm(variables={y:1},constant=2)
+t4 = PolyhedralTerm(variables={y:-1},constant=-2)
+component = PolyhedralTermList([t1,t2,t3,t4])
+
+print(contract.contains_environment(component))
+print(contract.contains_implementation(component))
diff --git a/mkdocs.yml b/mkdocs.yml
@@ -9,7 +9,8 @@ watch: [README.md, CONTRIBUTING.md, CHANGELOG.md, src/pacti]
 nav:
 - Home:
   - Overview: index.md
-  - Getting started: getting_started.md
+  - Installing: installing.md
+  - Getting Started: getting_started.ipynb
   - Changelog: changelog.md
   - Credits: credits.md
   - License: license.md
@@ -21,7 +22,7 @@ nav:
   - Multi-agent Coordination: _case_studies/multiagent_coordination/multiagent.ipynb
   - Signal Processing in Digital ICs: _case_studies/digital_signal_processing/dsp_wl.ipynb
   - Synthetic Biology: _case_studies/biocircuit_specifications/specification_based_synthetic_biology.ipynb
-- Documentation: #reference/
+- API: #reference/
   - IoContract: iocontract.md
   - PolyhedralTerms : Polyhedral.md
 - Development:
@@ -108,4 +109,4 @@ plugins:
 extra:
   social:
   - icon: fontawesome/brands/github
-    link: https://github.com/github_username
+    link: https://github.com/FormalSystems