From fa7413bb9a9aafaaecb7c284b1966e098fb7e188 Mon Sep 17 00:00:00 2001
From: Inigo Incer <inigo@eecs.berkeley.edu>
Date: Fri, 7 Apr 2023 09:41:44 -0700
Subject: [PATCH] Improving formatting

---
 docs/getting_started.ipynb | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/docs/getting_started.ipynb b/docs/getting_started.ipynb
index e3ae48d..4107e84 100644
--- a/docs/getting_started.ipynb
+++ b/docs/getting_started.ipynb
@@ -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: "
@@ -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:"
@@ -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`."
    ]
   },
   {
@@ -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:"
    ]
@@ -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:"