Skip to content

Commit

Permalink
Improving formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
iincer committed Apr 7, 2023
1 parent 4ae0dc3 commit fa7413b
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions docs/getting_started.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@
"\n",
"| Component | Contract | Inputs | Outputs | Assumptions | Guarantees |\n",
"| - | - | - | - | - | - |\n",
"| $M$ | `contract1` | `i` | `o` | `\\|i\\| <= 2` | `o <= i <= 2o + 2` |\n",
"| $M$ | `contract1` | `i` | `o` | `|i| <= 2` | `o <= i <= 2o + 2` |\n",
"| $M'$ | `contract2` | `o` | `o_p` | `-1 <= o <= 1/5` | `o_p <= o` |\n",
"\n",
"We can use Pacti to obtain the contract of the system that assembles these two components as follows: "
Expand Down Expand Up @@ -102,7 +102,7 @@
"\n",
"| Component | Contract | Inputs | Outputs | Assumptions | Guarantees |\n",
"| - | - | - | - | - | - |\n",
"| $M_1$ | `contract1_n` | `i` | `o` | `\\|i\\| <= 2` | `\\|o\\| <= 3` |\n",
"| $M_1$ | `contract1_n` | `i` | `o` | `|i| <= 2` | `|o| <= 3` |\n",
"| $M'$ | `contract2` | `o` | `o_p` | `-1 <= o <= 1/5` | `o_p <= o` |\n",
"\n",
"The Pacti specification then becomes the following:"
Expand Down Expand Up @@ -151,7 +151,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"Pacti is unable to compute a system specification. In this case, this is due to the fact that our guarantee `\\|o\\| <= 3` for $M_1$ does not satisfy the assumptions of `contract2`."
"Pacti is unable to compute a system specification. In this case, this is due to the fact that our guarantee `|o| <= 3` for $M_1$ does not satisfy the assumptions of `contract2`."
]
},
{
Expand All @@ -175,8 +175,8 @@
"\n",
"| Component | Contract | Inputs | Outputs | Assumptions | Guarantees |\n",
"| - | - | - | - | - | - |\n",
"| $M$ | `contract_top_level` | `i` | `o_p` | `\\|i\\| <= 1` | `o_p = 2i + 1` |\n",
"| $M'$ | `contract_existing_subsystem` | `i` | `o` | `\\|i\\| <= 2` | `o = 2i` |\n",
"| $M$ | `contract_top_level` | `i` | `o_p` | `|i| <= 1` | `o_p = 2i + 1` |\n",
"| $M'$ | `contract_existing_subsystem` | `i` | `o` | `|i| <= 2` | `o = 2i` |\n",
"\n",
"We use Pacti's quotient operation to obtain the specification of the missing subsystem corresponding to the question mark above so that the resulting object meets the specification `contract_top_level`. The following codifies this missing subsystem problem:"
]
Expand Down Expand Up @@ -258,7 +258,7 @@
"\n",
"| Viewpoint | Contract | Inputs | Outputs | Assumptions | Guarantees |\n",
"| - | - | - | - | - | - |\n",
"| Functionality | `functionality_viewpoint` | `i` | `o` | `\\|i\\| <= 2` | `o = 2i + 1` |\n",
"| Functionality | `functionality_viewpoint` | `i` | `o` | `|i| <= 2` | `o = 2i + 1` |\n",
"| Power | `power_viewpoint` | `temp` | `P` | `temp <= 90` | `P <= 2.1` |\n",
"\n",
"We can use contract merging to obtain a single specification for the subsystem:"
Expand Down

0 comments on commit fa7413b

Please sign in to comment.