158 develop introductory jupyter notebook that shows pactis use cases

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
+```

docs/css/material.css

@@ -2,3 +2,8 @@
 .md-main__inner {
   margin-bottom: 1.5rem;
 }
+
+
+.md-content__button {
+  display: none;
+}

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
-```

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))

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