Repository: pacti-org/pacti (language: python)

Issue:
Generate tests & Improve code quality of DSP case study
## Tests

Please extract tests for Pacti from your case study. To do this, use the following statement:
```py
from pacti import write_contracts_to_file
```
Then, supposing that contracts `c1` and `c2` are two contracts, and `c3` is the result of composition (or other operation), say
```py
write_contracts_to_file([c1, c2, c3], ["contract1", "contract2", "contract3"], "file_name.json")
```
This will place the three contracts in the file `file_name.json`. Afterwards, move this file to 
```
tests/test_data/polyhedral_contracts/test_composition_success_<description_or_number>.json
```
In this file name, you can replace "composition" with "merging" or "quotient."
The word "success" means that the test framework will expect three contracts in the file. The first two are arguments of the operation and the third is the result.
The word "success" can be replaced by "failure." In this case, the framework will expect two contracts in the file. The framework will expect Pacti to say that there was a problem computing this operation.

If you place two contracts in a test file, and you name the file
```
test_refinement_<description_or_number>.json
```
the test framework will test that the first argument is a refinement of the second.

After you add your test to the folder `tests/test_data/polyhedral_contracts/`, it will be executed when you run make test.


## Code quality


In the file `duties.py`, replace the line
```py
PY_SRC_PATHS = (Path(_) for _ in ("src", "tests", "case_studies"))
```
with 
```py
PY_SRC_PATHS = (Path(_) for _ in ("case_studies/<your case_study>"))
```
Make sure the following commands give zero errors:
```
make check-jn-quality
check-jn-types
check-quality
check-types
```
The first two address jupyter notebooks. The other two analyze your python code.

When analyzing code quality, the linter will sometime say that a linter will make changes. Running the command
```
make format
```
may lower the number of violations.


Discussion / hints:

Fix patch:
diff --git a/case_studies/digital_signal_processing/dsp_wl.ipynb b/case_studies/digital_signal_processing/dsp_wl.ipynb
index 7f69f548..a35b56eb 100644
--- a/case_studies/digital_signal_processing/dsp_wl.ipynb
+++ b/case_studies/digital_signal_processing/dsp_wl.ipynb
@@ -58,7 +58,10 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "from tool import *\n",
+    "\"\"\"DSP Case Study Code\"\"\"\n",
+    "import itertools\n",
+    "\n",
+    "from tool import PortWordLength, float_to_bin, port_add, port_mult\n",
     "\n",
     "from pacti.terms.polyhedra import PolyhedralContract"
    ]
@@ -82,10 +85,14 @@
     "# Definition of value_num method in PortWordLength class\n",
     "#    def value_num(self):\n",
     "#        return int(self.value, base=2) * 2 ** (- (self.n - self.p))\n",
+    "def show_wordlength() -> None:\n",
+    "    \"\"\"Show the wordlength structure\"\"\"\n",
+    "    port = PortWordLength(n=5, p=2, value=\"11011\")\n",
+    "    print(f'The word length (n = {port.n}, p = {port.p}) of the bits \"{port.value}\" is: ')\n",
+    "    print(port.value_num())\n",
+    "\n",
     "\n",
-    "port = PortWordLength(n=5, p=2, value=\"11011\")\n",
-    "print(f'The word length (n = {port.n}, p = {port.p}) of the bits \"{port.value}\" is: ')\n",
-    "print(port.value_num())"
+    "show_wordlength()"
    ]
   },
   {
@@ -173,18 +180,35 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def truncation_error_same_position(pi, po):\n",
+    "def truncation_error_same_position(pi: PortWordLength, po: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Truncation error for the case where input ports and output ports have the same number of integer bits.\n",
+    "\n",
+    "    Args:\n",
+    "        pi: PortWordLength: input port word length\n",
+    "        po: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The maximum truncation error if a number is truncated from wordlength pi to wordlength po\n",
+    "    \"\"\"\n",
     "    assert pi.p == po.p\n",
     "    if pi.n > po.n:\n",
-    "        return 2**po.p * (2 ** (-po.n) - 2 ** (-pi.n))\n",
-    "    else:\n",
-    "        return 0\n",
+    "        return float(2**po.p * (2 ** (-po.n) - 2 ** (-pi.n)))\n",
+    "    return 0\n",
+    "\n",
     "\n",
+    "def truncate(pi: PortWordLength, po: PortWordLength) -> None:\n",
+    "    \"\"\"\n",
+    "    Truncate the value in pi into po.\n",
     "\n",
-    "def truncate(pi, po):\n",
+    "    Args:\n",
+    "        pi: PortWordLength: input port word length\n",
+    "        po: PortWordLength: input port word length\n",
+    "    \"\"\"\n",
     "    # separate the bits into two parts, before binary point and after binary point\n",
-    "    bits_before_point = pi.value[: pi.p]\n",
-    "    bits_after_point = pi.value[pi.p :]\n",
+    "    bits_str: str = str(pi.value)\n",
+    "    bits_before_point = bits_str[: pi.p]\n",
+    "    bits_after_point = bits_str[pi.p :]\n",
     "\n",
     "    # truncate or appending 0\n",
     "    if po.p >= pi.p:\n",
@@ -199,8 +223,7 @@
     "\n",
     "    # combine the both parts\n",
     "    ret = bits_before_point + bits_after_point\n",
-    "    po.value = ret\n",
-    "    return po.value"
+    "    po.value = ret"
    ]
   },
   {
@@ -223,17 +246,22 @@
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=2, name=\"p1\", value=\"1111111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "def example_truncation_error_same_position() -> None:\n",
+    "    \"\"\"The example showing truncation error for same number of integer bits\"\"\"\n",
+    "    p1 = PortWordLength(n=7, p=2, name=\"p1\", value=\"1111111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "\n",
+    "    print(\"Truncation Error: \")\n",
+    "    print(truncation_error_same_position(p1, p2))\n",
+    "    print(\"Example Value to produce the error\")\n",
     "\n",
-    "print(\"Truncation Error: \")\n",
-    "print(truncation_error_same_position(p1, p2))\n",
-    "print(\"Example Value to produce the error\")\n",
+    "    truncate(p1, p2)\n",
+    "    print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
+    "    print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
+    "    print(\"p1 - p2 = \", p1.value_num() - p2.value_num())\n",
     "\n",
-    "truncate(p1, p2)\n",
-    "print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
-    "print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
-    "print(f\"p1 - p2 = \", p1.value_num() - p2.value_num())"
+    "\n",
+    "example_truncation_error_same_position()"
    ]
   },
   {
@@ -273,7 +301,17 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def truncation_error(pi, po):\n",
+    "def truncation_error(pi: PortWordLength, po: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Truncation error for the case where input ports and output ports have different number of integer bits.\n",
+    "\n",
+    "    Args:\n",
+    "        pi: PortWordLength: input port word length\n",
+    "        po: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The maximum truncation error if a number is truncated from wordlength pi to wordlength po\n",
+    "    \"\"\"\n",
     "    # remove uneccesary most significant bits\n",
     "    # Remider: The assumption must hold!!\n",
     "    pi_adjusted = PortWordLength(n=pi.n - pi.p + po.p, p=po.p)\n",
@@ -281,22 +319,41 @@
     "    return truncation_error_same_position(pi=pi_adjusted, po=po)\n",
     "\n",
     "\n",
-    "def get_assumption_value(pi, po):\n",
+    "def get_assumption_value(pi: PortWordLength, po: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Compute the assumption required for truncation to ensure no loss of integer values.\n",
+    "\n",
+    "    Args:\n",
+    "        pi: PortWordLength: input port word length\n",
+    "        po: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The maximum bound pi such that it won't loss integer bits after truncation\n",
+    "    \"\"\"\n",
     "    if pi.p > po.p:\n",
-    "        return 2**po.p\n",
-    "    else:\n",
-    "        return float(\"inf\")  # no additional assumption needed\n",
+    "        return float(2**po.p)\n",
+    "    return float(\"inf\")  # no additional assumption needed\n",
     "\n",
     "\n",
-    "def check_assumption_value(pi, po):\n",
+    "def check_assumption_value(pi: PortWordLength, po: PortWordLength) -> bool:\n",
+    "    \"\"\"\n",
+    "    Check if the value of the input port satisfy the assumption for truncation.\n",
+    "\n",
+    "    Args:\n",
+    "        pi: PortWordLength: input port word length\n",
+    "        po: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        If the assumption to prevent integer bit loss is satisfied\n",
+    "    \"\"\"\n",
     "    assumption_value = get_assumption_value(pi, po)\n",
     "    print(f\"Assumption: {pi.name} < {assumption_value}\")\n",
-    "    if not pi.value_num() < assumption_value:\n",
+    "    if pi.value_num() >= assumption_value:\n",
     "        print(\"Assumption failed, truncation of MSB occurs\")\n",
     "        return False\n",
-    "    else:\n",
-    "        print(f\"Assumption Satisfied ({pi.name} = {pi.value_num()} < {assumption_value})\")\n",
-    "        return True"
+    "\n",
+    "    print(f\"Assumption Satisfied ({pi.name} = {pi.value_num()} < {assumption_value})\")\n",
+    "    return True"
    ]
   },
   {
@@ -309,8 +366,8 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "Assumption: p1 < 4\n",
-      "Assumption Satisfied (p1 = 2.4375 < 4)\n",
+      "Assumption: p1 < 4.0\n",
+      "Assumption Satisfied (p1 = 2.4375 < 4.0)\n",
       "Truncation Error: \n",
       "0.0625\n",
       "Example Value to produce the error\n",
@@ -321,19 +378,24 @@
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "def example_truncation_error() -> None:\n",
+    "    \"\"\"Example showing the truncation error\"\"\"\n",
+    "    p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "\n",
+    "    assert check_assumption_value(pi=p1, po=p2)\n",
+    "\n",
+    "    print(\"Truncation Error: \")\n",
+    "    print(truncation_error(p1, p2))\n",
+    "    print(\"Example Value to produce the error\")\n",
     "\n",
-    "assert check_assumption_value(pi=p1, po=p2)\n",
+    "    truncate(p1, p2)\n",
+    "    print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
+    "    print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
+    "    print(\"p1 - p2 = \", p1.value_num() - p2.value_num())\n",
     "\n",
-    "print(\"Truncation Error: \")\n",
-    "print(truncation_error(p1, p2))\n",
-    "print(\"Example Value to produce the error\")\n",
     "\n",
-    "truncate(p1, p2)\n",
-    "print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
-    "print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
-    "print(f\"p1 - p2 = \", p1.value_num() - p2.value_num())"
+    "example_truncation_error()"
    ]
   },
   {
@@ -377,21 +439,45 @@
    "outputs": [],
    "source": [
     "def compute_required_word_length_add(in1: PortWordLength, in2: PortWordLength) -> PortWordLength:\n",
+    "    \"\"\"\n",
+    "    Compute the minimum word length to hold all values after addition operation on the inputs without lossing any information.\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The minimum word length to hold all values after addition operation on the inputs without lossing any information.\n",
+    "    \"\"\"\n",
     "    new_n = max(in1.n, in2.n - in2.p + in1.p) - min(0, in1.p - in2.p) + 1\n",
     "    new_p = max(in1.p, in2.p) + 1\n",
     "    return PortWordLength(n=new_n, p=new_p)\n",
     "\n",
     "\n",
-    "def error_truncation_add(p1, p2, po):\n",
-    "    print(f\"Input {p1.name}: (n={p1.n}, p={p1.p})\")\n",
-    "    print(f\"Input {p2.name}: (n={p2.n}, p={p2.p})\")\n",
-    "    p_ideal = compute_required_word_length_add(in1=p1, in2=p2)\n",
+    "def error_truncation_add(in1: PortWordLength, in2: PortWordLength, out: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Compute the maximum error of truncation caused by the addition operation.\n",
+    "\n",
+    "    The addition operation is perform for ports out = in1 + in2.\n",
+    "    The value of in1 + in2 is truncated to fit in out\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "        out: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The maximum error of truncation caused by the addition operation\n",
+    "    \"\"\"\n",
+    "    print(f\"Input {in1.name}: (n={in1.n}, p={in1.p})\")\n",
+    "    print(f\"Input {in2.name}: (n={in2.n}, p={in2.p})\")\n",
+    "    p_ideal = compute_required_word_length_add(in1=in1, in2=in2)\n",
     "    print(f\"Ideal Output: (n={p_ideal.n}, p={p_ideal.p})\")\n",
-    "    print(f\"Actual Output ({po.name}): (n={po.n}, p={po.p})\")\n",
+    "    print(f\"Actual Output ({out.name}): (n={out.n}, p={out.p})\")\n",
     "\n",
-    "    assumption_value = get_assumption_value(pi=p_ideal, po=po)\n",
-    "    print(f\"Assumption: {p1.name} + {p2.name} < {assumption_value}\")\n",
-    "    return truncation_error(pi=p_ideal, po=po)"
+    "    assumption_value = get_assumption_value(pi=p_ideal, po=out)\n",
+    "    print(f\"Assumption: {in1.name} + {in2.name} < {assumption_value}\")\n",
+    "    return truncation_error(pi=p_ideal, po=out)"
    ]
   },
   {
@@ -408,19 +494,24 @@
       "Input p2: (n=5, p=2)\n",
       "Ideal Output: (n=8, p=4)\n",
       "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 + p2 < 8\n",
+      "Assumption: p1 + p2 < 8.0\n",
       "Error of the addition calculation: 0.1875\n"
      ]
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "def example_truncation_error_add() -> None:\n",
+    "    \"\"\"Example showing truncation error of addition operation\"\"\"\n",
+    "    p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
     "\n",
-    "err = error_truncation_add(p1=p1, p2=p2, po=p3)\n",
+    "    err = error_truncation_add(in1=p1, in2=p2, out=p3)\n",
     "\n",
-    "print(f\"Error of the addition calculation: {err}\")"
+    "    print(f\"Error of the addition calculation: {err}\")\n",
+    "\n",
+    "\n",
+    "example_truncation_error_add()"
    ]
   },
   {
@@ -445,21 +536,45 @@
    "outputs": [],
    "source": [
     "def compute_required_word_length_mult(in1: PortWordLength, in2: PortWordLength) -> PortWordLength:\n",
+    "    \"\"\"\n",
+    "    Compute the minimum word length to hold all values after multiplication operation on the inputs without lossing any information.\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The minimum word length to hold all values after multiplication operation on the inputs without lossing any information.\n",
+    "    \"\"\"\n",
     "    new_n = in1.n + in2.n\n",
     "    new_p = in1.p + in2.p\n",
     "    return PortWordLength(n=new_n, p=new_p)\n",
     "\n",
     "\n",
-    "def error_truncation_mult(p1, p2, po):\n",
-    "    print(f\"Input {p1.name}: (n={p1.n}, p={p1.p})\")\n",
-    "    print(f\"Input {p2.name}: (n={p2.n}, p={p2.p})\")\n",
-    "    p_ideal = compute_required_word_length_mult(in1=p1, in2=p2)\n",
+    "def error_truncation_mult(in1: PortWordLength, in2: PortWordLength, out: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Compute the maximum error of truncation caused by the multiplication operation.\n",
+    "\n",
+    "    The multiplication operation is perform for ports out = in1 * in2.\n",
+    "    The value of in1 * in2 is truncated to fit in out\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "        out: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The maximum error of truncation caused by the multiplication operation\n",
+    "    \"\"\"\n",
+    "    print(f\"Input {in1.name}: (n={in1.n}, p={in1.p})\")\n",
+    "    print(f\"Input {in2.name}: (n={in2.n}, p={in2.p})\")\n",
+    "    p_ideal = compute_required_word_length_mult(in1=in1, in2=in2)\n",
     "    print(f\"Ideal Output: (n={p_ideal.n}, p={p_ideal.p})\")\n",
-    "    print(f\"Actual Output ({po.name}): (n={po.n}, p={po.p})\")\n",
+    "    print(f\"Actual Output ({out.name}): (n={out.n}, p={out.p})\")\n",
     "\n",
-    "    assumption_value = get_assumption_value(pi=p_ideal, po=po)\n",
-    "    print(f\"Assumption: {p1.name} * {p2.name} < {assumption_value}\")\n",
-    "    return truncation_error(pi=p_ideal, po=po)"
+    "    assumption_value = get_assumption_value(pi=p_ideal, po=out)\n",
+    "    print(f\"Assumption: {in1.name} * {in2.name} < {assumption_value}\")\n",
+    "    return truncation_error(pi=p_ideal, po=out)"
    ]
   },
   {
@@ -476,19 +591,24 @@
       "Input p2: (n=5, p=2)\n",
       "Ideal Output: (n=12, p=5)\n",
       "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 * p2 < 8\n",
+      "Assumption: p1 * p2 < 8.0\n",
       "Error of the multiplication calculation: 0.2421875\n"
      ]
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "def example_truncation_error_mult() -> None:\n",
+    "    \"\"\"Example showing truncation error of multiplication operation\"\"\"\n",
+    "    p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "\n",
+    "    err = error_truncation_mult(in1=p1, in2=p2, out=p3)\n",
     "\n",
-    "err = error_truncation_mult(p1=p1, p2=p2, po=p3)\n",
+    "    print(f\"Error of the multiplication calculation: {err}\")\n",
     "\n",
-    "print(f\"Error of the multiplication calculation: {err}\")"
+    "\n",
+    "example_truncation_error_mult()"
    ]
   },
   {
@@ -544,8 +664,19 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def error_propagation_add(p1, p2, po):\n",
-    "    return p1.e + p2.e"
+    "def error_propagation_add(in1: PortWordLength, in2: PortWordLength, out: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Compute the propagation error caused by addtion operation.\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "        out: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The propagation error caused by addtion operation given the known error in the inputs.\n",
+    "    \"\"\"\n",
+    "    return float(in1.e + in2.e)"
    ]
   },
   {
@@ -562,7 +693,7 @@
       "Input p2: (n=5, p=2)\n",
       "Ideal Output: (n=8, p=4)\n",
       "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 + p2 < 8\n",
+      "Assumption: p1 + p2 < 8.0\n",
       "Propagation error: 0.7\n",
       "Truncation error: 0.1875\n",
       "Error bound of the addition calculation: 0.8875\n"
@@ -570,17 +701,24 @@
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, e=0.5, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, e=0.2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "def example_propagation_error_add() -> None:\n",
+    "    \"\"\"Example showing propagation error of addition operation\"\"\"\n",
+    "    e1 = 0.5\n",
+    "    e2 = 0.2\n",
+    "    p1 = PortWordLength(n=7, p=3, e=e1, name=\"p1\", value=\"0100111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, e=e2, name=\"p2\")\n",
+    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "\n",
+    "    e_p = error_propagation_add(in1=p1, in2=p2, out=p3)\n",
+    "    e_t = error_truncation_add(in1=p1, in2=p2, out=p3)\n",
     "\n",
-    "e_p = error_propagation_add(p1=p1, p2=p2, po=p3)\n",
-    "e_t = error_truncation_add(p1=p1, p2=p2, po=p3)\n",
+    "    err = e_p + e_t\n",
+    "    print(f\"Propagation error: {e_p}\")\n",
+    "    print(f\"Truncation error: {e_t}\")\n",
+    "    print(f\"Error bound of the addition calculation: {err}\")\n",
     "\n",
-    "err = e_p + e_t\n",
-    "print(f\"Propagation error: {e_p}\")\n",
-    "print(f\"Truncation error: {e_t}\")\n",
-    "print(f\"Error bound of the addition calculation: {err}\")"
+    "\n",
+    "example_propagation_error_add()"
    ]
   },
   {
@@ -603,12 +741,19 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def get_actual_possible_value(in_port: PortWordLength):\n",
-    "    return (1 - (2**-in_port.n)) * 2**in_port.p\n",
-    "\n",
-    "\n",
-    "def error_propagation_mult(p1, p2, po):\n",
-    "    return p1.a * p2.e + p2.a * p1.e + p1.e * p2.e"
+    "def error_propagation_mult(in1: PortWordLength, in2: PortWordLength, out: PortWordLength) -> float:\n",
+    "    \"\"\"\n",
+    "    Compute the propagation error caused by multiplication operation.\n",
+    "\n",
+    "    Args:\n",
+    "        in1: PortWordLength: input port word length\n",
+    "        in2: PortWordLength: input port word length\n",
+    "        out: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The propagation error caused by multiplication operation given the known error in the inputs.\n",
+    "    \"\"\"\n",
+    "    return float(in1.a * in2.e + in2.a * in1.e + in1.e * in2.e)"
    ]
   },
   {
@@ -625,7 +770,7 @@
       "Input p2: (n=5, p=2)\n",
       "Ideal Output: (n=12, p=5)\n",
       "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 * p2 < 8\n",
+      "Assumption: p1 * p2 < 8.0\n",
       "Propagation error: 2.81875\n",
       "Truncation error: 0.2421875\n",
       "Error bound of the multiplication calculation: 3.0609375\n"
@@ -633,17 +778,24 @@
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, e=0.5, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, e=0.3, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "def example_propagation_error_mult() -> None:\n",
+    "    \"\"\"Example showing propagation error of multiplication operation\"\"\"\n",
+    "    e1 = 0.5\n",
+    "    e2 = 0.3\n",
+    "    p1 = PortWordLength(n=7, p=3, e=e1, name=\"p1\", value=\"0100111\")\n",
+    "    p2 = PortWordLength(n=5, p=2, e=e2, name=\"p2\")\n",
+    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "\n",
+    "    e_p = error_propagation_mult(in1=p1, in2=p2, out=p3)\n",
+    "    e_t = error_truncation_mult(in1=p1, in2=p2, out=p3)\n",
+    "\n",
+    "    err = e_p + e_t\n",
+    "    print(f\"Propagation error: {e_p}\")\n",
+    "    print(f\"Truncation error: {e_t}\")\n",
+    "    print(f\"Error bound of the multiplication calculation: {err}\")\n",
     "\n",
-    "e_p = error_propagation_mult(p1=p1, p2=p2, po=p3)\n",
-    "e_t = error_truncation_mult(p1=p1, p2=p2, po=p3)\n",
     "\n",
-    "err = e_p + e_t\n",
-    "print(f\"Propagation error: {e_p}\")\n",
-    "print(f\"Truncation error: {e_t}\")\n",
-    "print(f\"Error bound of the multiplication calculation: {err}\")"
+    "example_propagation_error_mult()"
    ]
   },
   {
@@ -687,8 +839,23 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def form_contract_add(in_port1, in_port2, out_port):\n",
-    "    ret_contract = {}\n",
+    "def form_contract_add(\n",
+    "    in_port1: PortWordLength, in_port2: PortWordLength, out_port: PortWordLength\n",
+    ") -> dict[str, object]:\n",
+    "    \"\"\"\n",
+    "    Create contract in dictionary form for an addition operation.\n",
+    "\n",
+    "    The contract includes information about the bound for its output value and the bound for its maximum error\n",
+    "\n",
+    "    Args:\n",
+    "        in_port1: PortWordLength: input port word length\n",
+    "        in_port2: PortWordLength: input port word length\n",
+    "        out_port: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The contract in dictionary form for an addition operation.\n",
+    "    \"\"\"\n",
+    "    ret_contract: dict[str, object] = {}\n",
     "    # define input/output vars\n",
     "    ret_contract[\"input_vars\"] = [\n",
     "        f\"{in_port1.name}_a\",\n",
@@ -701,20 +868,20 @@
     "    ideal_out_port = compute_required_word_length_add(in1=in_port1, in2=in_port2)\n",
     "    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)\n",
     "    # write assumption in the contract\n",
-    "    if assumption_value != float(\"inf\"):\n",
+    "    if assumption_value == float(\"inf\"):\n",
+    "        ret_contract[\"assumptions\"] = []\n",
+    "    else:\n",
     "        ret_contract[\"assumptions\"] = [\n",
     "            {\"coefficients\": {f\"{in_port1.name}_a\": 1, f\"{in_port2.name}_a\": 1}, \"constant\": assumption_value}\n",
     "        ]\n",
-    "    else:\n",
-    "        ret_contract[\"assumptions\"] = []\n",
     "    # get guarantee\n",
-    "    e_t = truncation_error(pi=ideal_out_port, po=out_port)\n",
+    "    e_trunc = truncation_error(pi=ideal_out_port, po=out_port)\n",
     "\n",
     "    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints\n",
     "    ret_contract[\"guarantees\"] = [\n",
     "        {\n",
     "            \"coefficients\": {f\"{in_port1.name}_e\": -1, f\"{in_port2.name}_e\": -1, f\"{out_port.name}_e\": 1},\n",
-    "            \"constant\": e_t,\n",
+    "            \"constant\": e_trunc,\n",
     "        },\n",
     "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": out_port.a},\n",
     "        # {\"coefficients\":{f\"{out_port.name}_a\": 1}, \"constant\":in_port1.a + in_port2.a},\n",
@@ -723,39 +890,54 @@
     "    return ret_contract\n",
     "\n",
     "\n",
-    "def form_contract_mult_const(in_port1, in_port_const, out_port):\n",
-    "    ret_contract = {}\n",
+    "def form_contract_mult_const(\n",
+    "    in_port: PortWordLength, in_port_const: PortWordLength, out_port: PortWordLength\n",
+    ") -> dict[str, object]:\n",
+    "    \"\"\"\n",
+    "    Create contract in dictionary form for a constant coefficient multiplication operation.\n",
+    "\n",
+    "    The contract includes information about the bound for its output value and the bound for its maximum error\n",
+    "\n",
+    "    Args:\n",
+    "        in_port: PortWordLength: input port word length\n",
+    "        in_port_const: PortWordLength: constant input port word length\n",
+    "        out_port: PortWordLength: output port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The contract in dictionary form for a constant coefficient multiplication operation.\n",
+    "    \"\"\"\n",
+    "    ret_contract: dict[str, object] = {}\n",
     "    # define input/output vars\n",
-    "    ret_contract[\"input_vars\"] = [f\"{in_port1.name}_a\", f\"{in_port1.name}_e\"]\n",
+    "    ret_contract[\"input_vars\"] = [f\"{in_port.name}_a\", f\"{in_port.name}_e\"]\n",
     "    ret_contract[\"output_vars\"] = [f\"{out_port.name}_a\", f\"{out_port.name}_e\"]\n",
     "    # get assumption\n",
-    "    ideal_out_port = compute_required_word_length_mult(in1=in_port1, in2=in_port_const)\n",
+    "    ideal_out_port = compute_required_word_length_mult(in1=in_port, in2=in_port_const)\n",
     "    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)\n",
     "    # write assumption in the contract\n",
-    "    if assumption_value != float(\"inf\"):\n",
+    "    if assumption_value == float(\"inf\"):\n",
+    "        ret_contract[\"assumptions\"] = []\n",
+    "    else:\n",
     "        print(assumption_value)\n",
     "        ret_contract[\"assumptions\"] = [\n",
-    "            {\"coefficients\": {f\"{in_port1.name}_a\": in_port_const.a}, \"constant\": assumption_value}\n",
+    "            {\"coefficients\": {f\"{in_port.name}_a\": in_port_const.a}, \"constant\": assumption_value}\n",
     "        ]\n",
-    "    else:\n",
-    "        ret_contract[\"assumptions\"] = []\n",
     "    # get guarantee\n",
     "    print(ideal_out_port.to_string())\n",
-    "    e_t = truncation_error(pi=ideal_out_port, po=out_port)\n",
+    "    e_trunc = truncation_error(pi=ideal_out_port, po=out_port)\n",
     "\n",
     "    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints\n",
     "    ret_contract[\"guarantees\"] = [\n",
     "        {\n",
     "            \"coefficients\": {\n",
-    "                f\"{in_port1.name}_e\": -in_port_const.a + in_port_const.e,\n",
-    "                f\"{in_port1.name}_a\": -in_port_const.e,\n",
+    "                f\"{in_port.name}_e\": -in_port_const.a + in_port_const.e,\n",
+    "                f\"{in_port.name}_a\": -in_port_const.e,\n",
     "                f\"{out_port.name}_e\": 1,\n",
     "            },\n",
-    "            \"constant\": e_t,\n",
+    "            \"constant\": e_trunc,\n",
     "        },\n",
     "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": out_port.a},\n",
-    "        # {\"coefficients\":{f\"{out_port.name}_a\": 1}, \"constant\":in_port_const.a * in_port1.a},\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1, f\"{in_port1.name}_a\": -in_port_const.a}, \"constant\": 0},\n",
+    "        # {\"coefficients\":{f\"{out_port.name}_a\": 1}, \"constant\":in_port_const.a * in_port.a},\n",
+    "        {\"coefficients\": {f\"{out_port.name}_a\": 1, f\"{in_port.name}_a\": -in_port_const.a}, \"constant\": 0},\n",
     "    ]\n",
     "    return ret_contract"
    ]
@@ -770,7 +952,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "{'input_vars': ['p1_a', 'p1_e', 'p2_a', 'p2_e'], 'output_vars': ['p3_a', 'p3_e'], 'assumptions': [{'coefficients': {'p1_a': 1, 'p2_a': 1}, 'constant': 8}], 'guarantees': [{'coefficients': {'p1_e': -1, 'p2_e': -1, 'p3_e': 1}, 'constant': 0.1875}, {'coefficients': {'p3_a': 1}, 'constant': 7.75}, {'coefficients': {'p3_a': 1, 'p1_a': -1, 'p2_a': -1}, 'constant': 0}]}\n",
+      "{'input_vars': ['p1_a', 'p1_e', 'p2_a', 'p2_e'], 'output_vars': ['p3_a', 'p3_e'], 'assumptions': [{'coefficients': {'p1_a': 1, 'p2_a': 1}, 'constant': 8.0}], 'guarantees': [{'coefficients': {'p1_e': -1, 'p2_e': -1, 'p3_e': 1}, 'constant': 0.1875}, {'coefficients': {'p3_a': 1}, 'constant': 7.75}, {'coefficients': {'p3_a': 1, 'p1_a': -1, 'p2_a': -1}, 'constant': 0}]}\n",
       "InVars: [p1_a, p1_e, p2_a, p2_e]\n",
       "OutVars:[p3_a, p3_e]\n",
       "A: [\n",
@@ -781,7 +963,7 @@
       "  p3_a <= 7.75\n",
       "  -p1_a - p2_a + p3_a <= 0.0\n",
       "]\n",
-      "8\n",
+      "8.0\n",
       "Port: , (n, p) = (12, 5), e = 0, a = 31.9921875\n",
       "InVars: [p4_a, p4_e]\n",
       "OutVars:[p6_a, p6_e]\n",
@@ -797,21 +979,26 @@
     }
    ],
    "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)\n",
-    "print(c1)\n",
-    "contract1 = PolyhedralContract.from_dict(c1)\n",
-    "print(str(contract1))\n",
-    "\n",
-    "\n",
-    "p4 = PortWordLength(n=7, p=3, name=\"p4\")\n",
-    "p5 = PortWordLength(n=5, p=2, e=0.03, value=\"11011\", name=\"p5\")  # const\n",
-    "p6 = PortWordLength(n=5, p=3, name=\"p6\")\n",
-    "c2 = form_contract_mult_const(in_port1=p4, in_port_const=p5, out_port=p6)\n",
-    "contract2 = PolyhedralContract.from_dict(c2)\n",
-    "print(str(contract2))"
+    "def example_contract_formulation() -> None:\n",
+    "    \"\"\"Example of contract formulation\"\"\"\n",
+    "    p1 = PortWordLength(n=7, p=3, name=\"p1\")\n",
+    "    p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
+    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
+    "    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)\n",
+    "    print(c1)\n",
+    "    contract1 = PolyhedralContract.from_dict(c1)\n",
+    "    print(str(contract1))\n",
+    "\n",
+    "    e5 = 0.03\n",
+    "    p4 = PortWordLength(n=7, p=3, name=\"p4\")\n",
+    "    p5 = PortWordLength(n=5, p=2, e=e5, value=\"11011\", name=\"p5\")  # const\n",
+    "    p6 = PortWordLength(n=5, p=3, name=\"p6\")\n",
+    "    c2 = form_contract_mult_const(in_port=p4, in_port_const=p5, out_port=p6)\n",
+    "    contract2 = PolyhedralContract.from_dict(c2)\n",
+    "    print(str(contract2))\n",
+    "\n",
+    "\n",
+    "example_contract_formulation()"
    ]
   },
   {
@@ -843,38 +1030,15 @@
    "execution_count": 17,
    "id": "690cd39b",
    "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Contract 1:\n",
-      "InVars: [p1_a, p1_e, p2_a, p2_e]\n",
-      "OutVars:[p3_a, p3_e]\n",
-      "A: [\n",
-      "  p1_a + p2_a <= 8.0\n",
-      "]\n",
-      "G: [\n",
-      "  -p1_e - p2_e + p3_e <= 0.125\n",
-      "  p3_a <= 7.75\n",
-      "  -p1_a - p2_a + p3_a <= 0.0\n",
-      "]\n",
-      "Contract 2:\n",
-      "InVars: [p3_a, p3_e, p4_a, p4_e]\n",
-      "OutVars:[p5_a, p5_e]\n",
-      "A: [\n",
-      "  p3_a + p4_a <= 8.0\n",
-      "]\n",
-      "G: [\n",
-      "  -p3_e - p4_e + p5_e <= 0.0625\n",
-      "  p5_a <= 7.875\n",
-      "  -p3_a - p4_a + p5_a <= 0.0\n",
-      "]\n"
-     ]
-    }
-   ],
+   "outputs": [],
    "source": [
-    "def create_example1():\n",
+    "def create_example1() -> tuple:\n",
+    "    \"\"\"\n",
+    "    Generate the example contracts and ports for the example\n",
+    "\n",
+    "    Returns:\n",
+    "        A tuple with 2 elements. The first one is the list of contract, and the other is the list of ports\n",
+    "    \"\"\"\n",
     "    p1 = PortWordLength(n=5, p=2, name=\"p1\")\n",
     "    p2 = PortWordLength(n=5, p=3, name=\"p2\")\n",
     "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
@@ -886,12 +1050,9 @@
     "\n",
     "    contract1 = PolyhedralContract.from_dict(c1)\n",
     "    contract2 = PolyhedralContract.from_dict(c2)\n",
-    "    print(\"Contract 1:\\n\" + str(contract1))\n",
-    "    print(\"Contract 2:\\n\" + str(contract2))\n",
-    "    return contract1, contract2, p1, p2, p3, p4, p5\n",
-    "\n",
-    "\n",
-    "contract1, contract2, p1, p2, p3, p4, p5 = create_example1()"
+    "    contracts = [contract1, contract2]\n",
+    "    ports = [p1, p2, p3, p4, p5]\n",
+    "    return contracts, ports"
    ]
   },
   {
@@ -913,6 +1074,28 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
+      "Contract 1:\n",
+      "InVars: [p1_a, p1_e, p2_a, p2_e]\n",
+      "OutVars:[p3_a, p3_e]\n",
+      "A: [\n",
+      "  p1_a + p2_a <= 8.0\n",
+      "]\n",
+      "G: [\n",
+      "  -p1_e - p2_e + p3_e <= 0.125\n",
+      "  p3_a <= 7.75\n",
+      "  -p1_a - p2_a + p3_a <= 0.0\n",
+      "]\n",
+      "Contract 2:\n",
+      "InVars: [p3_a, p3_e, p4_a, p4_e]\n",
+      "OutVars:[p5_a, p5_e]\n",
+      "A: [\n",
+      "  p3_a + p4_a <= 8.0\n",
+      "]\n",
+      "G: [\n",
+      "  -p3_e - p4_e + p5_e <= 0.0625\n",
+      "  p5_a <= 7.875\n",
+      "  -p3_a - p4_a + p5_a <= 0.0\n",
+      "]\n",
       "Contract Sys:\n",
       "InVars: [p1_a, p1_e, p2_a, p2_e, p4_a, p4_e]\n",
       "OutVars:[p5_a, p5_e]\n",
@@ -930,8 +1113,18 @@
     }
    ],
    "source": [
-    "contract_sys = contract1.compose(contract2)\n",
-    "print(\"Contract Sys:\\n\" + str(contract_sys))"
+    "def example_composition_two_adder() -> None:\n",
+    "    \"\"\"Example of showing composition of two adder contracts\"\"\"\n",
+    "    contracts, ports = create_example1()\n",
+    "    contract1 = contracts[0]\n",
+    "    contract2 = contracts[1]\n",
+    "    print(\"Contract 1:\\n\" + str(contract1))\n",
+    "    print(\"Contract 2:\\n\" + str(contract2))\n",
+    "    contract_sys = contract1.compose(contract2)\n",
+    "    print(\"Contract Sys:\\n\" + str(contract_sys))\n",
+    "\n",
+    "\n",
+    "example_composition_two_adder()"
    ]
   },
   {
@@ -953,8 +1146,19 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def form_contract_input(in_port):\n",
-    "    ret_contract = {}\n",
+    "def form_contract_input(in_port: PortWordLength) -> dict[str, object]:\n",
+    "    \"\"\"\n",
+    "    Create contract in dictionary form for a input port to the system.\n",
+    "\n",
+    "    The contract includes information about the bound for its output value and the bound for its maximum error\n",
+    "\n",
+    "    Args:\n",
+    "        in_port: PortWordLength: input port word length\n",
+    "\n",
+    "    Returns:\n",
+    "        The contract in dictionary form for a input port to the system.\n",
+    "    \"\"\"\n",
+    "    ret_contract: dict[str, object] = {}\n",
     "    # define input/output vars\n",
     "    ret_contract[\"input_vars\"] = []\n",
     "    ret_contract[\"output_vars\"] = [f\"{in_port.name}_a\", f\"{in_port.name}_e\"]\n",
@@ -996,7 +1200,25 @@
     }
    ],
    "source": [
-    "def test_example_1():\n",
+    "def composition_with_inputs(\n",
+    "    contracts: list[PolyhedralContract], ports: list[PortWordLength]\n",
+    ") -> PolyhedralContract | None:\n",
+    "    \"\"\"\n",
+    "    Composition of the two adder system considering input infomation\n",
+    "\n",
+    "    Args:\n",
+    "        contracts: list of PolyhedralContract for the adders\n",
+    "        ports: list of port wordlengths for the ports\n",
+    "\n",
+    "    Returns:\n",
+    "        The composition result if the composition is valid\n",
+    "    \"\"\"\n",
+    "    p1 = ports[0]\n",
+    "    p2 = ports[1]\n",
+    "    p4 = ports[3]\n",
+    "    contract1 = contracts[0]\n",
+    "    contract2 = contracts[1]\n",
+    "\n",
     "    c_p1 = form_contract_input(in_port=p1)\n",
     "    c_p2 = form_contract_input(in_port=p2)\n",
     "    c_p4 = form_contract_input(in_port=p4)\n",
@@ -1005,33 +1227,43 @@
     "    contract_p2 = PolyhedralContract.from_dict(c_p2)\n",
     "    contract_p4 = PolyhedralContract.from_dict(c_p4)\n",
     "\n",
+    "    # compose the system\n",
     "    try:\n",
     "        contract_sys = contract1.compose(contract2)\n",
+    "    except ValueError as e:\n",
+    "        print(\"Composition Error\")\n",
+    "        print(e)\n",
+    "        return None\n",
+    "    try:\n",
     "        contract_sys = contract_p1.compose(contract_sys)\n",
+    "    except ValueError as e:\n",
+    "        print(\"Composition Error\")\n",
+    "        print(e)\n",
+    "        return None\n",
+    "    try:\n",
     "        contract_sys = contract_p2.compose(contract_sys)\n",
+    "    except ValueError as e:\n",
+    "        print(\"Composition Error\")\n",
+    "        print(e)\n",
+    "        return None\n",
+    "    try:\n",
     "        contract_sys = contract_p4.compose(contract_sys)\n",
-    "        print(\"Contract Sys:\\n\" + str(contract_sys))\n",
-    "        return contract_sys\n",
     "    except ValueError as e:\n",
     "        print(\"Composition Error\")\n",
     "        print(e)\n",
+    "        return None\n",
     "\n",
+    "    print(\"Contract Sys:\\n\" + str(contract_sys))\n",
+    "    return contract_sys\n",
     "\n",
-    "contract_sys = test_example_1()"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "67da6d8f",
-   "metadata": {},
-   "source": [
-    "Pacti raises an error about the composition, saying that the guarantees are insufficient to abduce the assumption.\n",
-    "What is wrong with the composition?\n",
     "\n",
-    "The fact is that overflow could occur in the system, and thus the assumption might be violated given the input values.\n",
-    "For example, if $P_2$ is 7.75, and $P_1$ is nonzero, the addition result requires a carry that cannot be expressed in three integer bits.\n",
-    "As a result, the guarantees of the inputs are insufficient to abduce the assumption of the operation contracts."
+    "def example_composition_without_input_bounds() -> None:\n",
+    "    \"\"\"Example of composition without input bounds\"\"\"\n",
+    "    contracts, ports = create_example1()\n",
+    "    composition_with_inputs(contracts, ports)\n",
+    "\n",
+    "\n",
+    "example_composition_without_input_bounds()"
    ]
   },
   {
@@ -1067,10 +1299,19 @@
     }
    ],
    "source": [
-    "p1.value = \"10000\"\n",
-    "p2.value = \"01111\"\n",
-    "p4.value = \"0000001\"\n",
-    "contract_sys = test_example_1()"
+    "def example_composition_with_input_bounds() -> None:\n",
+    "    \"\"\"Example of composition with correct input bounds\"\"\"\n",
+    "    contracts, ports = create_example1()\n",
+    "    p1 = ports[0]\n",
+    "    p2 = ports[1]\n",
+    "    p4 = ports[3]\n",
+    "    p1.value = \"10000\"\n",
+    "    p2.value = \"01111\"\n",
+    "    p4.value = \"0000001\"\n",
+    "    composition_with_inputs(contracts, ports)\n",
+    "\n",
+    "\n",
+    "example_composition_with_input_bounds()"
    ]
   },
   {
@@ -1138,18 +1379,29 @@
     }
    ],
    "source": [
-    "def get_desired_system_contract():\n",
-    "    ret_contract = {}\n",
+    "def get_desired_system_contract() -> PolyhedralContract:\n",
+    "    \"\"\"\n",
+    "    Generate contracts for the top-level specification\n",
+    "\n",
+    "    Returns:\n",
+    "        The top-level specification contract\n",
+    "    \"\"\"\n",
+    "    ret_contract: dict[str, object] = {}\n",
     "    ret_contract[\"input_vars\"] = []\n",
     "    ret_contract[\"output_vars\"] = [\"p5_a\", \"p5_e\"]\n",
     "    ret_contract[\"assumptions\"] = []\n",
-    "    ret_contract[\"guarantees\"] = [{\"coefficients\": {f\"p5_e\": 1}, \"constant\": 0.1}]\n",
+    "    ret_contract[\"guarantees\"] = [{\"coefficients\": {\"p5_e\": 1}, \"constant\": 0.1}]\n",
     "    return PolyhedralContract.from_dict(ret_contract)\n",
     "\n",
     "\n",
-    "contract_spec = get_desired_system_contract()\n",
-    "print(\"Top Level Specification:\")\n",
-    "print(str(contract_spec))"
+    "def example_show_top_level_spec() -> None:\n",
+    "    \"\"\"Example of showing the top level specification\"\"\"\n",
+    "    contract_spec = get_desired_system_contract()\n",
+    "    print(\"Top Level Specification:\")\n",
+    "    print(str(contract_spec))\n",
+    "\n",
+    "\n",
+    "example_show_top_level_spec()"
    ]
   },
   {
@@ -1183,7 +1435,22 @@
     }
    ],
    "source": [
-    "def quotient_example1():\n",
+    "def quotient_example1() -> PolyhedralContract:\n",
+    "    \"\"\"\n",
+    "    Generate quotient based on the top-level specification and the system.\n",
+    "\n",
+    "    Returns:\n",
+    "        The quotient result, the contract for the two adder operations\n",
+    "    \"\"\"\n",
+    "    contract_spec = get_desired_system_contract()\n",
+    "    contracts, ports = create_example1()\n",
+    "    p1 = ports[0]\n",
+    "    p2 = ports[1]\n",
+    "    p4 = ports[3]\n",
+    "    p1.value = \"10000\"\n",
+    "    p2.value = \"01111\"\n",
+    "    p4.value = \"0000001\"\n",
+    "\n",
     "    c_p1 = form_contract_input(in_port=p1)\n",
     "    c_p2 = form_contract_input(in_port=p2)\n",
     "    c_p4 = form_contract_input(in_port=p4)\n",
@@ -1195,13 +1462,17 @@
     "    tmp_c1 = contract_spec.quotient(contract_p1)\n",
     "\n",
     "    tmp_c2 = tmp_c1.quotient(contract_p2)\n",
-    "    tmp_c3 = tmp_c2.quotient(contract_p4)\n",
-    "    return tmp_c3\n",
+    "    return tmp_c2.quotient(contract_p4)\n",
+    "\n",
+    "\n",
+    "def example_quotient() -> None:\n",
+    "    \"\"\"Example of showing using quotient to get contracts for the two adder operations\"\"\"\n",
+    "    quotient_ret = quotient_example1()\n",
+    "    print(\"Quotient of the Spec:\")\n",
+    "    print(str(quotient_ret))\n",
     "\n",
     "\n",
-    "quotient_ret = quotient_example1()\n",
-    "print(\"Quotient of the Spec:\")\n",
-    "print(str(quotient_ret))"
+    "example_quotient()"
    ]
   },
   {
@@ -1232,7 +1503,17 @@
     }
    ],
    "source": [
-    "def create_example1_by_p3(p3_n, p3_p):\n",
+    "def create_example1_by_p3(p3_n: int, p3_p: int) -> tuple:\n",
+    "    \"\"\"\n",
+    "    Generate the example contracts and ports for the example, given different wordlength of p3\n",
+    "\n",
+    "    Args:\n",
+    "        p3_n: the integer which defines the wordlength n for p3\n",
+    "        p3_p: the integer which defines the wordlength p for p3\n",
+    "\n",
+    "    Returns:\n",
+    "        A tuple with 2 elements. The first one is the list of contract, and the other is the list of ports\n",
+    "    \"\"\"\n",
     "    p1 = PortWordLength(n=5, p=2, name=\"p1\")\n",
     "    p2 = PortWordLength(n=5, p=3, name=\"p2\")\n",
     "    p3 = PortWordLength(n=p3_n, p=p3_p, name=\"p3\")\n",
@@ -1250,52 +1531,44 @@
     "    contract2 = PolyhedralContract.from_dict(c2)\n",
     "    # print(\"Contract 1:\\n\" + str(contract1))\n",
     "    # print(\"Contract 2:\\n\" + str(contract2))\n",
-    "    return contract1, contract2, p1, p2, p3, p4, p5\n",
-    "\n",
-    "\n",
-    "def compose_all(contract1, contract2, p1, p2, p3, p4, p5):\n",
-    "    c_p1 = form_contract_input(in_port=p1)\n",
-    "    c_p2 = form_contract_input(in_port=p2)\n",
-    "    c_p4 = form_contract_input(in_port=p4)\n",
-    "\n",
-    "    contract_p1 = PolyhedralContract.from_dict(c_p1)\n",
-    "    contract_p2 = PolyhedralContract.from_dict(c_p2)\n",
-    "    contract_p4 = PolyhedralContract.from_dict(c_p4)\n",
-    "\n",
-    "    try:\n",
-    "        contract_sys = contract1.compose(contract2)\n",
-    "        contract_sys = contract_p1.compose(contract_sys)\n",
-    "        contract_sys = contract_p2.compose(contract_sys)\n",
-    "        contract_sys = contract_p4.compose(contract_sys)\n",
-    "        print(\"Contract Sys:\\n\" + str(contract_sys))\n",
-    "        return contract_sys\n",
-    "    except ValueError as e:\n",
-    "        print(\"Composition Error\")\n",
-    "        print(e)\n",
-    "        raise ValueError(\"Composition Fails\")\n",
-    "\n",
+    "    contracts = [contract1, contract2]\n",
+    "    ports = [p1, p2, p3, p4, p5]\n",
+    "    return contracts, ports\n",
     "\n",
-    "# contract_sys = test_example_1()\n",
     "\n",
+    "def exhaustive_search() -> int:\n",
+    "    \"\"\"\n",
+    "    Perform exhaustive search on finding the minimum wordlength that satisfy the top-level specification\n",
     "\n",
-    "def exhaustive_search():\n",
+    "    Returns:\n",
+    "        The word length n for p3\n",
+    "    \"\"\"\n",
+    "    quotient_ret = quotient_example1()\n",
     "    for n in range(5, 10):\n",
     "        # print(n)\n",
     "        p = 3  # keep the same number of bits (2) before binary point\n",
-    "        contract1, contract2, p1, p2, p3, p4, p5 = create_example1_by_p3(p3_n=n, p3_p=p)\n",
+    "        contracts, ports = create_example1_by_p3(p3_n=n, p3_p=p)\n",
+    "        contract1 = contracts[0]\n",
+    "        contract2 = contracts[1]\n",
     "        try:\n",
     "            contract_sys = contract1.compose(contract2)\n",
     "            # contract_sys = compose_all(contract1, contract2, p1, p2, p3, p4, p5)\n",
     "            # print(str(contract_sys))\n",
-    "        except ValueError as e:\n",
+    "        except ValueError:\n",
     "            continue\n",
     "\n",
     "        if contract_sys.refines(quotient_ret):\n",
     "            return n\n",
+    "    return -1\n",
     "\n",
     "\n",
-    "n = exhaustive_search()\n",
-    "print(f\"Wordlength for P3 to satisfy the spec is n = {n}\")"
+    "def example_word_length_optimization() -> None:\n",
+    "    \"\"\"Example of showing word length optimization on p3 for the case study\"\"\"\n",
+    "    n = exhaustive_search()\n",
+    "    print(f\"Wordlength for P3 to satisfy the spec is n = {n}\")\n",
+    "\n",
+    "\n",
+    "example_word_length_optimization()"
    ]
   },
   {
@@ -1362,56 +1635,64 @@
     }
    ],
    "source": [
-    "in1 = PortWordLength(n=6, p=0, e=0, name=\"in1\")\n",
-    "in2 = PortWordLength(n=6, p=0, e=0, name=\"in2\")\n",
-    "in3 = PortWordLength(n=6, p=0, e=0, name=\"in3\")\n",
-    "const1 = PortWordLength(n=6, p=0, name=\"const1\")\n",
-    "const2 = PortWordLength(n=6, p=0, name=\"const2\")\n",
-    "const3 = PortWordLength(n=6, p=0, name=\"const3\")\n",
-    "mult_out1 = PortWordLength(n=6, p=0, name=\"mult_out1\")\n",
-    "mult_out2 = PortWordLength(n=6, p=0, name=\"mult_out2\")\n",
-    "mult_out3 = PortWordLength(n=6, p=0, name=\"mult_out3\")\n",
-    "add_out1 = PortWordLength(n=6, p=0, name=\"add_out1\")\n",
-    "add_out2 = PortWordLength(n=6, p=0, name=\"add_out2\")\n",
-    "\n",
-    "const1.value = float_to_bin(0.2, const1)\n",
-    "const2.value = float_to_bin(0.6, const2)\n",
-    "const3.value = float_to_bin(0.2, const3)\n",
-    "const1.e = 0.2 - const1.value_num()\n",
-    "const2.e = 0.6 - const2.value_num()\n",
-    "const3.e = 0.2 - const3.value_num()\n",
-    "\n",
-    "print(f\"truncated coefficient: 0.2 to {const1.value_num()}\")\n",
-    "print(f\"truncated coefficient: 0.6 to {const2.value_num()}\")\n",
-    "print(f\"truncated coefficient: 0.2 to {const3.value_num()}\")\n",
-    "\n",
-    "c1 = form_contract_mult_const(in_port1=in1, in_port_const=const1, out_port=mult_out1)\n",
-    "c2 = form_contract_mult_const(in_port1=in2, in_port_const=const2, out_port=mult_out2)\n",
-    "c3 = form_contract_mult_const(in_port1=in3, in_port_const=const3, out_port=mult_out3)\n",
-    "\n",
-    "ci1 = form_contract_input(in_port=in1)\n",
-    "ci2 = form_contract_input(in_port=in2)\n",
-    "ci3 = form_contract_input(in_port=in3)\n",
-    "\n",
-    "contract1 = PolyhedralContract.from_dict(c1)\n",
-    "contract2 = PolyhedralContract.from_dict(c2)\n",
-    "contract3 = PolyhedralContract.from_dict(c3)\n",
-    "contract_i1 = PolyhedralContract.from_dict(ci1)\n",
-    "contract_i2 = PolyhedralContract.from_dict(ci2)\n",
-    "contract_i3 = PolyhedralContract.from_dict(ci3)\n",
-    "c4 = form_contract_add(in_port1=mult_out1, in_port2=mult_out2, out_port=add_out1)\n",
-    "c5 = form_contract_add(in_port1=add_out1, in_port2=mult_out3, out_port=add_out2)\n",
-    "contract4 = PolyhedralContract.from_dict(c4)\n",
-    "contract5 = PolyhedralContract.from_dict(c5)\n",
-    "\n",
-    "contract_system = contract_i1.compose(contract1)\n",
-    "contract_system = contract_system.compose(contract_i2)\n",
-    "contract_system = contract_system.compose(contract2)\n",
-    "contract_system = contract_system.compose(contract_i3)\n",
-    "contract_system = contract_system.compose(contract3)\n",
-    "contract_system = contract_system.compose(contract4)\n",
-    "contract_system = contract_system.compose(contract5)\n",
-    "print(str(contract_system))"
+    "def example2_filter_design() -> None:\n",
+    "    \"\"\"Example showing the composition of the filter design\"\"\"\n",
+    "    in1 = PortWordLength(n=6, p=0, e=0, name=\"in1\")\n",
+    "    in2 = PortWordLength(n=6, p=0, e=0, name=\"in2\")\n",
+    "    in3 = PortWordLength(n=6, p=0, e=0, name=\"in3\")\n",
+    "    const1 = PortWordLength(n=6, p=0, name=\"const1\")\n",
+    "    const2 = PortWordLength(n=6, p=0, name=\"const2\")\n",
+    "    const3 = PortWordLength(n=6, p=0, name=\"const3\")\n",
+    "    mult_out1 = PortWordLength(n=6, p=0, name=\"mult_out1\")\n",
+    "    mult_out2 = PortWordLength(n=6, p=0, name=\"mult_out2\")\n",
+    "    mult_out3 = PortWordLength(n=6, p=0, name=\"mult_out3\")\n",
+    "    add_out1 = PortWordLength(n=6, p=0, name=\"add_out1\")\n",
+    "    add_out2 = PortWordLength(n=6, p=0, name=\"add_out2\")\n",
+    "\n",
+    "    a = 0.2\n",
+    "    b = 0.6\n",
+    "    c = 0.2\n",
+    "    const1.value = float_to_bin(a, const1)\n",
+    "    const2.value = float_to_bin(b, const2)\n",
+    "    const3.value = float_to_bin(c, const3)\n",
+    "    const1.e = a - const1.value_num()\n",
+    "    const2.e = b - const2.value_num()\n",
+    "    const3.e = c - const3.value_num()\n",
+    "\n",
+    "    print(f\"truncated coefficient: {a} to {const1.value_num()}\")\n",
+    "    print(f\"truncated coefficient: {b} to {const2.value_num()}\")\n",
+    "    print(f\"truncated coefficient: {c} to {const3.value_num()}\")\n",
+    "\n",
+    "    c1 = form_contract_mult_const(in_port=in1, in_port_const=const1, out_port=mult_out1)\n",
+    "    c2 = form_contract_mult_const(in_port=in2, in_port_const=const2, out_port=mult_out2)\n",
+    "    c3 = form_contract_mult_const(in_port=in3, in_port_const=const3, out_port=mult_out3)\n",
+    "\n",
+    "    ci1 = form_contract_input(in_port=in1)\n",
+    "    ci2 = form_contract_input(in_port=in2)\n",
+    "    ci3 = form_contract_input(in_port=in3)\n",
+    "\n",
+    "    contract1 = PolyhedralContract.from_dict(c1)\n",
+    "    contract2 = PolyhedralContract.from_dict(c2)\n",
+    "    contract3 = PolyhedralContract.from_dict(c3)\n",
+    "    contract_i1 = PolyhedralContract.from_dict(ci1)\n",
+    "    contract_i2 = PolyhedralContract.from_dict(ci2)\n",
+    "    contract_i3 = PolyhedralContract.from_dict(ci3)\n",
+    "    c4 = form_contract_add(in_port1=mult_out1, in_port2=mult_out2, out_port=add_out1)\n",
+    "    c5 = form_contract_add(in_port1=add_out1, in_port2=mult_out3, out_port=add_out2)\n",
+    "    contract4 = PolyhedralContract.from_dict(c4)\n",
+    "    contract5 = PolyhedralContract.from_dict(c5)\n",
+    "\n",
+    "    contract_system = contract_i1.compose(contract1)\n",
+    "    contract_system = contract_system.compose(contract_i2)\n",
+    "    contract_system = contract_system.compose(contract2)\n",
+    "    contract_system = contract_system.compose(contract_i3)\n",
+    "    contract_system = contract_system.compose(contract3)\n",
+    "    contract_system = contract_system.compose(contract4)\n",
+    "    contract_system = contract_system.compose(contract5)\n",
+    "    print(str(contract_system))\n",
+    "\n",
+    "\n",
+    "example2_filter_design()"
    ]
   },
   {
@@ -1441,51 +1722,71 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "0.06874999999999998 0.828125 0.578125 0.828125 0.921875\n"
+      "0.06874999999999998 0.828125 0.890625 0.90625 0.90625\n"
      ]
     }
    ],
    "source": [
-    "def enumerate_error():\n",
-    "    diff_max = 0\n",
-    "    a_max = 0\n",
-    "    i1_max = 0\n",
-    "    i2_max = 0\n",
-    "    i3_max = 0\n",
-    "    for i1 in range(0, 2**6):\n",
+    "def example_enumerate_error() -> None:\n",
+    "    \"\"\"Find the actual bound by enumerating the input combinations\"\"\"\n",
+    "    in1 = PortWordLength(n=6, p=0, e=0, name=\"in1\")\n",
+    "    in2 = PortWordLength(n=6, p=0, e=0, name=\"in2\")\n",
+    "    in3 = PortWordLength(n=6, p=0, e=0, name=\"in3\")\n",
+    "    const1 = PortWordLength(n=6, p=0, name=\"const1\")\n",
+    "    const2 = PortWordLength(n=6, p=0, name=\"const2\")\n",
+    "    const3 = PortWordLength(n=6, p=0, name=\"const3\")\n",
+    "    mult_out1 = PortWordLength(n=6, p=0, name=\"mult_out1\")\n",
+    "    mult_out2 = PortWordLength(n=6, p=0, name=\"mult_out2\")\n",
+    "    mult_out3 = PortWordLength(n=6, p=0, name=\"mult_out3\")\n",
+    "    add_out1 = PortWordLength(n=6, p=0, name=\"add_out1\")\n",
+    "    add_out2 = PortWordLength(n=6, p=0, name=\"add_out2\")\n",
+    "\n",
+    "    a = 0.2\n",
+    "    b = 0.6\n",
+    "    c = 0.2\n",
+    "    const1.value = float_to_bin(a, const1)\n",
+    "    const2.value = float_to_bin(b, const2)\n",
+    "    const3.value = float_to_bin(c, const3)\n",
+    "\n",
+    "    diff_max: float = 0\n",
+    "    a_max: float = 0\n",
+    "    i1_max: float = 0\n",
+    "    i2_max: float = 0\n",
+    "    i3_max: float = 0\n",
+    "    for i1, i2, i3 in itertools.combinations(range(0, 2**6), 3):\n",
     "        i1_float = i1 / 2**6\n",
     "        in1_a = float_to_bin(i1_float, in1)\n",
     "        in1.value = in1_a\n",
-    "        for i2 in range(0, 2**6):\n",
-    "            i2_float = i2 / 2**6\n",
-    "            in2_a = float_to_bin(i2_float, in2)\n",
-    "            in2.value = in2_a\n",
-    "            for i3 in range(0, 2**6):\n",
-    "                i3_float = i3 / 2**6\n",
-    "                in3_a = float_to_bin(i3_float, in3)\n",
-    "                in3.value = in3_a\n",
-    "\n",
-    "                port_mult(in1, const1, mult_out1)\n",
-    "                port_mult(in2, const2, mult_out2)\n",
-    "                port_mult(in3, const3, mult_out3)\n",
-    "                port_add(mult_out1, mult_out2, add_out1)\n",
-    "                port_add(add_out1, mult_out3, add_out2)\n",
-    "                actual_result = add_out2.value_num()\n",
-    "                ideal_result = i1_float * 0.2 + i2_float * 0.6 + i3_float * 0.2\n",
-    "                diff = ideal_result - actual_result\n",
-    "\n",
-    "                if diff > diff_max:\n",
-    "                    diff_max = diff\n",
-    "                    i1_max = i1_float\n",
-    "                    i2_max = i2_float\n",
-    "                    i3_max = i3_float\n",
-    "                if actual_result > a_max:\n",
-    "                    a_max = actual_result\n",
-    "    return diff_max, i1_max, i2_max, i3_max, a_max\n",
-    "\n",
-    "\n",
-    "diff_max, i1_max, i2_max, i3_max, a_max = enumerate_error()\n",
-    "print(diff_max, i1_max, i2_max, i3_max, a_max)"
+    "\n",
+    "        i2_float = i2 / 2**6\n",
+    "        in2_a = float_to_bin(i2_float, in2)\n",
+    "        in2.value = in2_a\n",
+    "\n",
+    "        i3_float = i3 / 2**6\n",
+    "        in3_a = float_to_bin(i3_float, in3)\n",
+    "        in3.value = in3_a\n",
+    "\n",
+    "        port_mult(in1, const1, mult_out1)\n",
+    "        port_mult(in2, const2, mult_out2)\n",
+    "        port_mult(in3, const3, mult_out3)\n",
+    "        port_add(mult_out1, mult_out2, add_out1)\n",
+    "        port_add(add_out1, mult_out3, add_out2)\n",
+    "        actual_result = add_out2.value_num()\n",
+    "        ideal_result = i1_float * a + i2_float * b + i3_float * c\n",
+    "        diff = ideal_result - actual_result\n",
+    "\n",
+    "        if diff > diff_max:\n",
+    "            diff_max = diff\n",
+    "            i1_max = i1_float\n",
+    "            i2_max = i2_float\n",
+    "            i3_max = i3_float\n",
+    "        if actual_result > a_max:\n",
+    "            a_max = actual_result\n",
+    "\n",
+    "    print(diff_max, i1_max, i2_max, i3_max, a_max)\n",
+    "\n",
+    "\n",
+    "example_enumerate_error()"
    ]
   },
   {
diff --git a/case_studies/digital_signal_processing/dsp_wl/figures/digital_data_path_example.png b/case_studies/digital_signal_processing/dsp_wl/figures/digital_data_path_example.png
deleted file mode 100644
index 5c4bf7d2..00000000
Binary files a/case_studies/digital_signal_processing/dsp_wl/figures/digital_data_path_example.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/dsp_wl/figures/digital_filter_flow.png b/case_studies/digital_signal_processing/dsp_wl/figures/digital_filter_flow.png
deleted file mode 100644
index 58472be4..00000000
Binary files a/case_studies/digital_signal_processing/dsp_wl/figures/digital_filter_flow.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/dsp_wl/figures/example1.png b/case_studies/digital_signal_processing/dsp_wl/figures/example1.png
deleted file mode 100644
index faefac93..00000000
Binary files a/case_studies/digital_signal_processing/dsp_wl/figures/example1.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/dsp_wl/figures/type_of_error.png b/case_studies/digital_signal_processing/dsp_wl/figures/type_of_error.png
deleted file mode 100644
index 6d6c20c8..00000000
Binary files a/case_studies/digital_signal_processing/dsp_wl/figures/type_of_error.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/dsp_wl_backup.ipynb b/case_studies/digital_signal_processing/dsp_wl_backup.ipynb
deleted file mode 100644
index b7246a9b..00000000
--- a/case_studies/digital_signal_processing/dsp_wl_backup.ipynb
+++ /dev/null
@@ -1,1660 +0,0 @@
-{
- "cells": [
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "37d4b21e",
-   "metadata": {},
-   "source": [
-    "## Introduction\n",
-    "In this example, we show that how gear can be applied to find the bounds of error of a digital signal processing circuit throught the fixed-number lengths of the internal calculation.\n",
-    "\n",
-    "The errors of computation of a digital signal processing circuit come from three sources: truncation error, quantization error, and inaccurate source.\n",
-    "1.  Truncation Error:\n",
-    "The truncation error is the error when a fixed-point number is converted from a longer representation to a shorter representation, which means the bits are not sufficient to represent the number, and thus the number must be truncated.\n",
-    "The truncation error occur when the result of an operation is connect to a signal with different word length.\n",
-    "2. Quantization Error:\n",
-    "The quantization error occurs when the an analog signal is converted into a digital signal, or an algorithm requires real numbers as its coefficients. As the fixed number cannot represent any real number with infinite precision. The number has to be quantized and thus are not as the exact value as the analog signal.\n",
-    "\n",
-    "3. Inaccurate Source:\n",
-    "This error comes from the measurement in the analog signal because of noise and non-ideal effect on the sensor, and could be seen as a random noise on the analog signal.\n",
-    "\n",
-    "The determination of the number of bits for fixed-point number requires tradeoff between the accuracy and the performance of the circuit.\n",
-    "Power, timing, and area of the circuit can benefit from reducing the number of bits for representation of fixed-point number as the gate count can be reduced, which results in shorter critical path length for optimization and smaller core footprint.\n",
-    "However, the accuracy of the signal processing decreases as more error is introduced in the computation and propagated to the output of the circuit.\n",
-    "\n",
-    "Therefore, in digital signal processing circuit design. Exploration of the word lengths for all fixed-point number is a crucial stage from algorithm design to circuit implementation for optimizing the circuit performance while satisfying the system requirements.\n"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "5d6da13b",
-   "metadata": {},
-   "source": [
-    "## Preliminaries\n",
-    "#### Representation of Fixed-point Number\n",
-    "\n",
-    "A word length of a fixed-point number can be described as a tuple $(n, p)$, where $n$ denotes the number of bits, and $p$ is the position of the binary point, with 0 position means the position before the most significant bit.\n",
-    "\n",
-    "For example, A fixed-point number with word length $(5,2)$ with bit value \"11011\" means the binary number $11.011$, which is equivalent to $3.375$ in decimal."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "0cc1ddb8",
-   "metadata": {},
-   "source": [
-    "First, we import some data structure for holding the wordlength, and the apis of gear."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 2,
-   "id": "aa002743",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "import numpy as np\n",
-    "from gear.terms.polyhedra.loaders import readContract\n",
-    "from tool import PortWordLength"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 3,
-   "id": "9659ebc0",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "The word length (n = 5, p = 2) of the bits \"11011\" is: \n",
-      "3.375\n"
-     ]
-    }
-   ],
-   "source": [
-    "# Definition of value_num method in PortWordLength class\n",
-    "#    def value_num(self):\n",
-    "#        return int(self.value, base=2) * 2 ** (- (self.n - self.p))\n",
-    "\n",
-    "\n",
-    "port = PortWordLength(n=5, p=2, value=\"11011\")\n",
-    "print(f'The word length (n = {port.n}, p = {port.p}) of the bits \"{port.value}\" is: ')\n",
-    "print(port.value_num())"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "78846570",
-   "metadata": {},
-   "source": [
-    "## Forming contract for capturing error of fixed-point number\n",
-    "\n",
-    "Here we introduce how to form the contract for the fixed-point number operation.\n",
-    "First, we need to model how the error is generated.\n",
-    "Then we consider the propagation of the error.\n",
-    "We formulate the contract by combining the generation of error and propagation of the error."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "af36060d",
-   "metadata": {},
-   "source": [
-    "#### Error Modeling\n",
-    "Each operation can be seen as a two-staged process.\n",
-    "First, an ideal output with certian wordlength is generated without losing any information, given the word lengths of all input ports.\n",
-    "Then the ideal output is truncated to the actual output port and could result in truncation error.\n",
-    "Therefore, the modeling of the ideal output wordlength and the truncation error is required to formulate the contract."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "f07d53c1",
-   "metadata": {},
-   "source": [
-    "#### Truncation Error Modeling\n",
-    "In the following, we details how to model the truncation error.\n",
-    "\n",
-    "##### Case 1. Binary Point Position Unchanged\n",
-    "In this case the change of word length only result in losing the lowest significant bits.\n",
-    "The maximal truncation error from the word length $(n_1, p)$ to the word length $(n_2, p)$ is $2^{p}(2^{-n_2}-2^{-n_1})$, when $n_1 > n_2$.\n",
-    "If $n_1 <= n_2$, there is no truncation and therefore the error is exactly $0$."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "dc165ff9",
-   "metadata": {},
-   "source": [
-    "The following example shows how the error is bounded:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 4,
-   "id": "cd58d386",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def truncation_error_same_position(pi, po):\n",
-    "    assert pi.p == po.p\n",
-    "    if pi.n > po.n:\n",
-    "        return 2**po.p * (2 ** (-po.n) - 2 ** (-pi.n))\n",
-    "    else:\n",
-    "        return 0\n",
-    "\n",
-    "\n",
-    "def truncate(pi, po):\n",
-    "    # separate the bits into two parts, before binary point and after binary point\n",
-    "    bits_before_point = pi.value[: pi.p]\n",
-    "    bits_after_point = pi.value[pi.p :]\n",
-    "\n",
-    "    # truncate or appending 0\n",
-    "    if po.p >= pi.p:\n",
-    "        bits_before_point = (\"0\" * (po.p - pi.p)) + bits_before_point\n",
-    "    else:\n",
-    "        bits_before_point = bits_before_point[pi.p - po.p :]\n",
-    "\n",
-    "    if po.n - po.p >= pi.n - pi.p:\n",
-    "        bits_after_point = bits_after_point + \"0\" * (po.n - po.p - pi.n + pi.p)\n",
-    "    else:\n",
-    "        bits_after_point = bits_after_point[: (po.n - po.p)]\n",
-    "\n",
-    "    # combine the both parts\n",
-    "    ret = bits_before_point + bits_after_point\n",
-    "    po.set_value(value=ret)\n",
-    "    return po.value"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 5,
-   "id": "13bee31b",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Truncation Error: \n",
-      "0.09375\n",
-      "Example Value to produce the error\n",
-      "p1 = 3.96875, bits: 1111111\n",
-      "p2 = 3.875, bits: 11111\n",
-      "p1 - p2 =  0.09375\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=2, name=\"p1\", value=\"1111111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "\n",
-    "print(\"Truncation Error: \")\n",
-    "print(truncation_error_same_position(p1, p2))\n",
-    "print(\"Example Value to produce the error\")\n",
-    "\n",
-    "truncate(p1, p2)\n",
-    "print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
-    "print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
-    "print(f\"p1 - p2 = \", p1.value_num() - p2.value_num())"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "1ba6de6f",
-   "metadata": {},
-   "source": [
-    "Then let's see what happen if the binary point position is changed\n",
-    "##### Case 2. Binary Point Position Change\n",
-    "Consider the case when $(n_1, p_1)$ to the word length $(n_2, p_2)$\n",
-    "If the binary point position is change and result in less bits before the binary point ($p_1 > p_2$), the significant bits in the initial representation will be lost. \n",
-    "Therefore, it is reasonable to assume that we know exactly the maximum number of the initial number should not set bits that cannot be included in $2^{p_2}$, which sets an assumption that the initial number must be strictly less than $2^{p_2}$.\n",
-    "Then, we can see the fixed-point number as if the those uneccesary most significant bits ($p_1 - p_2$) can be discarded.\n",
-    "$(n_1, p_1)$ can be seen as $(n_1 - p_1 + p_2, p_2)$. \n",
-    "Then it become the case one, only with the additional assumption."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "489baea4",
-   "metadata": {},
-   "source": [
-    "The following example shows how the error can be calculated."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 6,
-   "id": "478aec9d",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def truncation_error(pi, po):\n",
-    "    # remove uneccesary most significant bits\n",
-    "    # Remider: The assumption must hold!!\n",
-    "    pi_adjusted = PortWordLength(n=pi.n - pi.p + po.p, p=po.p)\n",
-    "    # return the truncation error as in case 1\n",
-    "    return truncation_error_same_position(pi=pi_adjusted, po=po)\n",
-    "\n",
-    "\n",
-    "def get_assumption_value(pi, po):\n",
-    "    if pi.p > po.p:\n",
-    "        return 2**po.p\n",
-    "    else:\n",
-    "        return float(\"inf\")  # no additional assumption needed\n",
-    "\n",
-    "\n",
-    "def check_assumption_value(pi, po):\n",
-    "    assumption_value = get_assumption_value(pi, po)\n",
-    "    print(f\"Assumption: {pi.name} < {assumption_value}\")\n",
-    "    if not pi.value_num() < assumption_value:\n",
-    "        print(\"Assumption failed, truncation of MSB occurs\")\n",
-    "        return False\n",
-    "    else:\n",
-    "        print(f\"Assumption Satisfied ({pi.name} = {pi.value_num()} < {assumption_value})\")\n",
-    "        return True"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 7,
-   "id": "9a24f2bb",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Assumption: p1 < 4\n",
-      "Assumption Satisfied (p1 = 2.4375 < 4)\n",
-      "Truncation Error: \n",
-      "0.0625\n",
-      "Example Value to produce the error\n",
-      "p1 = 2.4375, bits: 0100111\n",
-      "p2 = 2.375, bits: 10011\n",
-      "p1 - p2 =  0.0625\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "\n",
-    "assert check_assumption_value(pi=p1, po=p2)\n",
-    "\n",
-    "print(\"Truncation Error: \")\n",
-    "print(truncation_error(p1, p2))\n",
-    "print(\"Example Value to produce the error\")\n",
-    "\n",
-    "truncate(p1, p2)\n",
-    "print(f\"p1 = {p1.value_num()}, bits: {p1.value}\")\n",
-    "print(f\"p2 = {p2.value_num()}, bits: {p2.value}\")\n",
-    "print(f\"p1 - p2 = \", p1.value_num() - p2.value_num())"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "2bfb710e",
-   "metadata": {},
-   "source": [
-    "#### Ideal Output Wordlength\n",
-    "After we analyze the truncation error, the next problem is what is the wordlength before truncation?\n",
-    "Each operation requires an minimal ideal output wordlength to fully hold the resulting value without losing any information.\n",
-    "We represent the ideal output wordlength using $(n^*, p^*)$.\n",
-    "This is the wordlength truncated before sending to the output port.\n",
-    "And $(n_1, p_1), (n_2, n_2)$ denotes the wordlength of two inputs.\n",
-    "\n",
-    "The ideal output wordlength depends on the type of operation\n",
-    "Let's first examine the addition and then the multiplication"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "7397b1b8",
-   "metadata": {},
-   "source": [
-    "##### Addition\n",
-    "The following equations show the ideal output wordlnegth for addition.\n",
-    "\n",
-    "$n^* = \\max(n_1, n_2 - p_2 + p_1) + \\min(0, p_1 - p_2) + 1$,\n",
-    "\n",
-    "$p* = \\max(p_1, p_2) + 1$.\n",
-    "\n",
-    "The rationale behind the equations is to keep every bits in both inputs and add an additional one bits in the front of the output to handle the carry.\n",
-    "\n",
-    "Using the ideal output wordlength and the above truncation error. We can calculate the error induced by addition"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 8,
-   "id": "b0bc548f",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def compute_required_word_length_add(in1: PortWordLength, in2: PortWordLength) -> PortWordLength:\n",
-    "    new_n = max(in1.n, in2.n - in2.p + in1.p) - min(0, in1.p - in2.p) + 1\n",
-    "    new_p = max(in1.p, in2.p) + 1\n",
-    "    return PortWordLength(n=new_n, p=new_p)\n",
-    "\n",
-    "\n",
-    "def error_truncation_add(p1, p2, po):\n",
-    "    print(f\"Input {p1.name}: (n={p1.n}, p={p1.p})\")\n",
-    "    print(f\"Input {p2.name}: (n={p2.n}, p={p2.p})\")\n",
-    "    p_ideal = compute_required_word_length_add(in1=p1, in2=p2)\n",
-    "    print(f\"Ideal Output: (n={p_ideal.n}, p={p_ideal.p})\")\n",
-    "    print(f\"Actual Output ({po.name}): (n={po.n}, p={po.p})\")\n",
-    "\n",
-    "    assumption_value = get_assumption_value(pi=p_ideal, po=po)\n",
-    "    print(f\"Assumption: {p1.name} + {p2.name} < {assumption_value}\")\n",
-    "    return truncation_error(pi=p_ideal, po=po)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 9,
-   "id": "2f36d06c",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Input p1: (n=7, p=3)\n",
-      "Input p2: (n=5, p=2)\n",
-      "Ideal Output: (n=8, p=4)\n",
-      "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 + p2 < 8\n",
-      "Error of the addition calculation: 0.1875\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "\n",
-    "err = error_truncation_add(p1=p1, p2=p2, po=p3)\n",
-    "\n",
-    "print(f\"Error of the addition calculation: {err}\")"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "50d6572b",
-   "metadata": {},
-   "source": [
-    "\n",
-    "##### Multiplication\n",
-    "The following equations show the ideal output wordlnegth for multiplication.\n",
-    "$n^* = n_1 + n_2$,\n",
-    "$p* = p_1, p_2$."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 10,
-   "id": "dea9ad92",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def compute_required_word_length_mult(in1: PortWordLength, in2: PortWordLength) -> PortWordLength:\n",
-    "    new_n = in1.n + in2.n\n",
-    "    new_p = in1.p + in2.p\n",
-    "    return PortWordLength(n=new_n, p=new_p)\n",
-    "\n",
-    "\n",
-    "def error_truncation_mult(p1, p2, po):\n",
-    "    print(f\"Input {p1.name}: (n={p1.n}, p={p1.p})\")\n",
-    "    print(f\"Input {p2.name}: (n={p2.n}, p={p2.p})\")\n",
-    "    p_ideal = compute_required_word_length_mult(in1=p1, in2=p2)\n",
-    "    print(f\"Ideal Output: (n={p_ideal.n}, p={p_ideal.p})\")\n",
-    "    print(f\"Actual Output ({po.name}): (n={po.n}, p={po.p})\")\n",
-    "\n",
-    "    assumption_value = get_assumption_value(pi=p_ideal, po=po)\n",
-    "    print(f\"Assumption: {p1.name} * {p2.name} < {assumption_value}\")\n",
-    "    return truncation_error(pi=p_ideal, po=po)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 11,
-   "id": "ba1a5db7",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Input p1: (n=7, p=3)\n",
-      "Input p2: (n=5, p=2)\n",
-      "Ideal Output: (n=12, p=5)\n",
-      "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 * p2 < 8\n",
-      "Error of the multiplication calculation: 0.2421875\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "\n",
-    "err = error_truncation_mult(p1=p1, p2=p2, po=p3)\n",
-    "\n",
-    "print(f\"Error of the multiplication calculation: {err}\")"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "c5b0fd1f",
-   "metadata": {},
-   "source": [
-    "#### Propagation of Error\n",
-    "\n",
-    "The error $e$ already presents in a signal to the port $p$ will propagate to the final output.\n",
-    "Such error including error from the previus operation, quantization error and known inaccuracies of the input.\n",
-    "This error is independent to the error of truncation error, as truncation error compares the value of the output to the nominal value of the input signal.\n",
-    "As a result, the error can be represented as the sum of the propagation error and the truncation error in the stage: \n",
-    "\n",
-    "$e = e_p + e_t$,\n",
-    "\n",
-    "where $e_p$ is the propagtion error from inputs regardless of how many bits we have in the output, and $e_t$ denotes the truncation error that occurs due to the descrepancy between the wordlength of the ideal output and that of the actual output.\n",
-    "Thus, it is important to explore differnet word length in the circuit, as one change to the word length affect the accuracy of the output.\n",
-    "\n",
-    "Let's now see how the error is propagated in different operation"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "eee89085",
-   "metadata": {},
-   "source": [
-    "##### Propagation of Error in Addition\n",
-    "The error is exactly the sum of error from both inputs.\n",
-    "$e_p = e_1 + e_2$\n"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 12,
-   "id": "36582cb6",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def error_propagation_add(p1, p2, po):\n",
-    "    return p1.e + p2.e"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 13,
-   "id": "3719ba6f",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Input p1: (n=7, p=3)\n",
-      "Input p2: (n=5, p=2)\n",
-      "Ideal Output: (n=8, p=4)\n",
-      "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 + p2 < 8\n",
-      "Propagation error: 0.7\n",
-      "Truncation error: 0.1875\n",
-      "Error bound of the addition calculation: 0.8875\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, e=0.5, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, e=0.2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "\n",
-    "e_p = error_propagation_add(p1=p1, p2=p2, po=p3)\n",
-    "e_t = error_truncation_add(p1=p1, p2=p2, po=p3)\n",
-    "\n",
-    "err = e_p + e_t\n",
-    "print(f\"Propagation error: {e_p}\")\n",
-    "print(f\"Truncation error: {e_t}\")\n",
-    "print(f\"Error bound of the addition calculation: {err}\")"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "d25836eb",
-   "metadata": {},
-   "source": [
-    "##### Propagation of Error in Multiplication\n",
-    "The error is as follows:\n",
-    "\n",
-    "$e_p = a_1*e_2 + a_2*e_1 - e_1 * e_2$, \n",
-    "\n",
-    "where $a_1$ is the maximal possible value from input $1$, $a_2$ is the maximum possible value from input $2$.\n"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 14,
-   "id": "5613e607",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def get_actual_possible_value(in_port: PortWordLength):\n",
-    "    return (1 - (2**-in_port.n)) * 2**in_port.p\n",
-    "\n",
-    "\n",
-    "def error_propagation_mult(p1, p2, po):\n",
-    "    return p1.a * p2.e + p2.a * p1.e + p1.e * p2.e"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 15,
-   "id": "6497f4b4",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Input p1: (n=7, p=3)\n",
-      "Input p2: (n=5, p=2)\n",
-      "Ideal Output: (n=12, p=5)\n",
-      "Actual Output (p3): (n=5, p=3)\n",
-      "Assumption: p1 * p2 < 8\n",
-      "Propagation error: 2.81875\n",
-      "Truncation error: 0.2421875\n",
-      "Error bound of the multiplication calculation: 3.0609375\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, e=0.5, name=\"p1\", value=\"0100111\")\n",
-    "p2 = PortWordLength(n=5, p=2, e=0.3, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "\n",
-    "e_p = error_propagation_mult(p1=p1, p2=p2, po=p3)\n",
-    "e_t = error_truncation_mult(p1=p1, p2=p2, po=p3)\n",
-    "\n",
-    "err = e_p + e_t\n",
-    "print(f\"Propagation error: {e_p}\")\n",
-    "print(f\"Truncation error: {e_t}\")\n",
-    "print(f\"Error bound of the multiplication calculation: {err}\")"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "a90f8c44",
-   "metadata": {},
-   "source": [
-    "##### General operation\n",
-    "Using the above analysis, we now formulate the contract for different operation.\n",
-    "The error of any general operations with arity n, denoted by $f(x_1, x_2,..., x_n)$ is as follows:\n",
-    "\n",
-    "$e_p = f(x_1, x_2,..., x_n)) - f(x_1 - e_1, x_2 - e_2,..., x_n - e_n)$ "
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "84358426",
-   "metadata": {},
-   "source": [
-    "#### Contract Formulation\n",
-    "Combining the error bound modeling from propagation and truncation. We can formalte contracts for each operation.\n",
-    "A contract is a pair of assumption and guarantee, denoted by $C = (A, G)$, where $C$ represents the contract, $A$ denotes its assumption, and $G$ is the guarantee.\n",
-    "In the following, we introduce how the contract is formulated for addition and multiplication.\n",
-    "\n",
-    "##### Variables in the contract\n",
-    "To describe the behavior of the operations, we encode two variables for each port: the actual value and the error.\n",
-    "The actual value means the nominal value appears at the port instead of the ideal value we hope to use in the signal processing algorithm.\n",
-    "The error is the deviation of the nominal value to the ideal value in the signal processing algorithm.\n",
-    "\n",
-    "##### Assumption\n",
-    "The only source of assumption is the assumption in truncation to prevent losing significant bits when the binary point positions of the ideal output and the truncated output is different.\n",
-    "\n",
-    "##### Guarantee\n",
-    "The guarantee of the contract includees two part. The first part describes the error of the output port, and the second part ensures the range of the actual value in the output port."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "f6001d88",
-   "metadata": {},
-   "source": [
-    "The following functions show how we form contract for arbitrary length of input ports and output ports.\n",
-    "The \"_a\" variables are used as the variable for the actual value going through the port."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 16,
-   "id": "7ec7baf9",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def form_contract_add(in_port1, in_port2, out_port):\n",
-    "    ret_contract = {}\n",
-    "    # define input/output vars\n",
-    "    ret_contract[\"input_vars\"] = [\n",
-    "        f\"{in_port1.name}_a\",\n",
-    "        f\"{in_port1.name}_e\",\n",
-    "        f\"{in_port2.name}_a\",\n",
-    "        f\"{in_port2.name}_e\",\n",
-    "    ]\n",
-    "    ret_contract[\"output_vars\"] = [f\"{out_port.name}_a\", f\"{out_port.name}_e\"]\n",
-    "    # get assumption\n",
-    "    ideal_out_port = compute_required_word_length_add(in1=in_port1, in2=in_port2)\n",
-    "    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)\n",
-    "    # write assumption in the contract\n",
-    "    if assumption_value != float(\"inf\"):\n",
-    "        ret_contract[\"assumptions\"] = [\n",
-    "            {\"coefficients\": {f\"{in_port1.name}_a\": 1, f\"{in_port2.name}_a\": 1}, \"constant\": assumption_value}\n",
-    "        ]\n",
-    "    else:\n",
-    "        ret_contract[\"assumptions\"] = []\n",
-    "    # get guarantee\n",
-    "    e_t = truncation_error(pi=ideal_out_port, po=out_port)\n",
-    "\n",
-    "    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints\n",
-    "    ret_contract[\"guarantees\"] = [\n",
-    "        {\n",
-    "            \"coefficients\": {f\"{in_port1.name}_e\": -1, f\"{in_port2.name}_e\": -1, f\"{out_port.name}_e\": 1},\n",
-    "            \"constant\": e_t,\n",
-    "        },\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": out_port.a},\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": in_port1.a + in_port2.a},\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1, f\"{in_port1.name}_a\": -1, f\"{in_port2.name}_a\": -1}, \"constant\": 0},\n",
-    "    ]\n",
-    "    return ret_contract\n",
-    "\n",
-    "\n",
-    "def form_contract_mult_const(in_port1, in_port_const, out_port):\n",
-    "    ret_contract = {}\n",
-    "    # define input/output vars\n",
-    "    ret_contract[\"input_vars\"] = [f\"{in_port1.name}_a\", f\"{in_port1.name}_e\"]\n",
-    "    ret_contract[\"output_vars\"] = [f\"{out_port.name}_a\", f\"{out_port.name}_e\"]\n",
-    "    # get assumption\n",
-    "    ideal_out_port = compute_required_word_length_mult(in1=in_port1, in2=in_port_const)\n",
-    "    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)\n",
-    "    # write assumption in the contract\n",
-    "    if assumption_value != float(\"inf\"):\n",
-    "        print(assumption_value)\n",
-    "        ret_contract[\"assumptions\"] = [\n",
-    "            {\"coefficients\": {f\"{in_port1.name}_a\": in_port_const.a}, \"constant\": assumption_value}\n",
-    "        ]\n",
-    "    else:\n",
-    "        ret_contract[\"assumptions\"] = []\n",
-    "    # get guarantee\n",
-    "    print(ideal_out_port.to_string())\n",
-    "    e_t = truncation_error(pi=ideal_out_port, po=out_port)\n",
-    "\n",
-    "    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints\n",
-    "    ret_contract[\"guarantees\"] = [\n",
-    "        {\n",
-    "            \"coefficients\": {\n",
-    "                f\"{in_port1.name}_e\": -in_port_const.a + in_port_const.e,\n",
-    "                f\"{in_port1.name}_a\": -in_port_const.e,\n",
-    "                f\"{out_port.name}_e\": 1,\n",
-    "            },\n",
-    "            \"constant\": e_t,\n",
-    "        },\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": out_port.a},\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1}, \"constant\": in_port_const.a * in_port1.a},\n",
-    "        {\"coefficients\": {f\"{out_port.name}_a\": 1, f\"{in_port1.name}_a\": -in_port_const.a}, \"constant\": 0},\n",
-    "    ]\n",
-    "    return ret_contract"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 16,
-   "id": "a2684ccb",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "{'input_vars': ['p1_a', 'p1_e', 'p2_a', 'p2_e'], 'output_vars': ['p3_a', 'p3_e'], 'assumptions': [{'coefficients': {'p1_a': 1, 'p2_a': 1}, 'constant': 8}], 'guarantees': [{'coefficients': {'p1_e': -1, 'p2_e': -1, 'p3_e': 1}, 'constant': 0.1875}, {'coefficients': {'p3_a': 1}, 'constant': 7.75}, {'coefficients': {'p3_a': 1}, 'constant': 11.8125}, {'coefficients': {'p3_a': 1, 'p1_a': -1, 'p2_a': -1}, 'constant': 0}]}\n",
-      "InVars: [<Var p1_a>, <Var p1_e>, <Var p2_a>, <Var p2_e>]\n",
-      "OutVars:[<Var p3_a>, <Var p3_e>]\n",
-      "A: 1*p1_a + 1*p2_a <= 8\n",
-      "G: -1*p1_e + -1*p2_e + 1*p3_e <= 0.1875, 1*p3_a <= 7.75, -1*p1_a + -1*p2_a + 1*p3_a <= 0.0\n",
-      "8\n",
-      "Port: , (n, p) = (12, 5), e = 0, a = 31.9921875\n",
-      "InVars: [<Var p4_a>, <Var p4_e>]\n",
-      "OutVars:[<Var p6_a>, <Var p6_e>]\n",
-      "A: 3.375*p4_a <= 8\n",
-      "G: -0.03*p4_a + -3.345*p4_e + 1.0*p6_e <= 0.2421875, 1.0*p6_a <= 7.75, -3.375*p4_a + 1.0*p6_a <= 0.0\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1 = PortWordLength(n=7, p=3, name=\"p1\")\n",
-    "p2 = PortWordLength(n=5, p=2, name=\"p2\")\n",
-    "p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)\n",
-    "print(c1)\n",
-    "contract1 = readContract(c1)\n",
-    "print(str(contract1))\n",
-    "\n",
-    "\n",
-    "p4 = PortWordLength(n=7, p=3, name=\"p4\")\n",
-    "p5 = PortWordLength(n=5, p=2, e=0.03, value=\"11011\", name=\"p5\")  # const\n",
-    "p6 = PortWordLength(n=5, p=3, name=\"p6\")\n",
-    "c2 = form_contract_mult_const(in_port1=p4, in_port_const=p5, out_port=p6)\n",
-    "contract2 = readContract(c2)\n",
-    "print(str(contract2))"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "9756b6c2",
-   "metadata": {},
-   "source": [
-    "#### Example 1\n",
-    "Consider the following simple system with only two adder.\n",
-    "\n",
-    "![Example 1](figures/example1.png)\n",
-    "\n",
-    "We will show that how gear can be applied to get the system errors."
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "43122d15",
-   "metadata": {},
-   "source": [
-    "First, we express each port using the PortWordLength class, and then form the contracts for the operations."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 32,
-   "id": "690cd39b",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Contract 1:\n",
-      "InVars: [<Var p1_a>, <Var p1_e>, <Var p2_a>, <Var p2_e>]\n",
-      "OutVars:[<Var p3_a>, <Var p3_e>]\n",
-      "A: 1*p1_a + 1*p2_a <= 8\n",
-      "G: -1*p1_e + -1*p2_e + 1*p3_e <= 0.125, 1*p3_a <= 7.75, -1*p1_a + -1*p2_a + 1*p3_a <= 0.0\n",
-      "Contract 2:\n",
-      "InVars: [<Var p3_a>, <Var p3_e>, <Var p4_a>, <Var p4_e>]\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: 1*p3_a + 1*p4_a <= 8\n",
-      "G: -1*p3_e + -1*p4_e + 1*p5_e <= 0.0625, 1*p5_a <= 7.875, -1*p3_a + -1*p4_a + 1*p5_a <= 0.0\n"
-     ]
-    }
-   ],
-   "source": [
-    "def create_example1():\n",
-    "    p1 = PortWordLength(n=5, p=2, name=\"p1\")\n",
-    "    p2 = PortWordLength(n=5, p=3, name=\"p2\")\n",
-    "    p3 = PortWordLength(n=5, p=3, name=\"p3\")\n",
-    "    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)\n",
-    "\n",
-    "    p4 = PortWordLength(n=7, p=3, name=\"p4\")\n",
-    "    p5 = PortWordLength(n=6, p=3, name=\"p5\")\n",
-    "    c2 = form_contract_add(in_port1=p3, in_port2=p4, out_port=p5)\n",
-    "\n",
-    "    contract1 = readContract(c1)\n",
-    "    contract2 = readContract(c2)\n",
-    "    print(\"Contract 1:\\n\" + str(contract1))\n",
-    "    print(\"Contract 2:\\n\" + str(contract2))\n",
-    "    return contract1, contract2, p1, p2, p3, p4, p5\n",
-    "\n",
-    "\n",
-    "contract1, contract2, p1, p2, p3, p4, p5 = create_example1()"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "67058ba5",
-   "metadata": {},
-   "source": [
-    "We then use the composition to get the system contract."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 33,
-   "id": "bd19b796",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Contract Sys:\n",
-      "InVars: [<Var p1_a>, <Var p1_e>, <Var p2_a>, <Var p2_e>, <Var p4_a>, <Var p4_e>]\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: 1*p4_a <= 0.250000000000000, 1*p1_a + 1*p2_a <= 8\n",
-      "G: -1*p1_e + -1*p2_e + -1*p4_e + 1*p5_e <= 0.187500000000000, -1*p4_a + 1*p5_a <= 7.75, -1*p1_a + -1*p2_a + -1*p4_a + 1*p5_a <= 0.0, 1*p5_a <= 7.875\n"
-     ]
-    }
-   ],
-   "source": [
-    "contract_sys = contract1.compose(contract2)\n",
-    "print(\"Contract Sys:\\n\" + str(contract_sys))"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "07cfc78b",
-   "metadata": {},
-   "source": [
-    "The system contracts show the relation between the actual value and error bounds in input values.\n",
-    "\n",
-    "If the designers know the context how the system is used, they can includes additional contracts to constrain the input:\n",
-    "\n",
-    "First, we try an example that has no additional contraint on the input, meaning that it can take arbitrary value for the fixed-point number."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 17,
-   "id": "e166f72a",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def form_contract_input(in_port):\n",
-    "    ret_contract = {}\n",
-    "    # define input/output vars\n",
-    "    ret_contract[\"input_vars\"] = []\n",
-    "    ret_contract[\"output_vars\"] = [f\"{in_port.name}_a\", f\"{in_port.name}_e\"]\n",
-    "    # get assumption\n",
-    "    ret_contract[\"assumptions\"] = []\n",
-    "    ret_contract[\"guarantees\"] = [\n",
-    "        {\"coefficients\": {f\"{in_port.name}_a\": 1}, \"constant\": in_port.a},\n",
-    "        {\"coefficients\": {f\"{in_port.name}_a\": -1}, \"constant\": 0},\n",
-    "        {\"coefficients\": {f\"{in_port.name}_e\": 1}, \"constant\": in_port.e},\n",
-    "        {\"coefficients\": {f\"{in_port.name}_e\": -1}, \"constant\": -in_port.e},\n",
-    "    ]\n",
-    "    return ret_contract"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 34,
-   "id": "286e38e8",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Composition Error\n",
-      "The guarantees \n",
-      "1*p2_a <= 7.75, -1*p2_a <= 0.0, 1*p2_e <= 0.0, -1*p2_e <= 0.0\n",
-      "were insufficient to abduce the assumptions \n",
-      "1*p4_a <= 0.250000000000000, 1*p2_a <= 4.12500000000000\n",
-      "by eliminating the variables \n",
-      "[<Var p2_a>, <Var p2_e>, <Var p5_a>, <Var p5_e>]\n"
-     ]
-    }
-   ],
-   "source": [
-    "def test_example_1():\n",
-    "    c_p1 = form_contract_input(in_port=p1)\n",
-    "    c_p2 = form_contract_input(in_port=p2)\n",
-    "    c_p4 = form_contract_input(in_port=p4)\n",
-    "\n",
-    "    contract_p1 = readContract(c_p1)\n",
-    "    contract_p2 = readContract(c_p2)\n",
-    "    contract_p4 = readContract(c_p4)\n",
-    "\n",
-    "    try:\n",
-    "        contract_sys = contract1.compose(contract2)\n",
-    "        contract_sys = contract_p1.compose(contract_sys)\n",
-    "        contract_sys = contract_p2.compose(contract_sys)\n",
-    "        contract_sys = contract_p4.compose(contract_sys)\n",
-    "        print(\"Contract Sys:\\n\" + str(contract_sys))\n",
-    "        return contract_sys\n",
-    "    except ValueError as e:\n",
-    "        print(\"Composition Error\")\n",
-    "        print(e)\n",
-    "\n",
-    "\n",
-    "contract_sys = test_example_1()"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "67da6d8f",
-   "metadata": {},
-   "source": [
-    "The result shows that the guarantees are not sufficient to abduce the assumption.\n",
-    "\n",
-    "It can be observed easily that the input value of `p2_a` = 7.75 would violate the required assumption to prevent MSB from truncated.\n"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "303b6882",
-   "metadata": {},
-   "source": [
-    "Then we consider the case where certain constraints are known for the inputs:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 35,
-   "id": "7620625b",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Contract Sys:\n",
-      "InVars: []\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: true\n",
-      "G: 1*p5_a <= 6.00000000000000, 1*p5_e <= 0.187500000000000\n"
-     ]
-    }
-   ],
-   "source": [
-    "p1.set_value(\"10000\")\n",
-    "p2.set_value(\"01111\")\n",
-    "p4.set_value(\"0000100\")\n",
-    "contract_sys = test_example_1()"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "97fc7bd1",
-   "metadata": {},
-   "source": [
-    "Under these sets of constraints on the input, the system is compatible with the environment and thus we obtain the bounds on the actual output and the error bounds to an ideal output. "
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "b156f32a",
-   "metadata": {},
-   "source": [
-    "The contract bring us the benefits of performing more operations on the system.\n",
-    "\n",
-    "For example, we can apply the quotient to find word length for a certain signal.\n",
-    "\n",
-    "Take the system as an example again. If we want to reduce the wordlength of the intermediate signal $P_3$, we can use quotient to get the required wordlength.\n",
-    "\n",
-    "![Example 1](figures/example1.png)"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "fbd47751",
-   "metadata": {},
-   "source": [
-    "To use quotient, we starts from the system contract.\n",
-    "The system contract describes what the system looks like without knowing the underlying components.\n",
-    "Let's say we can tolerate an error of the output by 0.1 given the same input constraints for the previous refined one.\n",
-    "\n",
-    "The system contract should be like this:\n",
-    "```\n",
-    "A: True\n",
-    "G: 1*p5_a <= 6.00000000000000, 1*p5_e <= 0.1\n",
-    "```\n",
-    "\n",
-    "We can invoke contract quotient to get the desired system contract:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 38,
-   "id": "9c168335",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "InVars: []\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: true\n",
-      "G: 1*p5_a <= 6.0, 1*p5_e <= 0.10000000000000009\n"
-     ]
-    }
-   ],
-   "source": [
-    "def get_desired_system_contract():\n",
-    "    ret_contract = {}\n",
-    "    ret_contract[\"input_vars\"] = []\n",
-    "    ret_contract[\"output_vars\"] = [\"p5_a\", \"p5_e\"]\n",
-    "    ret_contract[\"assumptions\"] = []\n",
-    "    ret_contract[\"guarantees\"] = [\n",
-    "        {\"coefficients\": {f\"p5_a\": 1}, \"constant\": 6.00},\n",
-    "        {\"coefficients\": {f\"p5_e\": 1}, \"constant\": 0.1},\n",
-    "    ]\n",
-    "    return readContract(ret_contract)\n",
-    "\n",
-    "\n",
-    "contract_spec = get_desired_system_contract()\n",
-    "print(str(contract_spec))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 39,
-   "id": "874e95da",
-   "metadata": {},
-   "outputs": [
-    {
-     "ename": "ValueError",
-     "evalue": "not enough values to unpack (expected 2, got 1)",
-     "output_type": "error",
-     "traceback": [
-      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[0;31mValueError\u001b[0m                                Traceback (most recent call last)",
-      "Cell \u001b[0;32mIn[39], line 14\u001b[0m\n\u001b[1;32m     11\u001b[0m     tmp_c2 \u001b[39m=\u001b[39m tmp_c1\u001b[39m.\u001b[39mquotient(contract_p2)\n\u001b[1;32m     12\u001b[0m     tmp_c3 \u001b[39m=\u001b[39m tmp_c2\u001b[39m.\u001b[39mquotient(contract_p4)\n\u001b[0;32m---> 14\u001b[0m quotient_example1()\n",
-      "Cell \u001b[0;32mIn[39], line 10\u001b[0m, in \u001b[0;36mquotient_example1\u001b[0;34m()\u001b[0m\n\u001b[1;32m      7\u001b[0m contract_p2 \u001b[39m=\u001b[39m readContract(c_p2)\n\u001b[1;32m      8\u001b[0m contract_p4 \u001b[39m=\u001b[39m readContract(c_p4)\n\u001b[0;32m---> 10\u001b[0m tmp_c1 \u001b[39m=\u001b[39m contract_spec\u001b[39m.\u001b[39;49mquotient(contract_p1)\n\u001b[1;32m     11\u001b[0m tmp_c2 \u001b[39m=\u001b[39m tmp_c1\u001b[39m.\u001b[39mquotient(contract_p2)\n\u001b[1;32m     12\u001b[0m tmp_c3 \u001b[39m=\u001b[39m tmp_c2\u001b[39m.\u001b[39mquotient(contract_p4)\n",
-      "File \u001b[0;32m~/shengjungyu/Research/UC_Berkeley/Research/DesignSpecification/Contract/Tools/Contract/gear/src/gear/iocontract/iocontract.py:457\u001b[0m, in \u001b[0;36mIoContract.quotient\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m    455\u001b[0m assumptions \u001b[39m=\u001b[39m copy\u001b[39m.\u001b[39mdeepcopy(\u001b[39mself\u001b[39m\u001b[39m.\u001b[39ma)\n\u001b[1;32m    456\u001b[0m empty_context \u001b[39m=\u001b[39m \u001b[39mtype\u001b[39m(assumptions)(\u001b[39mlist\u001b[39m())\n\u001b[0;32m--> 457\u001b[0m \u001b[39mif\u001b[39;00m assumptions\u001b[39m.\u001b[39;49mrefines(other\u001b[39m.\u001b[39;49ma):\n\u001b[1;32m    458\u001b[0m     assumptions \u001b[39m=\u001b[39m assumptions \u001b[39m|\u001b[39m other\u001b[39m.\u001b[39mg\n\u001b[1;32m    459\u001b[0m assumptions \u001b[39m=\u001b[39m assumptions\u001b[39m.\u001b[39mdeduce_with_context(empty_context, list_union(intvars, outputvars))\n",
-      "File \u001b[0;32m~/shengjungyu/Research/UC_Berkeley/Research/DesignSpecification/Contract/Tools/Contract/gear/src/gear/terms/polyhedra/polyhedra.py:651\u001b[0m, in \u001b[0;36mPolyhedralTermList.refines\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m    649\u001b[0m variables, self_mat, self_cons, ctx_mat, ctx_cons \u001b[39m=\u001b[39m PolyhedralTermList\u001b[39m.\u001b[39mtermlist_to_polytope(\u001b[39mself\u001b[39m, other)\n\u001b[1;32m    650\u001b[0m logging\u001b[39m.\u001b[39mdebug(\u001b[39m\"\u001b[39m\u001b[39mPolytope is \u001b[39m\u001b[39m\\n\u001b[39;00m\u001b[39m%s\u001b[39;00m\u001b[39m\"\u001b[39m, self_mat)\n\u001b[0;32m--> 651\u001b[0m result \u001b[39m=\u001b[39m PolyhedralTermList\u001b[39m.\u001b[39;49mverify_polytope_containment(self_mat, self_cons, ctx_mat, ctx_cons)\n\u001b[1;32m    652\u001b[0m \u001b[39mreturn\u001b[39;00m result\n",
-      "File \u001b[0;32m~/shengjungyu/Research/UC_Berkeley/Research/DesignSpecification/Contract/Tools/Contract/gear/src/gear/terms/polyhedra/polyhedra.py:831\u001b[0m, in \u001b[0;36mPolyhedralTermList.verify_polytope_containment\u001b[0;34m(a_l, b_l, a_r, b_r)\u001b[0m\n\u001b[1;32m    816\u001b[0m \u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m    817\u001b[0m \u001b[39mSay whether a polytope is contained in another. Both are given in their\u001b[39;00m\n\u001b[1;32m    818\u001b[0m \u001b[39mH-representation.\u001b[39;00m\n\u001b[0;32m   (...)\u001b[0m\n\u001b[1;32m    828\u001b[0m \u001b[39m        Vector of H-representation of polytope on RHS of inequality.\u001b[39;00m\n\u001b[1;32m    829\u001b[0m \u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m    830\u001b[0m \u001b[39m# If the LHS is empty, it is a refinement\u001b[39;00m\n\u001b[0;32m--> 831\u001b[0m \u001b[39mif\u001b[39;00m PolyhedralTermList\u001b[39m.\u001b[39;49mis_polytope_empty(a_l, b_l):\n\u001b[1;32m    832\u001b[0m     \u001b[39mreturn\u001b[39;00m \u001b[39mTrue\u001b[39;00m\n\u001b[1;32m    833\u001b[0m \u001b[39m# If the RHS is empty, but not the LHS, not a refinement\u001b[39;00m\n",
-      "File \u001b[0;32m~/shengjungyu/Research/UC_Berkeley/Research/DesignSpecification/Contract/Tools/Contract/gear/src/gear/terms/polyhedra/polyhedra.py:881\u001b[0m, in \u001b[0;36mPolyhedralTermList.is_polytope_empty\u001b[0;34m(a, b)\u001b[0m\n\u001b[1;32m    870\u001b[0m \u001b[39m@staticmethod\u001b[39m\n\u001b[1;32m    871\u001b[0m \u001b[39mdef\u001b[39;00m \u001b[39mis_polytope_empty\u001b[39m(a: np\u001b[39m.\u001b[39marray, b: np\u001b[39m.\u001b[39marray) \u001b[39m-\u001b[39m\u001b[39m>\u001b[39m \u001b[39mbool\u001b[39m:\n\u001b[1;32m    872\u001b[0m     \u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m    873\u001b[0m \u001b[39m    Say whether a polytope is empty.\u001b[39;00m\n\u001b[1;32m    874\u001b[0m \n\u001b[0;32m   (...)\u001b[0m\n\u001b[1;32m    879\u001b[0m \u001b[39m            Vector of H-representation of polytope to verify.\u001b[39;00m\n\u001b[1;32m    880\u001b[0m \u001b[39m    \"\"\"\u001b[39;00m\n\u001b[0;32m--> 881\u001b[0m     n, m \u001b[39m=\u001b[39m a\u001b[39m.\u001b[39mshape\n\u001b[1;32m    882\u001b[0m     \u001b[39massert\u001b[39;00m n \u001b[39m==\u001b[39m \u001b[39mlen\u001b[39m(b)\n\u001b[1;32m    883\u001b[0m     \u001b[39mif\u001b[39;00m n \u001b[39m*\u001b[39m m \u001b[39m==\u001b[39m \u001b[39m0\u001b[39m:\n",
-      "\u001b[0;31mValueError\u001b[0m: not enough values to unpack (expected 2, got 1)"
-     ]
-    }
-   ],
-   "source": [
-    "def quotient_example1():\n",
-    "    c_p1 = form_contract_input(in_port=p1)\n",
-    "    c_p2 = form_contract_input(in_port=p2)\n",
-    "    c_p4 = form_contract_input(in_port=p4)\n",
-    "\n",
-    "    contract_p1 = readContract(c_p1)\n",
-    "    contract_p2 = readContract(c_p2)\n",
-    "    contract_p4 = readContract(c_p4)\n",
-    "\n",
-    "    tmp_c1 = contract_spec.quotient(contract_p1)\n",
-    "    tmp_c2 = tmp_c1.quotient(contract_p2)\n",
-    "    tmp_c3 = tmp_c2.quotient(contract_p4)\n",
-    "\n",
-    "\n",
-    "quotient_example1()"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "830ca81b",
-   "metadata": {},
-   "source": [
-    "#### Example 2: Filter Design\n",
-    "\n",
-    "We apply the contract to a simple filter that computes the moving average of the signal\n",
-    "\n",
-    "$y[n] = 0.2 \\times x[n-2] + 0.6 \\times x[n-1] + 0.2 \\times x[n] $\n",
-    "\n",
-    "And the following function perform the filter on the signal"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 23,
-   "id": "b6dbabf4",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[0.25 1.2  2.34 3.97 4.94 2.2  0.3 ]\n"
-     ]
-    }
-   ],
-   "source": [
-    "def example2_filter(x):\n",
-    "    v = np.array([0.2, 0.6, 0.2])\n",
-    "    return np.convolve(x, v)\n",
-    "\n",
-    "\n",
-    "print(example2_filter([1.25, 2.25, 3.7, 6.5, 1.5]))"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "b32d9868",
-   "metadata": {},
-   "source": [
-    "If we want to implement this filter in a digital circuit in the transpose form, "
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 24,
-   "id": "3c026d5f",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "import math\n",
-    "\n",
-    "\n",
-    "def float_to_bin(x, word_length: PortWordLength):\n",
-    "    frac_part, int_part = math.modf(x)\n",
-    "    p = word_length.p\n",
-    "    # get integer part\n",
-    "    if int_part == 0:\n",
-    "        bin_str = \"\"\n",
-    "    else:\n",
-    "        bin_str = bin(int(int_part))[2:]\n",
-    "        if len(bin_str) > p:\n",
-    "            print(\"The port unable to hold the number, significant bits lost\")\n",
-    "        else:\n",
-    "            bin_str = bin_str.zfill(p)\n",
-    "    # get fractional part\n",
-    "    frac_str = \"\"\n",
-    "    req_length = word_length.n - word_length.p\n",
-    "    while len(frac_str) != req_length:\n",
-    "        frac_part *= 2\n",
-    "        if frac_part >= 1:\n",
-    "            frac_str += \"1\"\n",
-    "            frac_part -= 1\n",
-    "        else:\n",
-    "            frac_str += \"0\"\n",
-    "\n",
-    "    return bin_str + frac_str"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 25,
-   "id": "062572a4",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Port: , (n, p) = (12, 0), e = 0, a = 0.999755859375\n",
-      "Port: , (n, p) = (12, 0), e = 0, a = 0.999755859375\n",
-      "Port: , (n, p) = (12, 0), e = 0, a = 0.999755859375\n",
-      "InVars: [<Var in1_a>, <Var in1_e>]\n",
-      "OutVars:[<Var mult_out1_a>, <Var mult_out1_e>]\n",
-      "A: true\n",
-      "G: -0.012500000000000011*in1_a + -0.175*in1_e + 1.0*mult_out1_e <= 0.015380859375, 1.0*mult_out1_a <= 0.1845703125, -0.1875*in1_a + 1.0*mult_out1_a <= 0.0\n",
-      "InVars: [<Var in1_a>, <Var in1_e>, <Var in2_a>, <Var in2_e>, <Var in3_a>, <Var in3_e>]\n",
-      "OutVars:[<Var add_out2_a>, <Var add_out2_e>]\n",
-      "A: true\n",
-      "G: 1*add_out2_e + -0.0125000000000000*in1_a + -0.175000000000000*in1_e + -0.00625000000000000*in2_a + -0.587500000000000*in2_e + -0.0125000000000000*in3_a + -0.175000000000000*in3_e <= 0.0461425781250000, 1*add_out2_a <= 0.953613281250000\n",
-      "InVars: []\n",
-      "OutVars:[<Var in1_a>, <Var in1_e>]\n",
-      "A: true\n",
-      "G: 1*in1_a <= 0.984375, -1*in1_a <= 0.0, 1*in1_e <= 0.0, -1*in1_e <= 0.0\n",
-      "InVars: []\n",
-      "OutVars:[<Var in2_a>, <Var in2_e>]\n",
-      "A: true\n",
-      "G: 1*in2_a <= 0.984375, -1*in2_a <= 0.0, 1*in2_e <= 0.0, -1*in2_e <= 0.0\n",
-      "InVars: []\n",
-      "OutVars:[<Var in3_a>, <Var in3_e>]\n",
-      "A: true\n",
-      "G: 1*in3_a <= 0.984375, -1*in3_a <= 0.0, 1*in3_e <= 0.0, -1*in3_e <= 0.0\n",
-      "InVars: [<Var in2_a>, <Var in2_e>, <Var in3_a>, <Var in3_e>]\n",
-      "OutVars:[<Var add_out2_a>, <Var add_out2_e>]\n",
-      "A: true\n",
-      "G: 1*add_out2_e + -0.00625000000000000*in2_a + -0.587500000000000*in2_e + -0.0125000000000000*in3_a + -0.175000000000000*in3_e <= 0.0584472656249999, 1*add_out2_a <= 0.953613281250000\n",
-      "InVars: []\n",
-      "OutVars:[<Var add_out2_a>, <Var add_out2_e>]\n",
-      "A: true\n",
-      "G: 1*add_out2_e <= 0.0769042968749998, 1*add_out2_a <= 0.953613281250000\n"
-     ]
-    }
-   ],
-   "source": [
-    "in1 = PortWordLength(n=6, p=0, e=0, name=\"in1\")\n",
-    "in2 = PortWordLength(n=6, p=0, e=0, name=\"in2\")\n",
-    "in3 = PortWordLength(n=6, p=0, e=0, name=\"in3\")\n",
-    "const1 = PortWordLength(n=6, p=0, name=\"const1\")\n",
-    "const2 = PortWordLength(n=6, p=0, name=\"const2\")\n",
-    "const3 = PortWordLength(n=6, p=0, name=\"const3\")\n",
-    "mult_out1 = PortWordLength(n=6, p=0, name=\"mult_out1\")\n",
-    "mult_out2 = PortWordLength(n=6, p=0, name=\"mult_out2\")\n",
-    "mult_out3 = PortWordLength(n=6, p=0, name=\"mult_out3\")\n",
-    "add_out1 = PortWordLength(n=6, p=0, name=\"add_out1\")\n",
-    "add_out2 = PortWordLength(n=6, p=0, name=\"add_out2\")\n",
-    "\n",
-    "const1.set_value(float_to_bin(0.2, const1))\n",
-    "const2.set_value(float_to_bin(0.6, const2))\n",
-    "const3.set_value(float_to_bin(0.2, const3))\n",
-    "const1.set_e(0.2 - const1.value_num())\n",
-    "const2.set_e(0.6 - const2.value_num())\n",
-    "const3.set_e(0.2 - const3.value_num())\n",
-    "\n",
-    "c1 = form_contract_mult_const(in_port1=in1, in_port_const=const1, out_port=mult_out1)\n",
-    "c2 = form_contract_mult_const(in_port1=in2, in_port_const=const2, out_port=mult_out2)\n",
-    "c3 = form_contract_mult_const(in_port1=in3, in_port_const=const3, out_port=mult_out3)\n",
-    "\n",
-    "ci1 = form_contract_input(in_port=in1)\n",
-    "ci2 = form_contract_input(in_port=in2)\n",
-    "ci3 = form_contract_input(in_port=in3)\n",
-    "\n",
-    "contract1 = readContract(c1)\n",
-    "contract2 = readContract(c2)\n",
-    "contract3 = readContract(c3)\n",
-    "print(str(contract1))\n",
-    "contract_i1 = readContract(ci1)\n",
-    "contract_i2 = readContract(ci2)\n",
-    "contract_i3 = readContract(ci3)\n",
-    "# print(str(contract1))\n",
-    "# print(str(contract2))\n",
-    "# print(str(contract3))\n",
-    "c4 = form_contract_add(in_port1=mult_out1, in_port2=mult_out2, out_port=add_out1)\n",
-    "c5 = form_contract_add(in_port1=add_out1, in_port2=mult_out3, out_port=add_out2)\n",
-    "contract4 = readContract(c4)\n",
-    "contract5 = readContract(c5)\n",
-    "# print(str(contract4))\n",
-    "# print(str(contract5))\n",
-    "contract_system = contract1.compose(contract2)\n",
-    "contract_system = contract_system.compose(contract3)\n",
-    "contract_system = contract_system.compose(contract4)\n",
-    "contract_system = contract_system.compose(contract5)\n",
-    "print(str(contract_system))\n",
-    "contract_system = contract_i1.compose(contract_system)\n",
-    "print(str(contract_i1))\n",
-    "print(str(contract_i2))\n",
-    "print(str(contract_i3))\n",
-    "print(str(contract_system))\n",
-    "contract_system = contract_i2.compose(contract_system)\n",
-    "contract_system = contract_i3.compose(contract_system)\n",
-    "print(str(contract_system))"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "6a546be1",
-   "metadata": {},
-   "source": [
-    "The result shows that we can get an upper bound on the error of the output `add_out_e` is bounded by about 0.07690.\n",
-    "And this is the extreme case when the input is the following case:\n",
-    "\n",
-    "Note that this is always an upper bound to the actual errors as we abstract the calculation and considers the worse case truncation error for each operation.\n",
-    "\n",
-    "If the obtained error is smaller than the specification, we can rest assure that the design already satisfy the goal and we can either submit the design or change some wordlength and see if we can use smaller wordlength to achieve the same specification.\n",
-    "\n",
-    "If the obtained error is larger than the specification, the level of abstraction is not sufficient to prove the correctness of the design.\n",
-    "Refinement of the error model or extensive verfication is therefore needed to verify the design.\n",
-    " "
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "cd0558b3",
-   "metadata": {},
-   "source": [
-    "To see the actual errors for this specific case, we can enumerate all input sequence.\n"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 26,
-   "id": "4e0031d7",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "for i1 in range(0, 2**6):\n",
-    "    in1_a = float_to_bin(i1 / 2**6, in1)\n",
-    "    in1.set_value(in1_a)\n",
-    "    for i2 in range(0, 2**6):\n",
-    "        in2_a = float_to_bin(i2 / 2**6, in2)\n",
-    "        in2.set_value(in2_a)\n",
-    "        for i3 in range(0, 2**6):\n",
-    "            in3_a = float_to_bin(i3 / 2**6, in3)\n",
-    "            in3.set_value(in3_a)\n",
-    "\n",
-    "            in1.value_num() * const1.value_num()\n",
-    "            in2.value_num() * const2.value_num()\n",
-    "            in3.value_num() * const3.value_num()"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 27,
-   "id": "29ddbff5",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "'0b111110000001'"
-      ]
-     },
-     "execution_count": 27,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "bin(int(0.984375 * 2**6) * int(0.984375 * 2**6))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 28,
-   "id": "f82bde73",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "InVars: []\n",
-      "OutVars:[<Var p3_e>]\n",
-      "A: true\n",
-      "G: 1*p3_e <= 10.1000000000000\n"
-     ]
-    }
-   ],
-   "source": [
-    "# exp\n",
-    "c1 = {\n",
-    "    \"input_vars\": [],\n",
-    "    \"output_vars\": [\"p2_a\", \"t2\"],\n",
-    "    \"assumptions\": [],\n",
-    "    \"guarantees\": [\n",
-    "        {\"coefficients\": {\"p2_a\": 1}, \"constant\": 0.1},\n",
-    "        {\"coefficients\": {\"p2_a\": -1}, \"constant\": 0.0},\n",
-    "        {\"coefficients\": {\"t2\": 1}, \"constant\": 0.1},\n",
-    "        {\"coefficients\": {\"t2\": -1}, \"constant\": 0.0},\n",
-    "    ],\n",
-    "}\n",
-    "\n",
-    "c2 = {\n",
-    "    \"input_vars\": [\"p2_a\", \"t2\"],\n",
-    "    \"output_vars\": [\"p3_e\"],\n",
-    "    \"assumptions\": [],\n",
-    "    \"guarantees\": [{\"coefficients\": {\"p3_e\": 1, \"p2_a\": 1, \"t2\": -1}, \"constant\": 10}],\n",
-    "}\n",
-    "\n",
-    "contract1 = readContract(c1)\n",
-    "contract2 = readContract(c2)\n",
-    "system = contract1.compose(contract2)\n",
-    "print(str(system))"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "9e4c7c7a",
-   "metadata": {},
-   "source": [
-    "#### Example 3: Fast-Fourier Transform (FFT) Cooley-Tucker Algorthm\n",
-    "\n",
-    "We applied the contract on the FFT Cooley-Tucker Algorithm of the Radix 2 decimation-in-time form.\n",
-    "The following function implements the eight-point FFT."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 29,
-   "id": "a120182a",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[1.+0.j 1.+0.j 1.+0.j 1.+0.j 1.+0.j 1.+0.j 1.+0.j 2.+0.j]\n",
-      "[ 9.00000000e+00+0.j          7.07106781e-01+0.70710678j\n",
-      " -6.12323400e-17+1.j         -7.07106781e-01+0.70710678j\n",
-      " -1.00000000e+00+0.j         -7.07106781e-01-0.70710678j\n",
-      "  6.12323400e-17-1.j          7.07106781e-01-0.70710678j]\n",
-      "[ 9.        +0.j          0.70710678+0.70710678j  0.        +1.j\n",
-      " -0.70710678+0.70710678j -1.        +0.j         -0.70710678-0.70710678j\n",
-      "  0.        -1.j          0.70710678-0.70710678j]\n",
-      "[1.+0.j 1.+0.j]\n"
-     ]
-    }
-   ],
-   "source": [
-    "import numpy as np\n",
-    "\n",
-    "\n",
-    "def fft_8points(x):\n",
-    "    s1 = np.zeros(x.shape, dtype=complex)\n",
-    "    W0 = np.exp(-2j * np.pi / 8 * 0)\n",
-    "    W1 = np.exp(-2j * np.pi / 8 * 1)\n",
-    "    W2 = np.exp(-2j * np.pi / 8 * 2)\n",
-    "    W3 = np.exp(-2j * np.pi / 8 * 3)\n",
-    "    # print(W0, W1, W2, W3)\n",
-    "\n",
-    "    s1[0] = x[0] + W0 * x[4]\n",
-    "    s1[1] = x[0] - W0 * x[4]\n",
-    "    s1[2] = x[2] + W0 * x[6]\n",
-    "    s1[3] = x[2] - W0 * x[6]\n",
-    "    s1[4] = x[1] + W0 * x[5]\n",
-    "    s1[5] = x[1] - W0 * x[5]\n",
-    "    s1[6] = x[3] + W0 * x[7]\n",
-    "    s1[7] = x[3] - W0 * x[7]\n",
-    "\n",
-    "    s2 = np.zeros(x.shape, dtype=complex)\n",
-    "    s2[0] = s1[0] + W0 * s1[2]\n",
-    "    s2[2] = s1[0] - W0 * s1[2]\n",
-    "    s2[1] = s1[1] + W2 * s1[3]\n",
-    "    s2[3] = s1[1] - W2 * s1[3]\n",
-    "    s2[4] = s1[4] + W0 * s1[6]\n",
-    "    s2[6] = s1[4] - W0 * s1[6]\n",
-    "    s2[5] = s1[5] + W2 * s1[7]\n",
-    "    s2[7] = s1[5] - W2 * s1[7]\n",
-    "\n",
-    "    s3 = np.zeros(x.shape, dtype=complex)\n",
-    "    s3[0] = s2[0] + W0 * s2[4]\n",
-    "    s3[4] = s2[0] - W0 * s2[4]\n",
-    "    s3[1] = s2[1] + W1 * s2[5]\n",
-    "    s3[5] = s2[1] - W1 * s2[5]\n",
-    "    s3[2] = s2[2] + W2 * s2[6]\n",
-    "    s3[6] = s2[2] - W2 * s2[6]\n",
-    "    s3[3] = s2[3] + W3 * s2[7]\n",
-    "    s3[7] = s2[3] - W3 * s2[7]\n",
-    "\n",
-    "    return s3\n",
-    "\n",
-    "\n",
-    "t = np.arange(8)\n",
-    "# x = np.sin(t * 2 * np.pi / 8)\n",
-    "\n",
-    "x = np.array([1, 1, 1, 1, 1, 1, 1, 2], dtype=complex)\n",
-    "print(x)\n",
-    "print(fft_8points(x=x))\n",
-    "print(np.fft.fft(x))\n",
-    "\n",
-    "x = np.array([1, 0], dtype=complex)\n",
-    "print(np.fft.fft(x))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 30,
-   "id": "3fbe38d7",
-   "metadata": {},
-   "outputs": [
-    {
-     "ename": "AssertionError",
-     "evalue": "",
-     "output_type": "error",
-     "traceback": [
-      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[0;31mAssertionError\u001b[0m                            Traceback (most recent call last)",
-      "Cell \u001b[0;32mIn[30], line 2\u001b[0m\n\u001b[1;32m      1\u001b[0m p4 \u001b[39m=\u001b[39m PortWordLength(n\u001b[39m=\u001b[39m\u001b[39m8\u001b[39m, p\u001b[39m=\u001b[39m\u001b[39m3\u001b[39m, name\u001b[39m=\u001b[39m\u001b[39m\"\u001b[39m\u001b[39mp4\u001b[39m\u001b[39m\"\u001b[39m)\n\u001b[0;32m----> 2\u001b[0m p5 \u001b[39m=\u001b[39m PortWordLength(n\u001b[39m=\u001b[39;49m\u001b[39m8\u001b[39;49m, p\u001b[39m=\u001b[39;49m\u001b[39m3\u001b[39;49m, e\u001b[39m=\u001b[39;49m\u001b[39m0.03\u001b[39;49m, value\u001b[39m=\u001b[39;49m\u001b[39m\"\u001b[39;49m\u001b[39m11011\u001b[39;49m\u001b[39m\"\u001b[39;49m, name\u001b[39m=\u001b[39;49m\u001b[39m\"\u001b[39;49m\u001b[39mp5\u001b[39;49m\u001b[39m\"\u001b[39;49m) \u001b[39m# const\u001b[39;00m\n\u001b[1;32m      3\u001b[0m p6 \u001b[39m=\u001b[39m PortWordLength(n\u001b[39m=\u001b[39m\u001b[39m8\u001b[39m, p\u001b[39m=\u001b[39m\u001b[39m3\u001b[39m, name\u001b[39m=\u001b[39m\u001b[39m\"\u001b[39m\u001b[39mp6\u001b[39m\u001b[39m\"\u001b[39m)\n",
-      "File \u001b[0;32m~/shengjungyu/Research/UC_Berkeley/Research/DesignSpecification/Contract/Tools/Contract/gear/case_studies/digital_signal_processing/tool.py:14\u001b[0m, in \u001b[0;36mPortWordLength.__init__\u001b[0;34m(self, n, p, e, a, name, value)\u001b[0m\n\u001b[1;32m     12\u001b[0m \u001b[39mif\u001b[39;00m value \u001b[39mis\u001b[39;00m \u001b[39mnot\u001b[39;00m \u001b[39mNone\u001b[39;00m:\n\u001b[1;32m     13\u001b[0m     \u001b[39massert\u001b[39;00m(\u001b[39misinstance\u001b[39m(value, \u001b[39mstr\u001b[39m))\n\u001b[0;32m---> 14\u001b[0m     \u001b[39massert\u001b[39;00m(\u001b[39mlen\u001b[39m(value) \u001b[39m==\u001b[39m n)\n\u001b[1;32m     15\u001b[0m \u001b[39mself\u001b[39m\u001b[39m.\u001b[39m_value \u001b[39m=\u001b[39m value\n",
-      "\u001b[0;31mAssertionError\u001b[0m: "
-     ]
-    }
-   ],
-   "source": [
-    "p4 = PortWordLength(n=8, p=3, name=\"p4\")\n",
-    "p5 = PortWordLength(n=8, p=3, e=0.03, value=\"11011\", name=\"p5\")  # const\n",
-    "p6 = PortWordLength(n=8, p=3, name=\"p6\")"
-   ]
-  },
-  {
-   "attachments": {},
-   "cell_type": "markdown",
-   "id": "2ca6a125",
-   "metadata": {},
-   "source": [
-    "### Problem with Composition Order\n",
-    "The order matters and create too restrictive bounds."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 18,
-   "id": "992aafd0",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Contract Sys:\n",
-      "InVars: []\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: true\n",
-      "G: 1*p5_a <= 3.00000000000000, 1*p5_e <= 0.187500000000000\n",
-      "InVars: []\n",
-      "OutVars:[<Var p5_a>, <Var p5_e>]\n",
-      "A: true\n",
-      "G: 1*p5_a <= 3.00000000000000, 1*p5_e <= 0.187500000000000\n"
-     ]
-    }
-   ],
-   "source": [
-    "def create_example1_by_p3(p3_n, p3_p):\n",
-    "    p1 = PortWordLength(n=5, p=2, name=\"p1\")\n",
-    "    p2 = PortWordLength(n=5, p=3, name=\"p2\")\n",
-    "    p3 = PortWordLength(n=p3_n, p=p3_p, name=\"p3\")\n",
-    "    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)\n",
-    "\n",
-    "    p4 = PortWordLength(n=7, p=3, name=\"p4\")\n",
-    "    p5 = PortWordLength(n=6, p=3, name=\"p5\")\n",
-    "    c2 = form_contract_add(in_port1=p3, in_port2=p4, out_port=p5)\n",
-    "\n",
-    "    p1.set_value(\"10000\")\n",
-    "    p2.set_value(\"00001\")\n",
-    "    p4.set_value(\"0001100\")\n",
-    "\n",
-    "    contract1 = readContract(c1)\n",
-    "    contract2 = readContract(c2)\n",
-    "    # print(\"Contract 1:\\n\" + str(contract1))\n",
-    "    # print(\"Contract 2:\\n\" + str(contract2))\n",
-    "    return contract1, contract2, p1, p2, p3, p4, p5\n",
-    "\n",
-    "\n",
-    "def compose_order1(contract1, contract2, p1, p2, p3, p4, p5):\n",
-    "    c_p1 = form_contract_input(in_port=p1)\n",
-    "    c_p2 = form_contract_input(in_port=p2)\n",
-    "    c_p4 = form_contract_input(in_port=p4)\n",
-    "\n",
-    "    contract_p1 = readContract(c_p1)\n",
-    "    contract_p2 = readContract(c_p2)\n",
-    "    contract_p4 = readContract(c_p4)\n",
-    "\n",
-    "    try:\n",
-    "        contract_sys = contract_p1.compose(contract1)\n",
-    "        contract_sys = contract_p2.compose(contract_sys)\n",
-    "        contract_sys = contract_sys.compose(contract2)\n",
-    "        contract_sys = contract_p4.compose(contract_sys)\n",
-    "        print(\"Contract Sys:\\n\" + str(contract_sys))\n",
-    "        return contract_sys\n",
-    "    except ValueError as e:\n",
-    "        print(\"Composition Error\")\n",
-    "        print(e)\n",
-    "        raise ValueError(\"Composition Fails\")\n",
-    "\n",
-    "\n",
-    "def compose_order2(contract1, contract2, p1, p2, p3, p4, p5):\n",
-    "    c_p1 = form_contract_input(in_port=p1)\n",
-    "    c_p2 = form_contract_input(in_port=p2)\n",
-    "    c_p4 = form_contract_input(in_port=p4)\n",
-    "\n",
-    "    contract_p1 = readContract(c_p1)\n",
-    "    contract_p2 = readContract(c_p2)\n",
-    "    contract_p4 = readContract(c_p4)\n",
-    "\n",
-    "    try:\n",
-    "        contract_sys = contract1.compose(contract2)\n",
-    "        contract_sys = contract_p2.compose(contract_sys)\n",
-    "        contract_sys = contract_sys.compose(contract2)\n",
-    "        contract_sys = contract_p4.compose(contract_sys)\n",
-    "        print(\"Contract Sys:\\n\" + str(contract_sys))\n",
-    "        return contract_sys\n",
-    "    except ValueError as e:\n",
-    "        print(\"Composition Error\")\n",
-    "        print(e)\n",
-    "        raise ValueError(\"Composition Fails\")\n",
-    "\n",
-    "\n",
-    "contract1, contract2, p1, p2, p3, p4, p5 = create_example1_by_p3(p3_n=5, p3_p=3)\n",
-    "contract_sys = compose_order1(contract1, contract2, p1, p2, p3, p4, p5)\n",
-    "print(str(contract_sys))"
-   ]
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "EE227cfinal",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.10.4 | packaged by conda-forge | (main, Mar 24 2022, 17:45:10) [Clang 12.0.1 ]"
-  },
-  "vscode": {
-   "interpreter": {
-    "hash": "aed908b208154c5d14a5b26ec5e9587107b2c07b4bd6e6f91c00253c94cfc0d3"
-   }
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}
diff --git a/case_studies/digital_signal_processing/figures/digital_data_path_example.png b/case_studies/digital_signal_processing/figures/digital_data_path_example.png
deleted file mode 100644
index 5c4bf7d2..00000000
Binary files a/case_studies/digital_signal_processing/figures/digital_data_path_example.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/figures/digital_filter_flow.png b/case_studies/digital_signal_processing/figures/digital_filter_flow.png
deleted file mode 100644
index 58472be4..00000000
Binary files a/case_studies/digital_signal_processing/figures/digital_filter_flow.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/figures/example1.png b/case_studies/digital_signal_processing/figures/example1.png
deleted file mode 100644
index faefac93..00000000
Binary files a/case_studies/digital_signal_processing/figures/example1.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/figures/type_of_error.png b/case_studies/digital_signal_processing/figures/type_of_error.png
deleted file mode 100644
index 6d6c20c8..00000000
Binary files a/case_studies/digital_signal_processing/figures/type_of_error.png and /dev/null differ
diff --git a/case_studies/digital_signal_processing/tool.py b/case_studies/digital_signal_processing/tool.py
index 5a9940e8..9778dee7 100644
--- a/case_studies/digital_signal_processing/tool.py
+++ b/case_studies/digital_signal_processing/tool.py
@@ -76,6 +76,16 @@ def e(self) -> float:
         """
         return self._e
 
+    @e.setter
+    def e(self, val: float) -> None:
+        """
+        Set known source error to the port
+
+        Args:
+            val: The known error source to the port
+        """
+        self._e = val
+
     @property
     def name(self) -> str:
         """
@@ -86,6 +96,16 @@ def name(self) -> str:
         """
         return self._name
 
+    @name.setter
+    def name(self, val: str) -> None:
+        """
+        Set name of the port
+
+        Args:
+            val: The name of the port
+        """
+        self._name = val
+
     @property
     def value(self) -> str | None:
         """
@@ -97,34 +117,14 @@ def value(self) -> str | None:
         return self._value
 
     @value.setter
-    def value(self, value: str) -> None:
+    def value(self, val: str) -> None:
         """
         Set constant value for the port
 
         Args:
-            value: the constant value to be set for the port
-        """
-        self._value = value
-
-    @e.setter
-    def e(self, e: float) -> None:
-        """
-        Set known source error to the port
-
-        Args:
-            e: The known error source to the port
-        """
-        self._e = e
-
-    @name.setter
-    def name(self, name: str) -> None:
-        """
-        Set name of the port
-
-        Args:
-            name: The name of the port
+            val: the constant value to be set for the port
         """
-        self._name = name
+        self._value = val
 
     def to_string(self) -> str:
         """


Test patch:
diff --git a/tests/test_data/polyhedral_contracts/test_composition_failure_dspexample1failed.json b/tests/test_data/polyhedral_contracts/test_composition_failure_dspexample1failed.json
new file mode 100644
index 00000000..b54ab3cd
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_failure_dspexample1failed.json
@@ -0,0 +1,45 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p2_a",
+        "p2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p2_a <= 7.75",
+        "-p2_a <= 0.0",
+        "p2_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p2_a",
+        "p2_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25",
+        "p2_a <= 4.125"
+      ],
+      "guarantees": [
+        "-p2_a - p4_a + p5_a <= 3.875",
+        "-p2_e - p4_e + p5_e <= 0.1875",
+        "-p4_a + p5_a <= 7.75",
+        "p5_a <= 7.875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition1.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition1.json
new file mode 100644
index 00000000..f6165cdd
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition1.json
@@ -0,0 +1,78 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e",
+        "p2_a",
+        "p2_e"
+      ],
+      "output_vars": [
+        "p3_a",
+        "p3_e"
+      ],
+      "assumptions": [
+        "p1_a + p2_a <= 8.0"
+      ],
+      "guarantees": [
+        "-p1_e - p2_e + p3_e <= 0.125",
+        "p3_a <= 7.75",
+        "-p1_a - p2_a + p3_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p3_a",
+        "p3_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p3_a + p4_a <= 8.0"
+      ],
+      "guarantees": [
+        "-p3_e - p4_e + p5_e <= 0.0625",
+        "p5_a <= 7.875",
+        "-p3_a - p4_a + p5_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contractsys",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e",
+        "p2_a",
+        "p2_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25",
+        "p1_a + p2_a <= 8.0"
+      ],
+      "guarantees": [
+        "-p1_e - p2_e - p4_e + p5_e <= 0.1875",
+        "-p4_a + p5_a <= 7.75",
+        "-p1_a - p2_a - p4_a + p5_a <= 0.0",
+        "p5_a <= 7.875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition2.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition2.json
new file mode 100644
index 00000000..b79a7e66
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition2.json
@@ -0,0 +1,73 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p1_a",
+        "p1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p1_a <= 2.0",
+        "-p1_a <= 0.0",
+        "p1_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e",
+        "p2_a",
+        "p2_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25",
+        "p1_a + p2_a <= 8.0"
+      ],
+      "guarantees": [
+        "-p1_e - p2_e - p4_e + p5_e <= 0.1875",
+        "-p4_a + p5_a <= 7.75",
+        "-p1_a - p2_a - p4_a + p5_a <= 0.0",
+        "p5_a <= 7.875"
+      ]
+    }
+  },
+  {
+    "name": "contractsys",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p2_a",
+        "p2_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25",
+        "p2_a <= 6.0"
+      ],
+      "guarantees": [
+        "-p2_a - p4_a + p5_a <= 2.0",
+        "-p2_e - p4_e + p5_e <= 0.1875",
+        "-p4_a + p5_a <= 7.75",
+        "p5_a <= 7.875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition3.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition3.json
new file mode 100644
index 00000000..047cd557
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition3.json
@@ -0,0 +1,66 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p2_a",
+        "p2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p2_a <= 3.75",
+        "-p2_a <= 0.0",
+        "p2_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p2_a",
+        "p2_e",
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25",
+        "p2_a <= 6.0"
+      ],
+      "guarantees": [
+        "-p2_a - p4_a + p5_a <= 2.0",
+        "-p2_e - p4_e + p5_e <= 0.1875",
+        "-p4_a + p5_a <= 7.75",
+        "p5_a <= 7.875"
+      ]
+    }
+  },
+  {
+    "name": "contractsys",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25"
+      ],
+      "guarantees": [
+        "-p4_a + p5_a <= 5.75",
+        "-p4_e + p5_e <= 0.1875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition4.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition4.json
new file mode 100644
index 00000000..4f0a5c90
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample1composition4.json
@@ -0,0 +1,56 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p4_a",
+        "p4_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p4_a <= 0.0625",
+        "-p4_a <= 0.0",
+        "p4_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p4_a",
+        "p4_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p4_a <= 0.25"
+      ],
+      "guarantees": [
+        "-p4_a + p5_a <= 5.75",
+        "-p4_e + p5_e <= 0.1875"
+      ]
+    }
+  },
+  {
+    "name": "contractsys",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p5_a <= 5.8125",
+        "p5_e <= 0.1875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition10.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition10.json
new file mode 100644
index 00000000..c68e5a8d
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition10.json
@@ -0,0 +1,70 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e",
+        "mult_out3_a",
+        "mult_out3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625",
+        "mult_out3_e <= 0.02768554687499991",
+        "mult_out3_a <= 0.1845703125"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e"
+      ],
+      "output_vars": [
+        "add_out1_a",
+        "add_out1_e"
+      ],
+      "assumptions": [
+        "mult_out1_a + mult_out2_a <= 1.0"
+      ],
+      "guarantees": [
+        "add_out1_e - mult_out1_e - mult_out2_e <= 0.0",
+        "add_out1_a <= 0.984375",
+        "add_out1_a - mult_out1_a - mult_out2_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out3_a",
+        "mult_out3_e",
+        "add_out1_a",
+        "add_out1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out3_e <= 0.02768554687499991",
+        "mult_out3_a <= 0.1845703125",
+        "add_out1_e <= 0.04921875000000009",
+        "add_out1_a <= 0.76904296875"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition11.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition11.json
new file mode 100644
index 00000000..05c59de0
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition11.json
@@ -0,0 +1,62 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out3_a",
+        "mult_out3_e",
+        "add_out1_a",
+        "add_out1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out3_e <= 0.02768554687499991",
+        "mult_out3_a <= 0.1845703125",
+        "add_out1_e <= 0.04921875000000009",
+        "add_out1_a <= 0.76904296875"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "add_out1_a",
+        "add_out1_e",
+        "mult_out3_a",
+        "mult_out3_e"
+      ],
+      "output_vars": [
+        "add_out2_a",
+        "add_out2_e"
+      ],
+      "assumptions": [
+        "add_out1_a + mult_out3_a <= 1.0"
+      ],
+      "guarantees": [
+        "-add_out1_e + add_out2_e - mult_out3_e <= 0.0",
+        "add_out2_a <= 0.984375",
+        "-add_out1_a + add_out2_a - mult_out3_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "add_out2_a",
+        "add_out2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "add_out2_e <= 0.076904296875",
+        "add_out2_a <= 0.95361328125"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition5.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition5.json
new file mode 100644
index 00000000..22f05a6d
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition5.json
@@ -0,0 +1,55 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "in1_a",
+        "in1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "in1_a <= 0.984375",
+        "-in1_a <= 0.0",
+        "in1_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "in1_a",
+        "in1_e"
+      ],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "-0.012500000000000011 in1_a - 0.175 in1_e + mult_out1_e <= 0.015380859375",
+        "mult_out1_a <= 0.984375",
+        "-0.1875 in1_a + mult_out1_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition6.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition6.json
new file mode 100644
index 00000000..4436412f
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition6.json
@@ -0,0 +1,56 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "in2_a",
+        "in2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "in2_a <= 0.984375",
+        "-in2_a <= 0.0",
+        "in2_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "in2_a",
+        "in2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "in2_a <= 0.984375",
+        "-in2_a <= 0.0",
+        "in2_e = 0.0"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition7.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition7.json
new file mode 100644
index 00000000..6644cbb1
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition7.json
@@ -0,0 +1,63 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "in2_a",
+        "in2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "in2_a <= 0.984375",
+        "-in2_a <= 0.0",
+        "in2_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "in2_a",
+        "in2_e"
+      ],
+      "output_vars": [
+        "mult_out2_a",
+        "mult_out2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "-0.006249999999999978 in2_a - 0.5875 in2_e + mult_out2_e <= 0.015380859375",
+        "mult_out2_a <= 0.984375",
+        "-0.59375 in2_a + mult_out2_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition8.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition8.json
new file mode 100644
index 00000000..3400729d
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition8.json
@@ -0,0 +1,64 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "in3_a",
+        "in3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "in3_a <= 0.984375",
+        "-in3_a <= 0.0",
+        "in3_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e",
+        "in3_a",
+        "in3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625",
+        "in3_a <= 0.984375",
+        "-in3_a <= 0.0",
+        "in3_e = 0.0"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition9.json b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition9.json
new file mode 100644
index 00000000..561369d8
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_composition_success_dspexample2composition9.json
@@ -0,0 +1,71 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e",
+        "in3_a",
+        "in3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625",
+        "in3_a <= 0.984375",
+        "-in3_a <= 0.0",
+        "in3_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "in3_a",
+        "in3_e"
+      ],
+      "output_vars": [
+        "mult_out3_a",
+        "mult_out3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "-0.012500000000000011 in3_a - 0.175 in3_e + mult_out3_e <= 0.015380859375",
+        "mult_out3_a <= 0.984375",
+        "-0.1875 in3_a + mult_out3_a <= 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "mult_out1_a",
+        "mult_out1_e",
+        "mult_out2_a",
+        "mult_out2_e",
+        "mult_out3_a",
+        "mult_out3_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "mult_out1_e <= 0.02768554687499991",
+        "mult_out1_a <= 0.1845703125",
+        "mult_out2_e <= 0.021533203124999956",
+        "mult_out2_a <= 0.58447265625",
+        "mult_out3_e <= 0.02768554687499991",
+        "mult_out3_a <= 0.1845703125"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient1.json b/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient1.json
new file mode 100644
index 00000000..ec134b28
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient1.json
@@ -0,0 +1,56 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p5_e <= 0.1"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p1_a",
+        "p1_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p1_a <= 2.0",
+        "-p1_a <= 0.0",
+        "p1_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p1_a <= 2.0",
+        "-p1_a <= 0.0",
+        "p1_e = 0.0"
+      ],
+      "guarantees": [
+        "p5_e <= 0.10000000000000009"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient2.json b/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient2.json
new file mode 100644
index 00000000..5749c51e
--- /dev/null
+++ b/tests/test_data/polyhedral_contracts/test_quotient_success_dspexample1quotient2.json
@@ -0,0 +1,68 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p1_a <= 2.0",
+        "-p1_a <= 0.0",
+        "p1_e = 0.0"
+      ],
+      "guarantees": [
+        "p5_e <= 0.10000000000000009"
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [],
+      "output_vars": [
+        "p2_a",
+        "p2_e"
+      ],
+      "assumptions": [],
+      "guarantees": [
+        "p2_a <= 3.75",
+        "-p2_a <= 0.0",
+        "p2_e = 0.0"
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "p1_a",
+        "p1_e",
+        "p2_a",
+        "p2_e"
+      ],
+      "output_vars": [
+        "p5_a",
+        "p5_e"
+      ],
+      "assumptions": [
+        "p1_a <= 2.0",
+        "-p1_a <= 0.0",
+        "p1_e = 0.0",
+        "p2_a <= 3.75",
+        "-p2_a <= 0.0",
+        "p2_e = 0.0"
+      ],
+      "guarantees": [
+        "p5_e <= 0.10000000000000009"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_digital_signal_processing.py b/tests/test_digital_signal_processing.py
deleted file mode 100644
index 32813386..00000000
--- a/tests/test_digital_signal_processing.py
+++ /dev/null
@@ -1,415 +0,0 @@
-from pacti.terms.polyhedra import PolyhedralContract
-
-
-####################################################
-#Copy from tool.py in case_studies
-import copy
-import math
-
-DEBUG = True
-
-class PortWordLength(object):
-    def __init__(self, n: int = 0, p: int = 0, e: float = 0, a: float = None, name: str = "", value = None):
-        self._n = n # wordlength
-        self._p = p # wordlength
-        self._e = e # error known for this port
-        self._a = a # maximum possible value for this port
-        self._name = name # name of the port
-        if value is not None:
-            assert(isinstance(value, str))
-            assert(len(value) == n)
-        self._value = value # actual value for constant port.
-    @property
-    def n(self):
-        return self._n
-
-    @property
-    def a(self):
-        if self._value is None:
-            return get_actual_possible_value(self)
-        else:
-            return self.value_num()
-    
-    @property
-    def p(self):
-        return self._p
-
-    @property
-    def e(self):
-        return self._e
-    
-    @property
-    def name(self):
-        return self._name
-
-    @property
-    def value(self):
-        return self._value
-
-    def set_value(self, value: str):
-        self._value = value
-
-    def set_e(self, e: float):
-        self._e = e
-
-    def set_a(self, a: float):
-        self._a = a
-
-    def set_name(self, name: str):
-        self._name = name
-
-    def to_string(self):
-        return f"Port: {self.name}, (n, p) = ({self.n}, {self.p}), e = {self.e}, a = {self.a}"
-
-    def value_num(self):
-        return int(self.value, base=2) * 2 ** (- (self.n - self.p))
-
-
-def port_add(in1, in2, out):
-    ideal_result = in1.value_num() + in2.value_num()
-    actual_result = float_to_bin(ideal_result, out)
-    out.set_value(actual_result)
-
-def port_mult(in1, in2, out):
-    ideal_result = in1.value_num() * in2.value_num()
-    actual_result = float_to_bin(ideal_result, out)
-    out.set_value(actual_result)
-
-def float_to_bin(x, word_length: PortWordLength):
-    frac_part, int_part = math.modf(x)
-    p = word_length.p
-    # get integer part
-    if int_part == 0:
-        bin_str = ""
-    else:
-        bin_str = bin(int(int_part))[2:]
-        if len(bin_str) > p:
-            print("The port unable to hold the number, significant bits lost")
-        else:
-            bin_str = bin_str.zfill(p)
-    # get fractional part
-    frac_str = ""
-    req_length = word_length.n - word_length.p
-    while len(frac_str) != req_length:
-        frac_part *= 2
-        if frac_part >= 1:
-            frac_str += '1'
-            frac_part -= 1
-        else:
-            frac_str += '0'
-
-    return bin_str + frac_str
-
-
-def get_actual_possible_value(in_port: PortWordLength):
-    return (1 - (2 ** -in_port.n) )* 2 ** in_port.p
-########################################################################################
-#### Copy from Jupyter Notebook
-def truncation_error_same_position(pi, po):
-    assert(pi.p == po.p)
-    if pi.n > po.n:
-        return 2 ** po.p * (2 ** (-po.n) - 2 ** (-pi.n))
-    else :
-        return 0
-
-def truncation_error(pi, po):
-    # remove uneccesary most significant bits
-    # Remider: The assumption must hold!!
-    pi_adjusted = PortWordLength(n=pi.n - pi.p + po.p, p=po.p)
-    # return the truncation error as in case 1
-    return truncation_error_same_position(pi=pi_adjusted, po=po)
-
-def get_assumption_value(pi, po):
-    if pi.p > po.p:
-        return 2 ** po.p
-    else:
-        return float("inf") # no additional assumption needed
-
-def compute_required_word_length_add(in1: PortWordLength, in2:PortWordLength) -> PortWordLength:
-    new_n = max(in1.n, in2.n - in2.p + in1.p) - min(0, in1.p - in2.p) + 1
-    new_p = max(in1.p, in2.p) + 1
-    return PortWordLength(n=new_n, p=new_p)
-
-def compute_required_word_length_mult(in1: PortWordLength, in2:PortWordLength) -> PortWordLength:
-    new_n = in1.n + in2.n
-    new_p = in1.p + in2.p
-    return PortWordLength(n=new_n, p=new_p)
-
-
-def form_contract_add(in_port1, in_port2, out_port):
-    ret_contract = {}
-    # define input/output vars
-    ret_contract["InputVars"] = [f"{in_port1.name}_a", f"{in_port1.name}_e",
-                                 f"{in_port2.name}_a", f"{in_port2.name}_e"]
-    ret_contract["OutputVars"] = [f"{out_port.name}_a", f"{out_port.name}_e"]
-    # get assumption
-    ideal_out_port = compute_required_word_length_add(in1=in_port1, in2=in_port2)
-    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)
-    # write assumption in the contract
-    if assumption_value != float("inf"):
-        ret_contract["assumptions"] =  [{"coefficients":{f"{in_port1.name}_a":1, f"{in_port2.name}_a":1},
-                                    "constant":assumption_value}]
-    else:
-        ret_contract["assumptions"] = []
-    # get guarantee
-    e_t = truncation_error(pi=ideal_out_port, po=out_port)
-
-    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints
-    ret_contract["guarantees"] =  [{"coefficients":{f"{in_port1.name}_e":-1, f"{in_port2.name}_e":-1, f"{out_port.name}_e": 1},
-                                "constant":e_t},
-                                {"coefficients":{f"{out_port.name}_a": 1}, "constant":out_port.a},
-                                #{"coefficients":{f"{out_port.name}_a": 1}, "constant":in_port1.a + in_port2.a},
-                                {"coefficients":{f"{out_port.name}_a": 1, f"{in_port1.name}_a": -1, f"{in_port2.name}_a": -1}, "constant":0}
-                                ]
-    return ret_contract
-
-
-def form_contract_mult_const(in_port1, in_port_const, out_port):
-    ret_contract = {}
-    # define input/output vars
-    ret_contract["InputVars"] = [f"{in_port1.name}_a", f"{in_port1.name}_e"]
-    ret_contract["OutputVars"] = [f"{out_port.name}_a", f"{out_port.name}_e"]
-    # get assumption
-    ideal_out_port = compute_required_word_length_mult(in1=in_port1, in2=in_port_const)
-    assumption_value = get_assumption_value(pi=ideal_out_port, po=out_port)
-    # write assumption in the contract
-    if assumption_value != float("inf"):
-        print(assumption_value)
-        ret_contract["assumptions"] =  [{"coefficients":{f"{in_port1.name}_a": in_port_const.a},
-                                    "constant":assumption_value}]
-    else:
-        ret_contract["assumptions"] = []
-    # get guarantee
-    print(ideal_out_port.to_string())
-    e_t = truncation_error(pi=ideal_out_port, po=out_port)
-
-    # write guarantee in the contract, note the propagation is encoded in the polyhedral constraints
-    ret_contract["guarantees"] =  [{"coefficients":
-                                    {   f"{in_port1.name}_e":-in_port_const.a+in_port_const.e, 
-                                        f"{in_port1.name}_a":-in_port_const.e,
-                                        f"{out_port.name}_e": 1},
-                                    "constant":e_t},
-                                    {"coefficients":{f"{out_port.name}_a": 1}, "constant":out_port.a},
-                                    #{"coefficients":{f"{out_port.name}_a": 1}, "constant":in_port_const.a * in_port1.a},
-                                    {"coefficients":{f"{out_port.name}_a": 1, f"{in_port1.name}_a": -in_port_const.a}, "constant":0}
-                                    ]
-    return ret_contract
-
-def form_contract_input(in_port):
-    ret_contract = {}
-    # define input/output vars
-    ret_contract["InputVars"] = []
-    ret_contract["OutputVars"] = [f"{in_port.name}_a", f"{in_port.name}_e"]
-    # get assumption
-    ret_contract["assumptions"] = []
-    ret_contract["guarantees"] =  [ {"coefficients": {f"{in_port.name}_a": 1}, "constant": in_port.a},
-                                    {"coefficients": {f"{in_port.name}_a": -1}, "constant": 0},
-                                    {"coefficients": {f"{in_port.name}_e": 1}, "constant": in_port.e},
-                                    {"coefficients": {f"{in_port.name}_e": -1}, "constant": -in_port.e}]
-    return ret_contract
-
-
-def test_example1_catch_error():
-    p1 = PortWordLength(n=5, p=2, name = "p1")
-    p2 = PortWordLength(n=5, p=3, name = "p2")
-    p3 = PortWordLength(n=5, p=3, name = "p3")
-    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)
-
-    p4 = PortWordLength(n=7, p=3, name = "p4")
-    p5 = PortWordLength(n=6, p=3, name = "p5")
-    c2 = form_contract_add(in_port1=p3, in_port2=p4, out_port=p5)
-
-    contract1 = PolyhedralContract.from_dict(c1)
-    contract2 = PolyhedralContract.from_dict(c2)
-
-    contract_sys = contract1.compose(contract2)
-
-    c_p1 = form_contract_input(in_port=p1)
-    c_p2 = form_contract_input(in_port=p2)
-    c_p4 = form_contract_input(in_port=p4)
-
-    contract_p1 = PolyhedralContract.from_dict(c_p1)
-    contract_p2 = PolyhedralContract.from_dict(c_p2)
-    contract_p4 = PolyhedralContract.from_dict(c_p4)
-    
-    catch_error = False
-    try: 
-        contract_sys = contract1.compose(contract2)
-        contract_sys = contract_p1.compose(contract_sys)
-        contract_sys = contract_p2.compose(contract_sys)
-        contract_sys = contract_p4.compose(contract_sys)
-        print("Contract Sys:\n" + str(contract_sys))
-        return contract_sys
-    except ValueError as e:
-        print("Composition Error")
-        catch_error = True
-        print(e)
-
-    assert(catch_error)
-
-
-def test_example1_pass_with_inputs():
-    p1 = PortWordLength(n=5, p=2, name = "p1")
-    p2 = PortWordLength(n=5, p=3, name = "p2")
-    p3 = PortWordLength(n=5, p=3, name = "p3")
-    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)
-
-    p4 = PortWordLength(n=7, p=3, name = "p4")
-    p5 = PortWordLength(n=6, p=3, name = "p5")
-    c2 = form_contract_add(in_port1=p3, in_port2=p4, out_port=p5)
-
-    contract1 = PolyhedralContract.from_dict(c1)
-    contract2 = PolyhedralContract.from_dict(c2)
-
-    contract_sys = contract1.compose(contract2)
-
-    p1.set_value("10000")
-    p2.set_value("01111")
-    p4.set_value("0000001")
-
-    c_p1 = form_contract_input(in_port=p1)
-    c_p2 = form_contract_input(in_port=p2)
-    c_p4 = form_contract_input(in_port=p4)
-
-    contract_p1 = PolyhedralContract.from_dict(c_p1)
-    contract_p2 = PolyhedralContract.from_dict(c_p2)
-    contract_p4 = PolyhedralContract.from_dict(c_p4)
-    
-    no_error = True
-    try: 
-        contract_sys = contract1.compose(contract2)
-        contract_sys = contract_p1.compose(contract_sys)
-        contract_sys = contract_p2.compose(contract_sys)
-        contract_sys = contract_p4.compose(contract_sys)
-        print("Contract Sys:\n" + str(contract_sys))
-        return contract_sys
-    except ValueError as e:
-        print("Composition Error")
-        no_error = False
-        print(e)
-
-    assert(no_error)
-
-
-def get_optimization_specs():
-    p1 = PortWordLength(n=5, p=2, name = "p1")
-    p2 = PortWordLength(n=5, p=3, name = "p2")
-    p4 = PortWordLength(n=7, p=3, name = "p4")
-
-    p1.set_value("10000")
-    p2.set_value("01111")
-    p4.set_value("0000000")
-
-    ret_contract = {}
-    ret_contract["InputVars"] = []
-    ret_contract["OutputVars"] = ["p5_a", "p5_e"]
-    ret_contract["assumptions"] = []
-    ret_contract["guarantees"] = [
-                                  {"coefficients": {f"p5_e": 1}, "constant": 0.1}]
-    contract_spec = PolyhedralContract.from_dict(ret_contract)
-
-    c_p1 = form_contract_input(in_port=p1)
-    c_p2 = form_contract_input(in_port=p2)
-    c_p4 = form_contract_input(in_port=p4)
-
-    contract_p1 = PolyhedralContract.from_dict(c_p1)
-    contract_p2 = PolyhedralContract.from_dict(c_p2)
-    contract_p4 = PolyhedralContract.from_dict(c_p4)
-
-    tmp_c1 = contract_spec.quotient(contract_p1)
-
-    tmp_c2 = tmp_c1.quotient(contract_p2)
-    tmp_c3 = tmp_c2.quotient(contract_p4)
-    quotient_ret = tmp_c3
-    return quotient_ret, contract_spec
-
-def create_example1_by_p3(p3_n, p3_p):
-    p1 = PortWordLength(n=5, p=2, name = "p1")
-    p2 = PortWordLength(n=5, p=3, name = "p2")
-    p3 = PortWordLength(n=p3_n, p=p3_p, name = "p3")
-    c1 = form_contract_add(in_port1=p1, in_port2=p2, out_port=p3)
-
-    p4 = PortWordLength(n=7, p=3, name = "p4")
-    p5 = PortWordLength(n=6, p=3, name = "p5")
-    c2 = form_contract_add(in_port1=p3, in_port2=p4, out_port=p5)
-
-    p1.set_value("10000")
-    p2.set_value("01111")
-    p4.set_value("0000000")
-
-    contract1 = PolyhedralContract.from_dict(c1)
-    contract2 = PolyhedralContract.from_dict(c2)
-    return contract1, contract2, p1, p2, p3, p4, p5
-
-def test_optimization():
-    quotient_ret, contract_specs = get_optimization_specs()
-    ret = None
-    for n in range(5, 10):
-        #print(n)
-        p = 3 # keep the same number of bits (2) before binary point
-        contract1, contract2, p1, p2, p3, p4, p5 = create_example1_by_p3(p3_n=n, p3_p=p)
-        try:
-            contract_sys = contract1.compose(contract2)
-            #contract_sys = compose_all(contract1, contract2, p1, p2, p3, p4, p5)
-            #print(str(contract_sys))
-        except ValueError as e:
-            continue
-
-        if contract_sys.refines(quotient_ret):
-            ret = n
-            break
-
-    assert(ret == 6)
-
-def test_example_2():
-    in1 = PortWordLength(n=6, p=0, e=0, name="in1")
-    in2 = PortWordLength(n=6, p=0, e=0, name="in2")
-    in3 = PortWordLength(n=6, p=0, e=0, name="in3")
-    const1 = PortWordLength(n=6, p=0, name="const1")
-    const2 = PortWordLength(n=6, p=0, name="const2")
-    const3 = PortWordLength(n=6, p=0, name="const3")
-    mult_out1 = PortWordLength(n=6, p=0, name="mult_out1")
-    mult_out2 = PortWordLength(n=6, p=0, name="mult_out2")
-    mult_out3 = PortWordLength(n=6, p=0, name="mult_out3")
-    add_out1 = PortWordLength(n=6, p=0, name="add_out1")
-    add_out2 = PortWordLength(n=6, p=0, name="add_out2")
-
-    const1.set_value(float_to_bin(0.2, const1))
-    const2.set_value(float_to_bin(0.6, const2))
-    const3.set_value(float_to_bin(0.2, const3))
-    const1.set_e(0.2 - const1.value_num())
-    const2.set_e(0.6 - const2.value_num())
-    const3.set_e(0.2 - const3.value_num())
-
-    print(f"truncated coefficient: 0.2 to {const1.value_num()}")
-    print(f"truncated coefficient: 0.6 to {const2.value_num()}")
-    print(f"truncated coefficient: 0.2 to {const3.value_num()}")
-
-    c1 = form_contract_mult_const(in_port1=in1, in_port_const=const1, out_port=mult_out1)
-    c2 = form_contract_mult_const(in_port1=in2, in_port_const=const2, out_port=mult_out2)
-    c3 = form_contract_mult_const(in_port1=in3, in_port_const=const3, out_port=mult_out3)
-
-    ci1 = form_contract_input(in_port=in1)
-    ci2 = form_contract_input(in_port=in2)
-    ci3 = form_contract_input(in_port=in3)
-
-    contract1 = PolyhedralContract.from_dict(c1)
-    contract2 = PolyhedralContract.from_dict(c2)
-    contract3 = PolyhedralContract.from_dict(c3)
-    contract_i1 = PolyhedralContract.from_dict(ci1)
-    contract_i2 = PolyhedralContract.from_dict(ci2)
-    contract_i3 = PolyhedralContract.from_dict(ci3)
-    c4 = form_contract_add(in_port1 = mult_out1, in_port2=mult_out2, out_port=add_out1)
-    c5 = form_contract_add(in_port1 = add_out1, in_port2=mult_out3, out_port=add_out2)
-    contract4 = PolyhedralContract.from_dict(c4)
-    contract5 = PolyhedralContract.from_dict(c5)
-
-    contract_system = contract_i1.compose(contract1)
-    contract_system = contract_system.compose(contract_i2)
-    contract_system = contract_system.compose(contract2)
-    contract_system = contract_system.compose(contract_i3)
-    contract_system = contract_system.compose(contract3)
-    contract_system = contract_system.compose(contract4)
-    contract_system = contract_system.compose(contract5)
-
-    # TODO check result of contract 
\ No newline at end of file