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

Issue:
Python version upper limit
Fixes #287 
[BUG] Space mission test has typing issues
**Describe the bug**
```bash
$ make check-types
pdm run duty check-types

✗ Type-checking (1)
  > mypy --strict --allow-any-generics --implicit-reexport --allow-untyped-calls --config-file=config/mypy.ini src tests
  tests\case_studies\space_mission\space_mission_power.py:224: error: Name "scenario_sequence" is not defined  [name-defined]
  tests\case_studies\space_mission\space_mission_power.py:238: error: Name "scenario_sequence" is not defined  [name-defined]
  tests\case_studies\space_mission\space_mission_power.py:243: error: Name "scenario_sequence" is not defined  [name-defined]
  tests\case_studies\space_mission\space_mission_power.py:251: error: Name "scenario_sequence" is not defined  [name-defined]
  Found 4 errors in 1 file (checked 23 source files)
```

**Expected behavior**
Is this test being executed in Pacti's testbench?


Discussion / hints:

Fix patch:
diff --git a/.gitattributes b/.gitattributes
deleted file mode 100644
index fbb3d448..00000000
--- a/.gitattributes
+++ /dev/null
@@ -1,1 +0,0 @@
-*.data binary
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
deleted file mode 100644
index 9313e5bb..00000000
--- a/.github/workflows/ci.yml
+++ /dev/null
@@ -1,34 +0,0 @@
-on: [push]
-
-name: Test Action
-
-jobs:
-  build:
-    runs-on: ${{ matrix.os }}
-    strategy:
-      fail-fast: false
-      max-parallel: 4
-      matrix:
-        os: [windows-latest, ubuntu-latest, macos-latest]
-        python-version: ["3.8", "3.9", "3.10", "3.11"]
-        steps:
-          - uses: pdm-project/setup-pdm@main
-          name: Setup PDM
-          with:
-            python-version: ${{ matrix.python-version }}
-            architecture: x64
-            enable-pep582: true
-            - name: Install dependencies
-            run: pdm install
-            - name: Test code
-            run: make test
-            - name: Check types
-            run: make check-types
-            - name: Run linters on code
-            run: make check-quality
-            - name: Check types on Jupyter notebooks
-            run: make check-jn-types
-            - name: Run linters on Jupyter notebooks
-            run: make check-jn-quality
-            - name: Check documentation
-            run: make check-docs
diff --git a/.github/workflows/pacti_dev_review.yml b/.github/workflows/pacti_dev_review.yml
new file mode 100644
index 00000000..0e81e811
--- /dev/null
+++ b/.github/workflows/pacti_dev_review.yml
@@ -0,0 +1,38 @@
+on:
+  workflow_dispatch:
+  # push:
+  #   branches: ["*","!main"]
+
+name: Pacti Development Review
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        os: [ubuntu-latest]
+        python-version: ["3.10"]
+    steps:
+      - uses: actions/checkout@v3
+      - name: Setup PDM
+        uses: pdm-project/setup-pdm@main
+        with:
+          python-version: ${{ matrix.python-version }}
+          architecture: x64
+          enable-pep582: true
+      - name: Install dependencies
+        run: pdm install
+      - name: Test code
+        run: make test
+      - name: Check types
+        run: make check-types
+      - name: Run linters on code
+        run: make check-quality
+      - name: Check types on Jupyter notebooks
+        run: make check-jn-types
+      - name: Run linters on Jupyter notebooks
+        run: make check-jn-quality
+      - name: Check documentation
+        run: make check-docs
diff --git a/.github/workflows/pacti_development.yml b/.github/workflows/pacti_development.yml
new file mode 100644
index 00000000..ce15fc5d
--- /dev/null
+++ b/.github/workflows/pacti_development.yml
@@ -0,0 +1,27 @@
+on:
+  push:
+    branches: ["*","!main"]
+
+name: Pacti Development
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        os: [ubuntu-latest]
+        python-version: ["3.10"]
+    steps:
+      - uses: actions/checkout@v3
+      - name: Setup PDM
+        uses: pdm-project/setup-pdm@main
+        with:
+          python-version: ${{ matrix.python-version }}
+          architecture: x64
+          enable-pep582: true
+      - name: Install dependencies
+        run: pdm install
+      - name: Test code
+        run: make test
diff --git a/.github/workflows/pacti_pre_production.yml b/.github/workflows/pacti_pre_production.yml
new file mode 100644
index 00000000..9f7c7b63
--- /dev/null
+++ b/.github/workflows/pacti_pre_production.yml
@@ -0,0 +1,40 @@
+on:
+  workflow_dispatch:
+  # push:
+  #   branches: ["main"]
+  # pull_request:
+  #   branches: ["main"]
+
+name: Pacti Pre-Production
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        os: [ubuntu-latest]
+        python-version: ["3.8", "3.11"]
+    steps:
+      - uses: actions/checkout@v3
+      - name: Setup PDM
+        uses: pdm-project/setup-pdm@main
+        with:
+          python-version: ${{ matrix.python-version }}
+          architecture: x64
+          enable-pep582: true
+      - name: Install dependencies
+        run: pdm install
+      - name: Test code
+        run: make test
+      - name: Check types
+        run: make check-types
+      - name: Run linters on code
+        run: make check-quality
+      - name: Check types on Jupyter notebooks
+        run: make check-jn-types
+      - name: Run linters on Jupyter notebooks
+        run: make check-jn-quality
+      - name: Check documentation
+        run: make check-docs
diff --git a/.github/workflows/pacti_production.yml b/.github/workflows/pacti_production.yml
new file mode 100644
index 00000000..57a64446
--- /dev/null
+++ b/.github/workflows/pacti_production.yml
@@ -0,0 +1,40 @@
+on:
+  workflow_dispatch:
+  # push:
+  #   branches: ["main"]
+  # pull_request:
+  #   branches: ["main"]
+
+name: Pacti Production
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        os: [windows-latest, ubuntu-latest, macos-latest]
+        python-version: ["3.8", "3.9", "3.10", "3.11"]
+    steps:
+      - uses: actions/checkout@v3
+      - name: Setup PDM
+        uses: pdm-project/setup-pdm@main
+        with:
+          python-version: ${{ matrix.python-version }}
+          architecture: x64
+          enable-pep582: true
+      - name: Install dependencies
+        run: pdm install
+      - name: Test code
+        run: make test
+      - name: Check types
+        run: make check-types
+      - name: Run linters on code
+        run: make check-quality
+      - name: Check types on Jupyter notebooks
+        run: make check-jn-types
+      - name: Run linters on Jupyter notebooks
+        run: make check-jn-quality
+      - name: Check documentation
+        run: make check-docs
diff --git a/.gitignore b/.gitignore
index 08b5215d..2c009d2a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -166,7 +166,7 @@ pip-log.txt
 pip-delete-this-directory.txt
 
 # Unit test / coverage reports
-.tox/
+.tox-info*
 .coverage
 .coverage.*
 .cache
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 575cd8de..ed7dfe90 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -28,4 +28,10 @@ Use `pdm add` to install new packages.
     1. run `make docs-serve`
     2. go to http://localhost:8000 and check that everything looks good
     
+## Continuous Integration and Development
+Pacti has continuous integration and development setup with Github Actions. Some workflows are automatically run while others are manual. Instructions for all developers:
 
+1. If you are in the process of developing a feature/fixing a bug in your own development branch: Make sure that the Pacti Development workflow passes. This will automatically be run with every commit, so you should be getting notifications of what Pacti functionality failed (if any).
+2. If you are contributing a development feature to any branch (that is, your development has finished): Run the Pacti Development Review workflow. This will test the functionality and also code quality.
+3. If you are reviewing a pull-request to the main branch from another developer: Make sure to go to the "Actions" tab and run the Pacti Pre-Production workflow manually. This workflow tests the package for functionality and quality on two Python versions.
+4. The Pacti Production workflow makes sure that the software works with all OS and all Python versions.
diff --git a/Makefile b/Makefile
index 984ff2e1..7ccb9d5d 100644
--- a/Makefile
+++ b/Makefile
@@ -27,10 +27,6 @@ BASIC_DUTIES = \
 	check-dependencies \
 	clean \
 	coverage \
-	docs \
-	docs-deploy \
-	docs-regen \
-	docs-serve \
 	format \
 	release \
 	tox
@@ -38,7 +34,6 @@ BASIC_DUTIES = \
 QUALITY_DUTIES = \
 	check-quality \
 	check-jn-quality \
-	check-docs \
 	check-types \
 	check-jn-types \
 	test
diff --git a/README.md b/README.md
index eb1a1456..89df6191 100644
--- a/README.md
+++ b/README.md
@@ -11,101 +11,10 @@ system using assume-guarantee specifications, or contracts. Pacti's capabilities
 - Computing specifications of subsystems that need to be added to a design in order to meet an objective.
 - Verifying whether a component meets a specification.
 
-## Examples
-
-
-### Composition
-
-
-Suppose we have the following system:
-
-<picture>
-  <source media="(prefers-color-scheme: dark)" srcset="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_composition_scheme_d.svg" width="250">
-  <source media="(prefers-color-scheme: light)" srcset="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_composition_scheme_l.svg" width="250">
-  <img alt="Logo in light and dark mode." src="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_composition_scheme_l.svg" width="250">
-</picture>
-
-
-Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \le 2, o \le i \le 2o + 2)$ and $C' = (-1 \le o \le 1/5, o' \le o)$. We can use Pacti to obtain the specification of the system by executing the command
-
-`pacti examples/example.json result.json`
-
-Pacti places the result of composition in the file result.json. The output is
-
-```
-  Composed contract:      
-  InVars: [<Var i>]       
-  OutVars:[<Var o_p>]     
-  A: 5*i <= 1, -1/2*i <= 0
-  G: -1*i + 1*o_p <= 0
-```
-
-### Quotient
-
-
-Now we consider an example of quotient. Consider the following circuits:
-
-<picture>
-  <source media="(prefers-color-scheme: dark)" srcset="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_quotient_scheme_d.svg" width="250">
-  <source media="(prefers-color-scheme: light)" srcset="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_quotient_scheme_l.svg" width="250">
-  <img alt="Logo in light and dark mode." src="https://raw.githubusercontent.com/FormalSystems/media/main/doc/source/static/exports/circuit_series_quotient_scheme_l.svg" width="250">
-</picture>
-
-We wish to implement a system $M$ with specification $C = (|i| \le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing so that the resulting object meets the specification $C$. We run the command
-
-`pacti examples/example_quotient.json result.json`
-
-And Pacti outputs
-
-```
-  Contract quotient:
-  InVars: [<Var o>]
-  OutVars:[<Var o_p>]
-  A: 1*o <= 2, -1*o <= 2
-  G: -1*o + 1*o_p <= 1, 1*o + -1*o_p <= -1
-```
-
-# Installing
-
-## System requirements
-
-[pdm](https://github.com/pdm-project/pdm) (Make sure you run pdm version larger than 2.1.4)
-
-
-The installation will provide access to the command-line tool `pacti` and to the Python package of the same name. Any updates to the dev folder `src/pacti` will immediately be available in the system.
-
-
-## Install Dependencies
-
-As Pacti is in development, we use pdm manage the dependencies. To install run:
-
-```bash
-pdm install
-```
-
-The installation will provide access to the command-line tool `pacti` and to the Python package of the same name.
-To launch the command-line tool run `pdm run pacti`
-
-
-## Examples
-
-You can run examples via the command line:
-
-
-```bash
-pdm run pacti examples/example.json output.json
-```
-
-Or via python a script
-
-```bash
-pdm run python src/pacti/cli.py ./examples/example.json ./output.json
-```
 
 
 ## Links
 
-- Documentation: `make docs-serve`
 - Source Code: https://github.com/FormalSystems/pacti
 
 
diff --git a/config/coverage.ini b/config/coverage.ini
index b1c19eab..39f760c8 100644
--- a/config/coverage.ini
+++ b/config/coverage.ini
@@ -3,7 +3,6 @@ branch = true
 parallel = true
 source =
   src/
-  tests/
 
 [coverage:paths]
 equivalent =
diff --git a/config/tox.ini b/config/tox.ini
index bdd7deb3..0c1c0086 100644
--- a/config/tox.ini
+++ b/config/tox.ini
@@ -1,8 +1,19 @@
-# Usage: run 'pdm run tox run'
-
 [tox]
-env_list = py{38,39,310, 311}
+env_list = py{38,39,310,311},lint
+isolated_build = true
 
 [testenv]
-groups = dev
+setenv =
+    PDM_IGNORE_SAVED_PYTHON="1"
+deps = pdm
+commands =
+    pdm install --dev
+    duty test
 
+[testenv:lint]
+deps = pdm
+commands =
+    duty check-types
+	duty check-jn-types
+	duty check-quality
+	duty check-jn-quality
\ No newline at end of file
diff --git a/docs/Polyhedral.md b/docs/Polyhedral.md
deleted file mode 100644
index 4a5d5c95..00000000
--- a/docs/Polyhedral.md
+++ /dev/null
@@ -1,1 +0,0 @@
-::: pacti.terms.polyhedra.polyhedra
diff --git a/docs/case_studies.md b/docs/case_studies.md
deleted file mode 100644
index 107dfbc9..00000000
--- a/docs/case_studies.md
+++ /dev/null
@@ -1,32 +0,0 @@
-# Case Studies
-In the following sections we will present case studies that illustrate the use of pacti for different applications.
-
-<font size="5">[**Safety of autonomous vehicles**](/pacti/_case_studies/evaluating_perception/saved_results/)</font>
-
-We present a case study to evaluate the perception system of an autonomous car using the _quotient_ operator.
-
-<img src="/pacti/_case_studies/evaluating_perception/imglib/autonomy-stack.png" alt= "autonomy figure" width="700"/>
-
-<font size="5">[**Trajectory planning for multi-agent systems**](/pacti/_case_studies/multiagent_coordination/multiagent/)</font>
-
-<img src="/pacti/_case_studies/multiagent_coordination/multiagent_overview.png" alt= "multiagent figure" width="700"/>
-
-A case study on multi-agent path finding (MAPF) where multiple agents need to reach their target location on a grid world according to a conflict-free strategy.
-We will treat each time step as our viewpoint to find a solution that satisfies the agents' dynamics and collision constraints using the _merge_ operator.
-
-<font size="5">[**Specification-based synthetic biology**](/pacti/_case_studies/biocircuit_specifications/specification_based_synthetic_biology/)</font>
-
-A case study on modeling the specifications of a biological circuit and speed up the experimental design process by finding optimal components to use from a library of parts. In the case study, we first build a characterized library of parts as assume-guarantee contracts using existing experimental data from the literature.With the use of _Pacti_, we demonstrate how scientists may describe the desired top-level behavior as contracts and then computationally choose from a library of available parts to ensure that the components meet the top-level system specification. For the engineered bacteria case study, we find the specification of the sensors that meet the top-level criteria on fold-change of the circuit response. Finally, we also show how we can find the specifications of missing parts in a system. In synthetic biology, it is common to have parts in the system for which no characterization data is available. Using quotient operation on contracts, we can find the constraints that this missing part must satisfy to meet the desired top-level criteria. 
-
-<font size="5">[**Signal processing pipelines in digital ICs**](/pacti/_case_studies/digital_signal_processing/dsp_wl/)</font>
-
-A case study on word length analysis and optimization for digital signal processing circuit design.
-<img src="https://github.com/FormalSystems/media/blob/main/case_studies/digital_signal_processing/digital_filter_flow.png?raw=True" alt= "DSP figure" width="700"/>
-
-<font size="5">**Generating UAV topologies**</font>
-
-# Space Mission
-
-A case study on modeling the specifications of autonomous tasks for a planning/scheduling onboard of a space mission system.
-<font size="5">[**Signal processing pipelines in digital ICs**](/pacti/_case_studies/digital_signal_processing/dsp_wl/)</font>
-
diff --git a/docs/changelog.md b/docs/changelog.md
deleted file mode 100644
index 786b75d5..00000000
--- a/docs/changelog.md
+++ /dev/null
@@ -1,1 +0,0 @@
---8<-- "CHANGELOG.md"
diff --git a/docs/contributing.md b/docs/contributing.md
deleted file mode 100644
index ea38c9bf..00000000
--- a/docs/contributing.md
+++ /dev/null
@@ -1,1 +0,0 @@
---8<-- "CONTRIBUTING.md"
diff --git a/docs/credits.md b/docs/credits.md
deleted file mode 100644
index 6548eebd..00000000
--- a/docs/credits.md
+++ /dev/null
@@ -1,3 +0,0 @@
-```python exec="yes"
---8<-- "docs/gen_credits.py"
-```
diff --git a/docs/css/material.css b/docs/css/material.css
deleted file mode 100644
index 3a4ee937..00000000
--- a/docs/css/material.css
+++ /dev/null
@@ -1,25 +0,0 @@
-/* More space at the bottom of the page. */
-.md-main__inner {
-  margin-bottom: 1.5rem;
-}
-
-
-.md-content__button {
-  display: none;
-}
-
-/* override max-width that would otherwise be 61rem */
-.md-grid {
-  max-width: 100%;
-}
-
-
-/* this property was set to 1000, preventing the header from hiding the copy button */
-.jupyter-wrapper .zeroclipboard-container {
-  z-index: 0 !important;
-}
-
-
-html {
-  scroll-padding-top: 4rem;
-}
\ No newline at end of file
diff --git a/docs/css/mkdocstrings.css b/docs/css/mkdocstrings.css
deleted file mode 100644
index 42c77416..00000000
--- a/docs/css/mkdocstrings.css
+++ /dev/null
@@ -1,6 +0,0 @@
-/* Indentation. */
-div.doc-contents:not(.first) {
-  padding-left: 25px;
-  border-left: 4px solid rgba(230, 230, 230);
-  margin-bottom: 80px;
-}
diff --git a/docs/gen_credits.py b/docs/gen_credits.py
deleted file mode 100644
index f9d75879..00000000
--- a/docs/gen_credits.py
+++ /dev/null
@@ -1,122 +0,0 @@
-"""
-ISC License
-
-Copyright (c) 2019, Timothée Mazzucotelli
-
-Permission to use, copy, modify, and/or distribute this software for any
-purpose with or without fee is hereby granted, provided that the above
-copyright notice and this permission notice appear in all copies.
-
-THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
-WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
-MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
-ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
-WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
-ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
-OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
-"""
-
-
-import re
-from importlib.metadata import PackageNotFoundError, metadata
-from itertools import chain
-from pathlib import Path
-from textwrap import dedent
-
-import toml
-from jinja2 import StrictUndefined
-from jinja2.sandbox import SandboxedEnvironment
-
-project_dir = Path(".")
-pyproject = toml.load(project_dir / "pyproject.toml")
-project = pyproject["project"]
-pdm = pyproject["tool"]["pdm"]
-lock_data = toml.load(project_dir / "pdm.lock")
-lock_pkgs = {pkg["name"].lower(): pkg for pkg in lock_data["package"]}
-project_name = project["name"]
-regex = re.compile(r"(?P<dist>[\w.-]+)(?P<spec>.*)$")
-
-
-def get_license(pkg_name):
-    try:
-        data = metadata(pkg_name)
-    except PackageNotFoundError:
-        return "?"
-    license = data.get("License", "").strip()
-    multiple_lines = bool(license.count("\n"))
-    if multiple_lines or not license or license == "UNKNOWN":
-        for header, value in data.items():
-            if header == "Classifier" and value.startswith("License ::"):
-                license = value.rsplit("::", 1)[1].strip()
-    return license or "?"
-
-
-def get_deps(base_deps):
-    deps = {}
-    for dep in base_deps:
-        parsed = regex.match(dep).groupdict()
-        dep_name = parsed["dist"].lower()
-        deps[dep_name] = {"license": get_license(dep_name), **parsed, **lock_pkgs[dep_name]}
-
-    again = True
-    while again:
-        again = False
-        for pkg_name in lock_pkgs:
-            if pkg_name in deps:
-                for pkg_dependency in lock_pkgs[pkg_name].get("dependencies", []):
-                    parsed = regex.match(pkg_dependency).groupdict()
-                    dep_name = parsed["dist"].lower()
-                    if dep_name not in deps:
-                        deps[dep_name] = {"license": get_license(dep_name), **parsed, **lock_pkgs[dep_name]}
-                        again = True
-
-    return deps
-
-
-dev_dependencies = get_deps(chain(*pdm.get("dev-dependencies", {}).values()))
-prod_dependencies = get_deps(
-    chain(
-        project.get("dependencies", []),
-        chain(*project.get("optional-dependencies", {}).values()),
-    )
-)
-
-template_data = {
-    "project_name": project_name,
-    "prod_dependencies": sorted(prod_dependencies.values(), key=lambda dep: dep["name"]),
-    "dev_dependencies": sorted(dev_dependencies.values(), key=lambda dep: dep["name"]),
-    "more_credits": "",
-}
-template_text = dedent(
-    """
-    These projects were used to build `{{ project_name }}`. **Thank you!**
-
-    [`python`](https://www.python.org/) |
-    [`pdm`](https://pdm.fming.dev/) |
-    [`copier-pdm`](https://github.com/pawamoy/copier-pdm)
-
-    {% macro dep_line(dep) -%}
-    [`{{ dep.name }}`](https://pypi.org/project/{{ dep.name }}/) | {{ dep.summary }} | {{ ("`" ~ dep.spec ~ "`") if dep.spec else "" }} | `{{ dep.version }}` | {{ dep.license }}
-    {%- endmacro %}
-
-    ### Runtime dependencies
-
-    Project | Summary | Version (accepted) | Version (last resolved) | License
-    ------- | ------- | ------------------ | ----------------------- | -------
-    {% for dep in prod_dependencies -%}
-    {{ dep_line(dep) }}
-    {% endfor %}
-
-    ### Development dependencies
-
-    Project | Summary | Version (accepted) | Version (last resolved) | License
-    ------- | ------- | ------------------ | ----------------------- | -------
-    {% for dep in dev_dependencies -%}
-    {{ dep_line(dep) }}
-    {% endfor %}
-
-    {% if more_credits %}**[More credits from the author]({{ more_credits }})**{% endif %}
-    """
-)
-jinja_env = SandboxedEnvironment(undefined=StrictUndefined)
-print(jinja_env.from_string(template_text).render(**template_data))
diff --git a/docs/gen_ref_nav.py b/docs/gen_ref_nav.py
deleted file mode 100644
index b3b96eb2..00000000
--- a/docs/gen_ref_nav.py
+++ /dev/null
@@ -1,57 +0,0 @@
-"""
-ISC License
-
-Copyright (c) 2019, Timothée Mazzucotelli
-
-Permission to use, copy, modify, and/or distribute this software for any
-purpose with or without fee is hereby granted, provided that the above
-copyright notice and this permission notice appear in all copies.
-
-THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
-WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
-MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
-ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
-WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
-ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
-OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
-"""
-
-"""Generate the code reference pages and navigation."""
-
-from pathlib import Path
-
-import mkdocs_gen_files
-
-nav = mkdocs_gen_files.Nav()
-
-for path in sorted(Path("src").rglob("*.py")):
-    module_path = path.relative_to("src").with_suffix("")
-    doc_path = path.relative_to("src").with_suffix(".md")
-    full_doc_path = Path("reference", doc_path)
-
-    parts = tuple(module_path.parts)
-
-    if parts[-1] == "__init__":
-        parts = parts[:-1]
-        doc_path = doc_path.with_name("index.md")
-        full_doc_path = full_doc_path.with_name("index.md")
-    elif parts[-1] == "__main__":
-        continue
-    elif parts[-1] == "utils":
-        continue
-    elif parts[-1] == "cli":
-        continue
-
-    nav[parts] = doc_path.as_posix()
-
-    with mkdocs_gen_files.open(full_doc_path, "w") as fd:
-        ident = ".".join(parts)
-        fd.write(f"::: {ident}")
-
-    mkdocs_gen_files.set_edit_path(full_doc_path, path)
-
-# add pages manually:
-# nav["package", "module"] = "path/to/file.md"
-
-with mkdocs_gen_files.open("reference/SUMMARY.md", "w") as nav_file:
-    nav_file.writelines(nav.build_literate_nav())
diff --git a/docs/index.md b/docs/index.md
deleted file mode 100644
index d94fabb6..00000000
--- a/docs/index.md
+++ /dev/null
@@ -1,18 +0,0 @@
----
-hide:
-  - footer
----
-
-#
-<p align="center">
-<img src="/pacti/logos/pacti_colorful.svg" alt= "pacti logo" width="300"/>
-</p>
-
-Pacti is a Python package for carrying out compositional system analysis and design. Pacti represents components in a
-system using assume-guarantee specifications, or contracts. Pacti's capabilities include the following:
-
-- Obtaining sensible system specifications from the specifications of the constituent subsystems.
-- Computing specifications of subsystems that need to be added to a design in order to meet an objective.
-- Verifying whether a component meets a specification.
-
-
diff --git a/docs/installing.md b/docs/installing.md
deleted file mode 100644
index 956a4f91..00000000
--- a/docs/installing.md
+++ /dev/null
@@ -1,62 +0,0 @@
-
-## Installing
-
-### System requirements
-
-[pdm](https://github.com/pdm-project/pdm) (Make sure you run pdm version larger than 2.1.4)
-
-[scipy](https://scipy.org/install/)
-
-The installation will provide access to the command-line tool `pacti` and to the the Python package of the same name. Any updates to the dev folder `src/pacti` will immediately be available in the system.
-
-
-### Install Dependencies
-
-As Pacti is in development, we use pdm manage the dependencies. To install run:
-
-```bash
-pdm install
-```
-
-The installation will provide access to the command-line tool `pacti` and to the Python package of the same name.
-To launch the command-line tool run `pdm run pacti`
-
-
-### Examples
-
-You can run examples via the command line:
-
-
-```bash
-pdm run pacti examples/example.json output.json
-```
-
-Or via python a script
-
-```bash
-pdm run python src/pacti/cli.py ./examples/example.json ./output.json
-```
-
-
-## Links
-
-- Documentation: `make docs-serve`
-- Source Code: https://github.com/iincer/contractTool
-
-## Troubleshooting
-
-### Working With Apple ICs
-
-Some packages do not fully support recent Apple ICs (i.e., `scipy`, `numpy`). 
-We recommend installing them at system level via pip as:
-
-```bash
-pip install --pre -i https://pypi.anaconda.org/scipy-wheels-nightly/simple scipy
-```
-
-Or via brew:
-
-```bash
-brew install scipy
-```
-
diff --git a/docs/iocontract.md b/docs/iocontract.md
deleted file mode 100644
index 697049e0..00000000
--- a/docs/iocontract.md
+++ /dev/null
@@ -1,2 +0,0 @@
-
-::: pacti.iocontract.iocontract
\ No newline at end of file
diff --git a/docs/license.md b/docs/license.md
deleted file mode 100644
index cdacdfef..00000000
--- a/docs/license.md
+++ /dev/null
@@ -1,3 +0,0 @@
-```
---8<-- "LICENSE"
-```
diff --git a/docs/pacti_small_icon.svg b/docs/pacti_small_icon.svg
deleted file mode 100644
index ed8e91b2..00000000
--- a/docs/pacti_small_icon.svg
+++ /dev/null
@@ -1,1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="500" zoomAndPan="magnify" viewBox="0 0 375 374.999991" height="500" preserveAspectRatio="xMidYMid meet" version="1.0"><defs><clipPath id="0dc03abead"><path d="M 107 79 L 208 79 L 208 181 L 107 181 Z M 107 79 " clip-rule="nonzero"/></clipPath><clipPath id="a8db864ebf"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="a7748e6ddc"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="40744be06d"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="f914eab84c"><path d="M 141 113 L 173 113 L 173 146 L 141 146 Z M 141 113 " clip-rule="nonzero"/></clipPath><clipPath id="48edd4f396"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="ce9d0b3873"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="53954893dd"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="2f152358f6"><path d="M 162 144 L 289 144 L 289 272 L 162 272 Z M 162 144 " clip-rule="nonzero"/></clipPath><clipPath id="ab8568eb48"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="148b62cceb"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="dfdacad933"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="f4136556b6"><path d="M 205 187 L 247 187 L 247 229 L 205 229 Z M 205 187 " clip-rule="nonzero"/></clipPath><clipPath id="9cafd204b6"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="0b10ebb184"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="697f185a59"><path d="M 89.125 254.597656 L 114.835938 72.800781 L 306.199219 99.867188 L 280.488281 281.664062 Z M 89.125 254.597656 " clip-rule="nonzero"/></clipPath><clipPath id="98e6e3569f"><path d="M 182.746094 166.859375 L 264 166.859375 L 264 249 L 182.746094 249 Z M 182.746094 166.859375 " clip-rule="nonzero"/></clipPath><clipPath id="96396babf3"><path d="M 223.316406 166.859375 C 200.910156 166.859375 182.746094 185.230469 182.746094 207.890625 C 182.746094 230.554688 200.910156 248.925781 223.316406 248.925781 C 245.71875 248.925781 263.882812 230.554688 263.882812 207.890625 C 263.882812 185.230469 245.71875 166.859375 223.316406 166.859375 " clip-rule="nonzero"/></clipPath><clipPath id="af6c12a8c8"><path d="M 130.863281 104.140625 L 181.863281 104.140625 L 181.863281 155.140625 L 130.863281 155.140625 Z M 130.863281 104.140625 " clip-rule="nonzero"/></clipPath></defs><g clip-path="url(#0dc03abead)"><g clip-path="url(#a8db864ebf)"><g clip-path="url(#a7748e6ddc)"><g clip-path="url(#40744be06d)"><path fill="#000000" d="M 133.636719 85.515625 L 133.441406 85.488281 C 129.097656 87.910156 125.257812 91.007812 121.53125 94.730469 L 121.730469 94.757812 C 123.800781 98.492188 126.070312 102.253906 128.363281 105.816406 C 127.382812 107.09375 126.628906 108.199219 125.871094 109.308594 C 124.863281 110.78125 123.855469 112.257812 123.207031 113.988281 C 122.929688 114.554688 122.648438 115.125 122.5625 115.71875 C 118.195312 115.503906 113.824219 115.292969 109.425781 115.277344 C 108.753906 117.207031 108.472656 119.191406 107.96875 121.34375 L 107.519531 124.519531 C 107.4375 126.53125 107.183594 128.316406 107.324219 130.15625 C 111.355469 131.335938 115.613281 132.339844 119.898438 133.148438 C 119.785156 133.941406 119.898438 134.566406 119.984375 135.386719 C 119.953125 135.585938 119.925781 135.785156 120.09375 136.011719 C 120.261719 137.652344 120.820312 139.351562 121.382812 141.046875 C 121.773438 142.519531 122.195312 143.792969 122.808594 145.09375 C 119.585938 148.078125 116.589844 150.894531 113.367188 153.878906 L 113.144531 154.046875 C 113.621094 154.925781 114.09375 155.800781 114.597656 156.480469 C 115.382812 158.007812 116.390625 159.363281 117.425781 160.523438 C 118.742188 162.53125 120.507812 164.195312 122.246094 166.058594 L 122.273438 165.863281 C 125.96875 163.753906 129.5 161.421875 133.226562 159.113281 C 134.289062 160.074219 135.550781 161.0625 136.644531 161.824219 C 138.097656 162.839844 139.78125 163.683594 141.292969 164.300781 C 142.019531 164.808594 142.777344 165.121094 143.363281 165.203125 C 143.140625 169.621094 142.914062 174.042969 142.914062 178.292969 C 144.816406 178.964844 146.75 179.441406 148.90625 179.746094 C 151.847656 180.164062 154.816406 180.378906 157.648438 180.171875 C 158.628906 176.0625 159.609375 171.953125 160.617188 167.644531 C 161.402344 167.753906 162.214844 167.667969 162.859375 167.351562 C 164.679688 167.207031 166.332031 166.832031 168.210938 166.289062 C 169.695312 165.6875 171.152344 165.289062 172.46875 164.460938 C 175.410156 167.710938 178.152344 170.933594 181.121094 173.980469 C 185.660156 171.589844 189.695312 168.515625 193.222656 164.765625 L 193.027344 164.738281 C 190.929688 161.203125 188.660156 157.445312 186.363281 153.882812 L 186.390625 153.683594 C 187.121094 152.773438 187.878906 151.667969 188.605469 150.757812 C 189.644531 149.082031 190.707031 147.210938 191.351562 145.480469 C 191.660156 144.714844 191.941406 144.148438 192.222656 143.582031 C 196.394531 143.765625 200.765625 143.980469 205.160156 143.992188 C 205.609375 142.234375 206.058594 140.476562 206.339844 138.496094 L 206.761719 135.519531 C 207.070312 133.335938 207.183594 131.125 207.097656 128.890625 C 203.035156 127.910156 198.78125 126.902344 194.523438 125.894531 C 194.410156 125.273438 194.296875 124.648438 194.1875 124.027344 C 194.046875 122.1875 193.683594 120.515625 193.125 118.816406 C 192.730469 117.347656 192.144531 115.847656 191.359375 114.320312 C 191.554688 114.347656 191.554688 114.347656 191.582031 114.148438 C 194.777344 111.363281 198 108.378906 201.027344 105.367188 C 200.71875 104.714844 200.410156 104.066406 199.933594 103.1875 C 199.121094 101.859375 198.113281 100.503906 197.078125 99.34375 C 195.566406 97.308594 193.855469 95.246094 191.925781 93.355469 C 188.199219 95.660156 184.472656 97.964844 180.941406 100.300781 L 180.746094 100.273438 C 179.851562 99.539062 178.757812 98.777344 177.667969 98.015625 C 176.183594 97.199219 174.726562 96.183594 173.214844 95.566406 C 173.015625 95.535156 172.820312 95.507812 172.847656 95.3125 C 172.066406 95.199219 171.503906 94.917969 171.140625 94.664062 C 171.367188 90.246094 171.589844 85.824219 171.789062 81.601562 C 169.882812 80.929688 167.921875 80.652344 165.988281 80.175781 L 162.65625 79.703125 C 160.667969 79.625 158.707031 79.347656 156.691406 79.46875 C 155.707031 83.578125 154.699219 87.886719 153.691406 92.195312 C 153.074219 92.3125 152.457031 92.425781 151.871094 92.34375 C 150.019531 92.6875 148.171875 93.035156 146.292969 93.578125 C 145.035156 94.007812 143.550781 94.605469 142.289062 95.035156 C 139.515625 92.011719 136.578125 88.765625 133.636719 85.515625 Z M 142.417969 140.785156 C 139.199219 136.6875 138.050781 132.074219 138.949219 127.140625 C 139.480469 121.957031 141.835938 118.039062 146.09375 114.796875 C 150.128906 111.726562 154.695312 110.550781 159.597656 111.242188 C 164.695312 111.964844 168.558594 114.332031 171.777344 118.429688 C 174.773438 122.699219 175.949219 127.113281 175.222656 132.273438 C 174.519531 137.230469 172.136719 141.347656 168.101562 144.417969 C 163.871094 147.460938 159.503906 148.664062 154.40625 147.945312 C 149.503906 147.25 145.441406 144.855469 142.417969 140.785156 Z M 142.417969 140.785156 " fill-opacity="1" fill-rule="nonzero"/></g></g></g></g><g clip-path="url(#f914eab84c)"><g clip-path="url(#48edd4f396)"><g clip-path="url(#ce9d0b3873)"><g clip-path="url(#53954893dd)"><path fill="#000000" d="M 141.523438 127.304688 C 140.90625 131.667969 141.972656 135.460938 144.464844 139.050781 C 147.179688 142.472656 150.484375 144.558594 154.796875 145.167969 C 159.113281 145.777344 162.867188 144.691406 166.421875 142.15625 C 170.007812 139.425781 172.082031 136.078125 172.699219 131.714844 C 173.316406 127.347656 172.253906 123.554688 169.566406 119.9375 C 166.878906 116.320312 163.542969 114.433594 159.230469 113.824219 C 154.917969 113.210938 151.191406 114.101562 147.605469 116.832031 C 144.214844 119.589844 142.140625 122.941406 141.523438 127.304688 Z M 147.601562 136.664062 C 145.78125 133.976562 144.996094 131.03125 145.445312 127.859375 C 145.894531 124.683594 147.464844 122.074219 149.957031 120 C 152.648438 117.949219 155.335938 117.320312 158.671875 117.789062 C 162.003906 118.261719 164.609375 119.640625 166.429688 122.328125 C 168.445312 125.039062 169.226562 127.984375 168.777344 131.160156 C 168.328125 134.332031 166.761719 136.945312 164.070312 138.992188 C 161.605469 140.867188 158.691406 141.671875 155.359375 141.199219 C 152.222656 140.757812 149.644531 139.175781 147.601562 136.664062 Z M 147.601562 136.664062 " fill-opacity="1" fill-rule="nonzero"/></g></g></g></g><g clip-path="url(#2f152358f6)"><g clip-path="url(#ab8568eb48)"><g clip-path="url(#148b62cceb)"><g clip-path="url(#dfdacad933)"><path fill="#000000" d="M 166.46875 182.835938 C 165.964844 183.574219 165.683594 184.144531 165.601562 184.738281 C 164.675781 187.035156 163.945312 189.359375 163.21875 191.6875 C 168.203125 194.617188 173.050781 197.125 177.894531 199.628906 L 177.390625 203.199219 C 177.25 205.609375 177.136719 207.820312 177.21875 210.054688 C 177.164062 211.871094 177.5 213.738281 177.835938 215.605469 C 172.875 218.144531 167.890625 220.878906 163.125 223.441406 L 162.902344 223.613281 C 163.125 224.859375 163.351562 226.105469 163.796875 227.179688 C 164.300781 229.273438 165.03125 231.199219 165.953125 233.152344 C 166.933594 236.121094 168.332031 238.949219 170.152344 241.636719 L 170.347656 241.664062 C 175.585938 239.976562 180.796875 238.488281 186.035156 236.800781 C 187.210938 238.382812 188.222656 239.738281 189.621094 241.152344 C 190.964844 242.960938 192.730469 244.625 194.523438 246.09375 C 195.222656 246.800781 195.949219 247.308594 196.875 247.84375 C 195.109375 253.261719 193.34375 258.675781 191.773438 264.121094 C 193.984375 265.445312 196.199219 266.769531 198.632812 267.921875 C 202.441406 269.269531 206.054688 270.59375 209.726562 271.515625 L 217.796875 256.875 L 220.542969 257.261719 C 222.699219 257.566406 225.078125 257.699219 227.515625 257.4375 C 229.503906 257.515625 231.550781 257.199219 233.59375 256.882812 C 236.085938 261.886719 238.605469 266.695312 241.292969 271.730469 C 247.511719 270.183594 253.480469 267.585938 259.136719 264.339844 L 259.167969 264.140625 C 257.515625 258.847656 256.058594 253.582031 254.4375 248.09375 C 255.78125 247.070312 256.929688 246.015625 258.273438 244.992188 C 260.097656 243.429688 261.777344 241.441406 263.484375 239.253906 C 263.960938 238.714844 264.46875 237.976562 265.167969 237.265625 C 270.320312 239.007812 275.699219 240.578125 281.078125 242.148438 C 282.367188 240.105469 283.457031 238.03125 284.382812 235.734375 C 284.664062 235.167969 285.222656 234.03125 285.898438 232.105469 C 287.074219 229.4375 287.859375 226.714844 288.617188 224.191406 C 283.628906 221.261719 278.8125 218.558594 273.773438 216.023438 L 274.136719 213.445312 C 274.472656 211.0625 274.585938 208.851562 274.503906 206.617188 C 274.390625 204.574219 274.082031 202.507812 273.777344 200.441406 C 273.777344 200.441406 273.972656 200.46875 274 200.269531 C 278.957031 197.734375 283.945312 195 288.902344 192.464844 C 288.457031 191.386719 288.203125 190.339844 287.921875 189.492188 C 287.417969 187.398438 286.691406 185.472656 285.964844 183.550781 C 284.621094 180.324219 283.050781 177.269531 281.261719 174.386719 C 275.855469 175.847656 270.617188 177.535156 265.179688 179.191406 C 264.171875 177.835938 263.136719 176.679688 262.128906 175.320312 C 260.5625 173.683594 258.796875 172.015625 257.199219 170.578125 C 257.003906 170.550781 256.835938 170.324219 256.640625 170.296875 C 256.109375 169.816406 255.378906 169.308594 254.847656 168.828125 C 256.613281 163.410156 258.183594 157.96875 259.949219 152.550781 C 257.738281 151.226562 255.496094 150.101562 253.058594 148.945312 C 252.5 148.664062 251.9375 148.382812 251.183594 148.074219 C 250.621094 147.792969 250.035156 147.710938 249.304688 147.203125 C 246.8125 146.445312 244.347656 145.488281 242.023438 144.957031 C 239.136719 149.8125 236.617188 154.917969 233.925781 159.796875 L 231.574219 159.464844 C 229.21875 159.132812 226.644531 158.972656 224.207031 159.234375 C 222.414062 159.183594 220.5625 159.527344 218.742188 159.675781 C 216.25 154.667969 213.5625 149.632812 210.847656 144.796875 L 210.875 144.601562 C 204.65625 146.148438 198.71875 148.546875 193.003906 152.191406 C 194.429688 157.652344 196.082031 162.945312 197.734375 168.238281 C 196.164062 169.433594 194.59375 170.625 193.222656 171.847656 C 191.597656 173.441406 189.972656 175.03125 188.710938 176.878906 C 188.039062 177.390625 187.535156 178.128906 187.058594 178.667969 C 181.679688 177.097656 176.332031 175.328125 170.953125 173.757812 C 169.636719 176 168.292969 178.441406 167.140625 180.910156 C 166.863281 181.476562 166.554688 182.242188 166.46875 182.835938 Z M 234.582031 230.109375 C 228.417969 232.675781 222.421875 232.636719 216.402344 229.964844 C 210.351562 227.492188 206.179688 223.054688 203.660156 216.832031 C 201.308594 210.832031 201.394531 204.570312 203.832031 198.644531 C 206.496094 192.546875 210.726562 188.085938 216.859375 185.714844 C 223.023438 183.144531 229.019531 183.183594 235.039062 185.859375 C 241.089844 188.332031 245.261719 192.765625 247.613281 198.765625 C 250.105469 205.1875 250.046875 211.25 247.414062 217.152344 C 244.945312 223.277344 240.519531 227.710938 234.582031 230.109375 Z M 234.582031 230.109375 " fill-opacity="1" fill-rule="nonzero"/></g></g></g></g><g clip-path="url(#f4136556b6)"><g clip-path="url(#9cafd204b6)"><g clip-path="url(#0b10ebb184)"><g clip-path="url(#697f185a59)"><path fill="#000000" d="M 217.886719 226.53125 C 222.957031 228.867188 228.140625 228.996094 233.238281 226.882812 L 233.265625 226.683594 C 238.558594 224.601562 242.089844 220.851562 244.417969 215.714844 C 246.546875 210.554688 246.6875 205.3125 244.644531 199.964844 C 242.40625 194.589844 238.902344 191.058594 233.835938 188.722656 L 233.636719 188.695312 C 228.542969 186.558594 223.332031 186.628906 218.234375 188.742188 C 212.9375 190.824219 209.210938 194.546875 207.082031 199.710938 C 204.753906 204.84375 204.78125 210.3125 206.855469 215.460938 C 208.898438 220.808594 212.59375 224.367188 217.886719 226.53125 Z M 211.726562 213.519531 C 210.105469 209.445312 210.050781 205.59375 211.785156 201.792969 C 213.328125 197.964844 216.128906 195.121094 220.164062 193.464844 C 224.003906 191.785156 227.980469 191.941406 231.761719 193.488281 C 235.515625 195.234375 238.3125 198.058594 239.769531 201.90625 L 239.964844 201.933594 C 241.394531 205.980469 241.449219 209.832031 239.710938 213.632812 C 238.140625 217.660156 235.367188 220.304688 231.332031 221.960938 C 227.523438 223.445312 223.714844 223.511719 219.738281 221.9375 C 215.984375 220.191406 213.378906 217.398438 211.726562 213.519531 Z M 211.726562 213.519531 " fill-opacity="1" fill-rule="nonzero"/></g></g></g></g><g clip-path="url(#98e6e3569f)"><g clip-path="url(#96396babf3)"><path fill="#000000" d="M 182.746094 166.859375 L 263.324219 166.859375 L 263.324219 249.804688 L 182.746094 249.804688 Z M 182.746094 166.859375 " fill-opacity="1" fill-rule="nonzero"/></g></g><g clip-path="url(#af6c12a8c8)"><path fill="#000000" d="M 181.863281 129.640625 C 181.863281 130.476562 181.820312 131.308594 181.738281 132.140625 C 181.65625 132.972656 181.535156 133.796875 181.371094 134.617188 C 181.210938 135.433594 181.007812 136.246094 180.765625 137.042969 C 180.523438 137.84375 180.242188 138.628906 179.921875 139.398438 C 179.601562 140.171875 179.246094 140.925781 178.851562 141.660156 C 178.457031 142.398438 178.027344 143.113281 177.566406 143.808594 C 177.101562 144.503906 176.605469 145.171875 176.074219 145.816406 C 175.542969 146.464844 174.984375 147.082031 174.394531 147.671875 C 173.804688 148.261719 173.183594 148.824219 172.539062 149.351562 C 171.894531 149.882812 171.222656 150.378906 170.527344 150.84375 C 169.835938 151.308594 169.121094 151.738281 168.382812 152.128906 C 167.644531 152.523438 166.890625 152.878906 166.121094 153.199219 C 165.347656 153.519531 164.5625 153.800781 163.765625 154.042969 C 162.964844 154.285156 162.15625 154.488281 161.335938 154.652344 C 160.519531 154.8125 159.691406 154.9375 158.863281 155.019531 C 158.03125 155.101562 157.199219 155.140625 156.363281 155.140625 C 155.527344 155.140625 154.695312 155.101562 153.863281 155.019531 C 153.03125 154.9375 152.207031 154.8125 151.386719 154.652344 C 150.566406 154.488281 149.757812 154.285156 148.960938 154.042969 C 148.160156 153.800781 147.375 153.519531 146.605469 153.199219 C 145.832031 152.878906 145.078125 152.523438 144.339844 152.128906 C 143.605469 151.738281 142.890625 151.308594 142.195312 150.84375 C 141.5 150.378906 140.832031 149.882812 140.183594 149.351562 C 139.539062 148.824219 138.921875 148.261719 138.332031 147.671875 C 137.742188 147.082031 137.179688 146.464844 136.648438 145.816406 C 136.121094 145.171875 135.625 144.503906 135.160156 143.808594 C 134.695312 143.113281 134.265625 142.398438 133.875 141.660156 C 133.480469 140.925781 133.121094 140.171875 132.804688 139.398438 C 132.484375 138.628906 132.203125 137.84375 131.960938 137.042969 C 131.71875 136.246094 131.515625 135.433594 131.351562 134.617188 C 131.1875 133.796875 131.066406 132.972656 130.984375 132.140625 C 130.902344 131.308594 130.863281 130.476562 130.863281 129.640625 C 130.863281 128.804688 130.902344 127.972656 130.984375 127.140625 C 131.066406 126.308594 131.1875 125.484375 131.351562 124.667969 C 131.515625 123.847656 131.71875 123.039062 131.960938 122.238281 C 132.203125 121.441406 132.484375 120.652344 132.804688 119.882812 C 133.121094 119.109375 133.480469 118.355469 133.875 117.621094 C 134.265625 116.882812 134.695312 116.167969 135.160156 115.472656 C 135.625 114.78125 136.121094 114.109375 136.648438 113.464844 C 137.179688 112.820312 137.742188 112.199219 138.332031 111.609375 C 138.921875 111.019531 139.539062 110.460938 140.183594 109.929688 C 140.832031 109.398438 141.5 108.902344 142.195312 108.4375 C 142.890625 107.976562 143.605469 107.546875 144.339844 107.152344 C 145.078125 106.757812 145.832031 106.402344 146.605469 106.082031 C 147.375 105.761719 148.160156 105.480469 148.960938 105.238281 C 149.757812 104.996094 150.566406 104.792969 151.386719 104.632812 C 152.207031 104.46875 153.03125 104.347656 153.863281 104.265625 C 154.695312 104.183594 155.527344 104.140625 156.363281 104.140625 C 157.199219 104.140625 158.03125 104.183594 158.863281 104.265625 C 159.691406 104.347656 160.519531 104.46875 161.335938 104.632812 C 162.15625 104.792969 162.964844 104.996094 163.765625 105.238281 C 164.5625 105.480469 165.347656 105.761719 166.121094 106.082031 C 166.890625 106.402344 167.644531 106.757812 168.382812 107.152344 C 169.121094 107.546875 169.835938 107.976562 170.527344 108.4375 C 171.222656 108.902344 171.894531 109.398438 172.539062 109.929688 C 173.183594 110.460938 173.804688 111.019531 174.394531 111.609375 C 174.984375 112.199219 175.542969 112.820312 176.074219 113.464844 C 176.605469 114.109375 177.101562 114.78125 177.566406 115.472656 C 178.027344 116.167969 178.457031 116.882812 178.851562 117.621094 C 179.246094 118.355469 179.601562 119.109375 179.921875 119.882812 C 180.242188 120.652344 180.523438 121.441406 180.765625 122.238281 C 181.007812 123.039062 181.210938 123.847656 181.371094 124.667969 C 181.535156 125.484375 181.65625 126.308594 181.738281 127.140625 C 181.820312 127.972656 181.863281 128.804688 181.863281 129.640625 Z M 181.863281 129.640625 " fill-opacity="1" fill-rule="nonzero"/></g></svg>
\ No newline at end of file
diff --git a/duties.py b/duties.py
index d02efc46..0d7fd423 100644
--- a/duties.py
+++ b/duties.py
@@ -33,17 +33,22 @@
 
 from duty import duty
 
-DIR_SEARCH = ["src", "tests", "case_studies", "docs"]
+DIR_SEARCH = ["src", "tests", "docs"]
 PY_SRC_PATHS = (Path(_) for _ in DIR_SEARCH)
 PY_SRC_LIST = tuple(str(_) for _ in PY_SRC_PATHS)
 PY_SRC = " ".join(PY_SRC_LIST)
 JNB_SRC = " ".join([el for src in DIR_SEARCH for el in glob.glob(src+"/**/*.ipynb", recursive=True)])
+print(JNB_SRC)
 TESTING = os.environ.get("TESTING", "0") in {"1", "true"}
 CI = os.environ.get("CI", "0") in {"1", "true", "yes", ""}
 WINDOWS = os.name == "nt"
 PTY = not WINDOWS and not CI
 MYPY_FLAGS = "--allow-any-generics --implicit-reexport --allow-untyped-calls"
-FLAKE8_FLAGS_JN = "--ignore=D100,WPS226,WPS421,WPS111,BLK100 "
+FLAKE8_FLAGS_JN = "--ignore=D100,WPS226,WPS421,WPS111,BLK100,E402,WPS331,WPS221,WPS231,N806,WPS114,D212"
+
+sys.stdin.reconfigure(encoding='utf-8')
+sys.stdout.reconfigure(encoding='utf-8')
+
 #FLAKE8_FLAGS_JN = ""
 
 #sys.stdin.reconfigure(encoding='utf-8')
@@ -133,7 +138,7 @@ def changelog(ctx):
     )
 
 
-@duty(pre=["check_quality", "check_types", "check_docs", "check_dependencies"])
+@duty(pre=["check_quality", "check_types", "check_dependencies"])
 def check(ctx):
     """
     Check it all!
@@ -175,7 +180,7 @@ def tox(ctx):
     Arguments:
         ctx: The context instance (passed automatically).
     """
-    ctx.run(f"tox run -c config/tox.ini", title="Running tox", pty=PTY, capture=False)
+    ctx.run(f"tox --workdir . --root . -c config/tox.ini", title="Testing over platforms", pty=PTY, capture=False)
 
 
 @duty
@@ -227,18 +232,6 @@ def safety():  # noqa: WPS430
     ctx.run(safety, title="Checking dependencies")
 
 
-@duty
-def check_docs(ctx):
-    """
-    Check if the documentation builds correctly.
-
-    Arguments:
-        ctx: The context instance (passed automatically).
-    """
-    Path("htmlcov").mkdir(parents=True, exist_ok=True)
-    Path("htmlcov/index.html").touch(exist_ok=True)
-    copy_case_studies(ctx)
-    ctx.run("mkdocs build -s", title="Building documentation", pty=PTY)
 
 
 @duty  # noqa: WPS231
@@ -281,70 +274,9 @@ def clean(ctx):
     shutil.rmtree("pip-wheel-metadata",ignore_errors=True)
     shutil.rmtree("site",ignore_errors=True)
     shutil.rmtree("__pycache__",ignore_errors=True)
-    shutil.rmtree("docs/_case_studies",ignore_errors=True)
     shutil.rmtree(".venv",ignore_errors=True)
 
 
-def copy_case_studies(ctx):
-    if os.path.exists("docs/_case_studies"):
-        shutil.rmtree("docs/_case_studies")
-
-    ctx.run("cp -r case_studies docs/_case_studies")
-    py_files = glob.glob("docs/_case_studies/**/*.py", recursive=True)
-    for path in py_files:
-        pathlib.Path.unlink(Path(path))
-    # get all jupyter files in configuration
-    with open("mkdocs.yml") as f:
-        contents = f.readlines()
-    nb_files_use = []
-    for line in contents:
-        m = re.match("^.*?([^\s]*\.ipynb)", line)
-        if m:
-            nb_files_use.append(Path("docs/" + m.groups()[0]))
-    nb_files = glob.glob("docs/_case_studies/**/*.ipynb", recursive=True)
-    for file in nb_files:
-        path = Path(file)
-        if path not in nb_files_use:
-            pathlib.Path.unlink(path)
-
-
-@duty
-def docs(ctx):
-    """
-    Build the documentation locally.
-
-    Arguments:
-        ctx: The context instance (passed automatically).
-    """
-    copy_case_studies(ctx)
-    ctx.run("mkdocs build", title="Building documentation")
-
-
-@duty
-def docs_serve(ctx, host="127.0.0.1", port=8000):
-    """
-    Serve the documentation (localhost:8000).
-
-    Arguments:
-        ctx: The context instance (passed automatically).
-        host: The host to serve the docs from.
-        port: The port to serve the docs on.
-    """
-    copy_case_studies(ctx)
-    ctx.run(f"mkdocs serve -a {host}:{port}", title="Serving documentation", capture=False)
-
-
-@duty
-def docs_deploy(ctx):
-    """
-    Deploy the documentation on GitHub pages.
-
-    Arguments:
-        ctx: The context instance (passed automatically).
-    """
-    copy_case_studies
-    ctx.run("mkdocs gh-deploy", title="Deploying documentation")
-
 
 @duty
 def format(ctx):
diff --git a/examples/issues/151.py b/examples/issues/151.py
index d40942fb..503031b8 100644
--- a/examples/issues/151.py
+++ b/examples/issues/151.py
@@ -35,3 +35,5 @@
 print("************")
 print(c1)
 print(conts[0])
+
+print(c1 == conts[1])
\ No newline at end of file
diff --git a/examples/wip/polyhedra_contracts/polyhedral-contract-example.py b/examples/wip/polyhedra_contracts/polyhedral-contract-example.py
index af5d7e55..037b4a76 100644
--- a/examples/wip/polyhedra_contracts/polyhedral-contract-example.py
+++ b/examples/wip/polyhedra_contracts/polyhedral-contract-example.py
@@ -2,7 +2,7 @@
 from pacti.iocontract import IoContract, Var
 from pacti.terms.polyhedra import *
 
-def input2output(i: str, outputs: list[Var], varPrefixes: list[str]) -> str:
+def input2output(i: str, outputs: List[Var], varPrefixes: List[str]) -> str:
   for o in outputs:
     for p in varPrefixes:
       if i.startswith(p) & o.name.startswith(p):
@@ -12,7 +12,7 @@ def input2output(i: str, outputs: list[Var], varPrefixes: list[str]) -> str:
 
 varPrefixes=["t", "soc", "d", "e", "r"]
 
-def connect(c1: IoContract, c2: IoContract, varPrefixes: list[str]) -> IoContract:
+def connect(c1: IoContract, c2: IoContract, varPrefixes: List[str]) -> IoContract:
     c12 = PolyhedralContract.from_string(
       input_vars = list(map(lambda x: x.name, c1.outputvars)),
       output_vars = list(map(lambda x: x.name, c2.inputvars)),
@@ -21,7 +21,7 @@ def connect(c1: IoContract, c2: IoContract, varPrefixes: list[str]) -> IoContrac
 
     return c1.compose(c12).compose(c2)
 
-def initial_contract() -> tuple[int, PolyhedralContract]:
+def initial_contract() -> Tuple[int, PolyhedralContract]:
   e=1
   spec = PolyhedralContract.from_string(
     input_vars = [],
@@ -43,7 +43,7 @@ def initial_contract() -> tuple[int, PolyhedralContract]:
   )
   return e, spec
 
-def SBO_contract(s: int, duration: float, generation: float, consumption: float, improvement: float) -> tuple[int, PolyhedralContract]:
+def SBO_contract(s: int, duration: float, generation: float, consumption: float, improvement: float) -> Tuple[int, PolyhedralContract]:
   e = s+1
   spec = PolyhedralContract.from_string(
     input_vars = [
diff --git a/jupytext.toml b/jupytext.toml
deleted file mode 100644
index 851a6858..00000000
--- a/jupytext.toml
+++ /dev/null
@@ -1,2 +0,0 @@
-[tool.jupytext]
-formats = "case_studies///ipynb,tests/case_studies///py:percent"
diff --git a/mkdocs.yml b/mkdocs.yml
deleted file mode 100644
index c93e358b..00000000
--- a/mkdocs.yml
+++ /dev/null
@@ -1,123 +0,0 @@
-site_name: "Pacti"
-site_description: "Compositional system analysis and design using contracts."
-site_url: "https://FormalSystems.github.io/pacti"
-repo_url: "https://github.com/FormalSystems/pacti"
-repo_name: ""
-site_dir: "site"
-watch: [README.md, CONTRIBUTING.md, CHANGELOG.md, src/pacti]
-
-nav:
-- Home:
-  - Overview: index.md
-  - Installing: installing.md
-  - Getting Started: getting_started.ipynb
-  - Changelog: changelog.md
-  - Credits: credits.md
-  - License: license.md
-# defer to gen-files + literate-nav
-- Case Studies:
-  - Overview: case_studies.md
-  - Autonomous Systems:
-    - From saved data: _case_studies/evaluating_perception/saved_results.ipynb
-    - Full demonstration: _case_studies/evaluating_perception/recompute.ipynb
-  - Multi-agent Coordination: _case_studies/multiagent_coordination/multiagent.ipynb
-  - Signal Processing in Digital ICs: _case_studies/digital_signal_processing/dsp_wl.ipynb
-  - Synthetic Biology: _case_studies/biocircuit_specifications/specification_based_synthetic_biology.ipynb
-  - Space Mission Scenario: 
-    - Overview: _case_studies/space_mission/space_mission.ipynb
-    - Power Viewpoint: _case_studies/space_mission/space_mission_power.ipynb
-    - Science & Communication Viewpoint: _case_studies/space_mission/space_mission_science.ipynb
-    - Navigation Viewpoint: _case_studies/space_mission/space_mission_navigation.ipynb
-    - Thermal Viewpoint: _case_studies/space_mission/space_mission_thermal.ipynb
-    - Schedulability Analysis with 3 Viewpoints: _case_studies/space_mission/space_mission_3viewpoints.ipynb
-  - Mars 2020 Entry-Descent-Landing: _case_studies/mars_entry_descent_landing/mars_edl_2nd_encoding.ipynb
-- API: #reference/
-  - IoContract: iocontract.md
-  - PolyhedralTerms : Polyhedral.md
-- Development:
-  - Contributing: contributing.md
-  - Coverage report: coverage.md
-
-
-theme:
-  name: material
-  features:
-  - navigation.tabs
-  - navigation.tabs.sticky
-  - navigation.top
-#  - toc.integrate
-  icon:
-    repo: fontawesome/brands/github
-  font:
-    #text: Eczar
-    #text: Alegreya Sans
-    #text: Roboto Slab
-    #text: Inknut Antiqua
-    text: Libre Baskerville
-    #text: Cardo
-    code: Roboto Mono
-    #text: Merriweather
-    #code: Inconsolata
-  palette:
-    scheme: default
-    primary: white
-    accent: purple
-  logo: pacti_small_icon.svg
-#  - media: "(prefers-color-scheme: light)"
-#    scheme: default
-#    primary: teal
-#    accent: purple
-#    toggle:
-#      icon: material/weather-sunny
-#      name: Switch to dark mode
-#  - media: "(prefers-color-scheme: dark)"
-#    scheme: slate
-#    primary: black
-#    accent: lime
-#    toggle:
-#      icon: material/weather-night
-#      name: Switch to light mode
-
-extra_css:
-- css/material.css
-- css/mkdocstrings.css
-
-markdown_extensions:
-  - pymdownx.arithmatex:
-      generic: true
-  - admonition
-  - callouts
-  - pymdownx.emoji
-  - pymdownx.magiclink
-  - pymdownx.snippets:
-      check_paths: true
-  - pymdownx.superfences
-  - pymdownx.tabbed:
-      alternate_style: true
-  - pymdownx.tasklist
-  - toc:
-      permalink: true
-
-extra_javascript:
-  - javascripts/mathjax.js
-  - https://polyfill.io/v3/polyfill.min.js?features=es6
-  - https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js
-
-plugins:
-- search
-- mkdocs-jupyter
-- mkdocs-video
-- markdown-exec
-- gen-files:
-    scripts:
-    - docs/gen_ref_nav.py
-- literate-nav:
-    nav_file: SUMMARY.md
-- coverage
-- section-index
-- mkdocstrings
-
-extra:
-  social:
-  #- icon: fontawesome/brands/github
-  #  link: https://github.com/FormalSystems
diff --git a/pyproject.toml b/pyproject.toml
index 66c1b467..2d894cac 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -6,7 +6,7 @@ build-backend = "pdm.pep517.api"
 name = "Pacti"
 description = "pacti-description"
 authors = [{name = "pacti-authors-name", email = "pacti-authors-email"}]
-license = "BSD-2-Clause"
+license = "BSD-3-Clause"
 readme = "README.md"
 keywords = []
 dynamic = ["version"]
@@ -16,11 +16,8 @@ dependencies = [
     "numpy>=1.24.1",
     "matplotlib>=3.6.2",
     "typing-extensions>=4.5.0",
-    "joblib>=1.2.0",
-    "ipykernel>=6.21.3",
-    "ipympl>=0.9.3",
 ]
-requires-python = ">=3.8, <=3.11.1"
+requires-python = ">=3.8, <3.12"
 
 [project.scripts]
 #pacti = "pacti.cli:main"
@@ -37,20 +34,7 @@ editable-backend = "editables"
 
 [tool.pdm.dev-dependencies]
 duty = ["duty>=0.7"]
-docs = [
-    "mkdocs>=1.3",
-    "mkdocs-jupyter>=0.22,<0.23",
-    "mkdocs-coverage>=0.2",
-    "mkdocs-gen-files>=0.3",
-    "mkdocs-literate-nav>=0.4",
-    "mkdocs-material>=8.1",
-    "mkdocs-section-index>=0.3",
-    "mkdocs-video>=1.3.0",
-    "mkdocstrings[python]>=0.18",
-    "markdown-callouts>=0.2",
-    "markdown-exec>=0.5",
-    "toml>=0.10",
-]
+
 format = [
     "autoflake>=1.4",
     "black>=21.10b0",
@@ -91,7 +75,7 @@ typing = [
 security = ["safety>=2"]
 dev = [
     "certifi>=2022.9.24",
-    "tox-pdm>=0.6.1",
+    "tox>=4.4.7",
 ]
 
 [tool.black]
@@ -100,7 +84,7 @@ exclude = "tests/fixtures"
 
 [tool.isort]
 line_length = 120
-not_skip = "__init__.py"
+#not_skip = "__init__.py"
 multi_line_output = 3
 force_single_line = false
 balanced_wrapping = true
diff --git a/src/pacti/iocontract/compundiocontract.py b/src/pacti/iocontract/compundiocontract.py
index d019ad10..ba5edf04 100644
--- a/src/pacti/iocontract/compundiocontract.py
+++ b/src/pacti/iocontract/compundiocontract.py
@@ -3,12 +3,13 @@
 from __future__ import annotations
 
 import logging
-from typing import Generic, List, TypeVar, Union
+from typing import Dict, Generic, List, TypeVar, Union
 
 from pacti.iocontract.iocontract import TermList_t, Var
 from pacti.utils.lists import list_diff, list_intersection, list_union
 
 NestedTermlist_t = TypeVar("NestedTermlist_t", bound="NestedTermList")
+IoContractCompound_t = TypeVar("IoContractCompound_t", bound="IoContractCompound")
 numeric = Union[int, float]
 
 
@@ -16,7 +17,7 @@ class NestedTermList:
     """A collection of termlists interpreted as their disjunction."""
 
     def __init__(  # noqa: WPS231 too much cognitive complexity
-        self, nested_termlist: list[TermList_t], force_empty_intersection: bool
+        self, nested_termlist: List[TermList_t], force_empty_intersection: bool
     ):
         """
         Class constructor.
@@ -36,7 +37,7 @@ def __init__(  # noqa: WPS231 too much cognitive complexity
                         intersection = tli | tlj
                         if not intersection.is_empty():
                             raise ValueError("Terms %s and %s have nonempty intersection" % (tli, tlj))
-        self.nested_termlist: list[TermList_t] = []
+        self.nested_termlist: List[TermList_t] = []
         for tl in nested_termlist:
             self.nested_termlist.append(tl.copy())
 
@@ -46,6 +47,24 @@ def __str__(self) -> str:
             return "\nor \n".join(res)
         return "true"
 
+    def __le__(self, other: object) -> bool:  # noqa: WPS231 too much cognitive complexity
+        if not isinstance(other, type(self)):
+            raise ValueError()
+        for this_tl in self.nested_termlist:
+            found = False
+            for that_tl in other.nested_termlist:
+                if this_tl <= that_tl:
+                    found = True
+                    break
+            if not found:
+                return False
+        return True
+
+    def __eq__(self, other: object) -> bool:
+        if not isinstance(other, type(self)):
+            raise ValueError()
+        return self <= other <= self
+
     def simplify(self: NestedTermlist_t, context: NestedTermlist_t, force_empty_intersection: bool) -> NestedTermlist_t:
         """
         Remove redundant terms in nested termlist.
@@ -88,13 +107,13 @@ def intersect(self: NestedTermlist_t, other: NestedTermlist_t, force_empty_inter
         return type(self)(new_nested_tl, force_empty_intersection)
 
     @property
-    def vars(self) -> list[Var]:  # noqa: A003
+    def vars(self) -> List[Var]:  # noqa: A003
         """The list of variables contained in this nested termlist.
 
         Returns:
             List of variables referenced in nested termlist.
         """
-        varlist: list[Var] = []
+        varlist: List[Var] = []
         for tl in self.nested_termlist:
             varlist = list_union(varlist, tl.vars)
         return varlist
@@ -111,7 +130,7 @@ def copy(self: NestedTermlist_t, force_empty_intersection: bool) -> NestedTermli
         """
         return type(self)([tl.copy() for tl in self.nested_termlist], force_empty_intersection)
 
-    def contains_behavior(self, behavior: dict[Var, numeric]) -> bool:
+    def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
         """
         Tell whether constraints contain the given behavior.
 
@@ -224,7 +243,17 @@ def __str__(self) -> str:
             + str(self.g)
         )
 
-    def merge(self, other: IoContractCompound) -> IoContractCompound:
+    def __eq__(self, other: object) -> bool:
+        if not isinstance(other, type(self)):
+            raise ValueError
+        return (
+            self.inputvars == other.inputvars
+            and self.outputvars == self.outputvars
+            and self.a == other.a
+            and self.g == other.g
+        )
+
+    def merge(self: IoContractCompound_t, other: IoContractCompound_t) -> IoContractCompound_t:
         """
         Compute the merging operation for two contracts.
 
diff --git a/src/pacti/iocontract/iocontract.py b/src/pacti/iocontract/iocontract.py
index 01ad88b6..8af0c883 100644
--- a/src/pacti/iocontract/iocontract.py
+++ b/src/pacti/iocontract/iocontract.py
@@ -81,7 +81,7 @@ class Term(ABC):
 
     @property
     @abstractmethod
-    def vars(self) -> list[Var]:  # noqa: A003
+    def vars(self) -> List[Var]:  # noqa: A003
         """Variables contained in the syntax of the term."""
 
     @abstractmethod
@@ -149,13 +149,13 @@ def __init__(self, term_list: Optional[List] = None):
             self.terms = []
 
     @property
-    def vars(self) -> list[Var]:  # noqa: A003
+    def vars(self) -> List[Var]:  # noqa: A003
         """The list of variables contained in this list of terms.
 
         Returns:
             List of variables referenced in the term.
         """
-        varlist: list[Var] = []
+        varlist: List[Var] = []
         for t in self.terms:
             varlist = list_union(varlist, t.vars)
         return varlist
@@ -199,6 +199,10 @@ def __sub__(self: TermList_t, other: TermList_t) -> TermList_t:
     def __le__(self: TermList_t, other: TermList_t) -> bool:
         return self.refines(other)
 
+    @abstractmethod
+    def __hash__(self) -> int:
+        ...
+
     def copy(self: TermList_t) -> TermList_t:
         """
         Makes copy of termlist.
@@ -388,7 +392,7 @@ def __init__(
         self.g = guarantees.simplify(self.a)
 
     @property
-    def vars(self) -> list[Var]:  # noqa: A003
+    def vars(self) -> List[Var]:  # noqa: A003
         """
         The list of variables in the interface of the contract.
 
@@ -424,6 +428,9 @@ def __eq__(self, other: object) -> bool:
             and self.g == other.g
         )
 
+    def __hash__(self) -> int:
+        return hash((tuple(self.inputvars), tuple(self.outputvars), self.a, self.g))
+
     def rename_variable(  # noqa: WPS231 too much cognitive complexity
         self: IoContract_t, source_var: Var, target_var: Var
     ) -> IoContract_t:
diff --git a/src/pacti/terms/polyhedra/plots.py b/src/pacti/terms/polyhedra/plots.py
index be0624a0..324ab0c9 100644
--- a/src/pacti/terms/polyhedra/plots.py
+++ b/src/pacti/terms/polyhedra/plots.py
@@ -2,7 +2,7 @@
 
 
 from math import atan2
-from typing import Union
+from typing import Dict, Tuple, Union
 
 import matplotlib.pyplot as plt  # noqa: WPS301 Found dotted raw import
 import numpy as np
@@ -23,9 +23,9 @@ def plot_assumptions(
     contract: PolyhedralContract,
     x_var: Var,
     y_var: Var,
-    var_values: dict[Var, numeric],
-    x_lims: tuple[numeric, numeric],
-    y_lims: tuple[numeric, numeric],
+    var_values: Dict[Var, numeric],
+    x_lims: Tuple[numeric, numeric],
+    y_lims: Tuple[numeric, numeric],
 ) -> MplFigure:
     """
     Plots the assumptions of an IoContract with polyhedral terms.
@@ -61,9 +61,9 @@ def plot_guarantees(
     contract: PolyhedralContract,
     x_var: Var,
     y_var: Var,
-    var_values: dict[Var, numeric],
-    x_lims: tuple[numeric, numeric],
-    y_lims: tuple[numeric, numeric],
+    var_values: Dict[Var, numeric],
+    x_lims: Tuple[numeric, numeric],
+    y_lims: Tuple[numeric, numeric],
 ) -> MplFigure:
     """
     Plots the guarantees and assumptions of an IoContract with polyhedral terms.
@@ -96,7 +96,7 @@ def plot_guarantees(
 
 
 def _substitute_in_termlist(  # noqa: WPS231
-    constraints: PolyhedralTermList, var_values: dict[Var, numeric]
+    constraints: PolyhedralTermList, var_values: Dict[Var, numeric]
 ) -> PolyhedralTermList:
     plot_list = []
     for term in constraints.terms:
@@ -128,7 +128,7 @@ def _get_feasible_point(a_mat: np.ndarray, b: np.ndarray, interior: bool = True)
 
 
 # given a bounded polygon, return its vertices
-def _get_bounding_vertices(a_mat: np.ndarray, b: np.ndarray) -> tuple[tuple, tuple]:
+def _get_bounding_vertices(a_mat: np.ndarray, b: np.ndarray) -> Tuple[tuple, tuple]:
     try:
         interior_point = _get_feasible_point(a_mat, b)
     except ValueError as e:
@@ -157,7 +157,7 @@ def _get_bounding_vertices(a_mat: np.ndarray, b: np.ndarray) -> tuple[tuple, tup
 
 
 def _gen_boundary_constraints(
-    x_var: Var, y_var: Var, x_lims: tuple[numeric, numeric], y_lims: tuple[numeric, numeric]
+    x_var: Var, y_var: Var, x_lims: Tuple[numeric, numeric], y_lims: Tuple[numeric, numeric]
 ) -> PolyhedralTermList:
     constraints = [PolyhedralTerm({x_var: 1}, x_lims[1])]
     constraints.append(PolyhedralTerm({x_var: -1}, -x_lims[0]))
@@ -170,9 +170,9 @@ def _plot_constraints(
     constraints: PolyhedralTermList,
     x_var: Var,
     y_var: Var,
-    var_values: dict[Var, numeric],
-    x_lims: tuple[numeric, numeric],
-    y_lims: tuple[numeric, numeric],
+    var_values: Dict[Var, numeric],
+    x_lims: Tuple[numeric, numeric],
+    y_lims: Tuple[numeric, numeric],
 ) -> MplFigure:
     if not isinstance(constraints, PolyhedralTermList):
         raise ValueError("Expecting polyhedral constraints. Constraint type: %s" % (type(constraints)))
diff --git a/src/pacti/terms/polyhedra/polyhedra.py b/src/pacti/terms/polyhedra/polyhedra.py
index d64b4f76..4603d37a 100644
--- a/src/pacti/terms/polyhedra/polyhedra.py
+++ b/src/pacti/terms/polyhedra/polyhedra.py
@@ -8,7 +8,7 @@
 from __future__ import annotations
 
 import logging
-from typing import Any, Optional, Tuple, Union
+from typing import Any, Dict, List, Optional, Tuple, Union
 
 import numpy as np
 import sympy
@@ -28,7 +28,7 @@ class PolyhedralTerm(Term):
     # values are the coefficients of those variables in the term, and (b) a
     # constant. The term is assumed to be in the form \Sigma_i a_i v_i +
     # constant <= 0
-    def __init__(self, variables: dict[Var, numeric], constant: numeric):
+    def __init__(self, variables: Dict[Var, numeric], constant: numeric):
         """
         Constructor for PolyhedralTerm.
 
@@ -122,7 +122,7 @@ def rename_variable(self, source_var: Var, target_var: Var) -> PolyhedralTerm:
         return new_term
 
     @property
-    def vars(self) -> list[Var]:  # noqa: A003
+    def vars(self) -> List[Var]:  # noqa: A003
         """
         Variables appearing in term with a nonzero coefficient.
 
@@ -205,7 +205,7 @@ def get_sign(self, var: Var) -> int:  # noqa: VNE002
             return 1
         return -1
 
-    def get_matching_vars(self, variable_polarity: dict[Var, bool]) -> list[Var]:
+    def get_matching_vars(self, variable_polarity: Dict[Var, bool]) -> List[Var]:
         """
         Get list of variables whose polarities match the polarities requested.
 
@@ -392,7 +392,7 @@ def to_term(expression: sympy.core.expr.Expr) -> PolyhedralTerm:
         return PolyhedralTerm(variable_dict, constant)
 
     @staticmethod
-    def term_to_polytope(term: PolyhedralTerm, variable_list: list[Var]) -> Tuple[list[numeric], numeric]:
+    def term_to_polytope(term: PolyhedralTerm, variable_list: List[Var]) -> Tuple[List[numeric], numeric]:
         """
         Transform a term into a vector according to the given order.
 
@@ -416,7 +416,7 @@ def term_to_polytope(term: PolyhedralTerm, variable_list: list[Var]) -> Tuple[li
         return coeffs, term.constant
 
     @staticmethod
-    def polytope_to_term(poly: list[numeric], const: numeric, variables: list[Var]) -> PolyhedralTerm:
+    def polytope_to_term(poly: List[numeric], const: numeric, variables: List[Var]) -> PolyhedralTerm:
         """
         Transform a list of coefficients and variables into a PolyhedralTerm.
 
@@ -435,7 +435,7 @@ def polytope_to_term(poly: list[numeric], const: numeric, variables: list[Var])
         return PolyhedralTerm(variable_dict, const)
 
     @staticmethod
-    def solve_for_variables(context: PolyhedralTermList, vars_to_elim: list[Var]) -> dict:
+    def solve_for_variables(context: PolyhedralTermList, vars_to_elim: List[Var]) -> dict:
         """
         Interpret termlist as equality and solve system of equations.
 
@@ -469,7 +469,7 @@ def solve_for_variables(context: PolyhedralTermList, vars_to_elim: list[Var]) ->
 class PolyhedralTermList(TermList):  # noqa: WPS338
     """A TermList of PolyhedralTerm instances."""
 
-    def __init__(self, terms: Optional[list[PolyhedralTerm]] = None):
+    def __init__(self, terms: Optional[List[PolyhedralTerm]] = None):
         """
         Constructor for PolyhedralTermList.
 
@@ -504,7 +504,10 @@ def __str__(self) -> str:
         res += "\n]"
         return res
 
-    def to_str_list(self) -> list[str]:
+    def __hash__(self) -> int:
+        return hash(tuple(self.terms))
+
+    def to_str_list(self) -> List[str]:
         """
         Convert termlist into a list of strings.
 
@@ -519,7 +522,7 @@ def to_str_list(self) -> list[str]:
             ts = rest
         return str_list
 
-    def evaluate(self, var_values: dict[Var, numeric]) -> PolyhedralTermList:  # noqa: WPS231
+    def evaluate(self, var_values: Dict[Var, numeric]) -> PolyhedralTermList:  # noqa: WPS231
         """
         Replace variables in termlist with given values.
 
@@ -550,7 +553,7 @@ def evaluate(self, var_values: dict[Var, numeric]) -> PolyhedralTermList:  # noq
             new_list.append(new_term)
         return PolyhedralTermList(new_list)
 
-    def contains_behavior(self, behavior: dict[Var, numeric]) -> bool:
+    def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
         """
         Tell whether TermList contains the given behavior.
 
@@ -612,7 +615,7 @@ def elim_vars_by_refining(self, context: PolyhedralTermList, vars_to_elim: list)
             return termlist._transform(context=context, vars_to_elim=vars_to_elim, refine=True)
         except ValueError as e:
             raise ValueError(
-                "The elimination of variables \n{}\n".format(vars_to_elim)
+                "The elimination of variables \n{}\n".format([str(x) for x in vars_to_elim])
                 + "by refining terms \n{}\n".format(self)
                 + "in context \n{}\n".format(context)
                 + "was not possible"
@@ -666,7 +669,7 @@ def elim_vars_by_relaxing(self, context: PolyhedralTermList, vars_to_elim: list)
             termlist = termlist._transform(context=context, vars_to_elim=vars_to_elim, refine=False)
         except ValueError as e:
             raise ValueError(
-                "The elimination of variables \n{}\n".format(vars_to_elim)
+                "The elimination of variables \n{}\n".format([str(x) for x in vars_to_elim])
                 + "by relaxing terms \n{}\n".format(self)
                 + "in context \n{}\n".format(context)
                 + "was not possible"
@@ -767,8 +770,7 @@ def _transform(self, context: PolyhedralTermList, vars_to_elim: list, refine: bo
         for i, term in enumerate(term_list):
             copy_new_terms = new_terms.copy()
             copy_new_terms.terms.remove(term)
-            helpers = (context | copy_new_terms)
-            #del helpers.terms[len(context.terms) + i]
+            helpers = context | copy_new_terms
             try:
                 new_term = PolyhedralTermList._transform_term(term, helpers, vars_to_elim, refine)
             except ValueError:
@@ -782,7 +784,7 @@ def _transform(self, context: PolyhedralTermList, vars_to_elim: list, refine: bo
         logging.debug("Ending transformation with simplification")
         return that.simplify(context)
 
-    def optimize(self, objective: dict[Var, numeric], maximize: bool = True) -> Optional[numeric]:
+    def optimize(self, objective: Dict[Var, numeric], maximize: bool = True) -> Optional[numeric]:
         """
         Optimizes a linear expression in the feasible region of the termlist.
 
@@ -820,7 +822,7 @@ def optimize(self, objective: dict[Var, numeric], maximize: bool = True) -> Opti
     @staticmethod
     def termlist_to_polytope(
         terms: PolyhedralTermList, context: PolyhedralTermList
-    ) -> Tuple[list[Var], np.ndarray, np.ndarray, np.ndarray, np.ndarray]:
+    ) -> Tuple[List[Var], np.ndarray, np.ndarray, np.ndarray, np.ndarray]:
         """
         Converts a list of terms with its context into matrix-vector pairs.
 
@@ -870,7 +872,7 @@ def termlist_to_polytope(
         return variables, np.array(a), np.array(b), a_h_ret, np.array(b_h)
 
     @staticmethod
-    def polytope_to_termlist(matrix: np.ndarray, vector: np.ndarray, variables: list[Var]) -> PolyhedralTermList:
+    def polytope_to_termlist(matrix: np.ndarray, vector: np.ndarray, variables: List[Var]) -> PolyhedralTermList:
         """
         Transforms a matrix-vector pair into a PolyhedralTermList.
 
@@ -955,25 +957,21 @@ def reduce_polytope(  # noqa: WPS231
         while i < n:
             objective = a_temp[i, :] * -1
             b_temp[i] += 1
-            # logging.debug("Optimization objective: \n%s", objective)
-            # logging.debug("a_temp is \n%s", a_temp)
-            # logging.debug("a_help is \n%s", a_help)
-            # logging.debug("b_temp is \n%s", b_temp)
-            # logging.debug("b_help is \n%s", b_help)
             if helper_present:
                 a_opt = np.concatenate((a_temp, a_help), axis=0)
                 b_opt = np.concatenate((b_temp, b_help))
             else:
                 a_opt = a_temp
                 b_opt = b_temp
+            # Linprog's status values
+            # 0 : Optimization proceeding nominally.
+            # 1 : Iteration limit reached.
+            # 2 : Problem appears to be infeasible.
+            # 3 : Problem appears to be unbounded.
+            # 4 : Numerical difficulties encountered.
             res = linprog(c=objective, A_ub=a_opt, b_ub=b_opt, bounds=(None, None))  # ,options={'tol':0.000001})
             b_temp[i] -= 1
-            if res["fun"]:
-                ...
-                # logging.debug("Optimal value: %s", -res["fun"])
-            # logging.debug("Results: %s", res)
-            # if res["success"] and -res["fun"] <= b_temp[i]:
-            if res["status"] != 2 and -res["fun"] <= b_temp[i]:  # noqa: WPS309
+            if res["status"] == 3 or (res["status"] == 0 and -res["fun"] <= b_temp[i]):  # noqa: WPS309
                 logging.debug("Can remove")
                 a_temp = np.delete(a_temp, i, 0)
                 b_temp = np.delete(b_temp, i)
@@ -1100,11 +1098,11 @@ def is_polytope_empty(a: np.ndarray, b: np.ndarray) -> bool:
     @staticmethod
     def _get_kaykobad_context(  # noqa: WPS231
         term: PolyhedralTerm, context: PolyhedralTermList, vars_to_elim: list, refine: bool
-    ) -> Tuple[list[PolyhedralTerm], list[Var]]:
+    ) -> Tuple[List[PolyhedralTerm], List[Var]]:
         forbidden_vars = list_intersection(vars_to_elim, term.vars)
         other_forbibben_vars = list_diff(vars_to_elim, term.vars)
         n = len(forbidden_vars)
-        matrix_row_terms = []  # type: list[PolyhedralTerm]
+        matrix_row_terms = []  # type: List[PolyhedralTerm]
         partial_sums = [float(0) for i in range(n)]
         transform_coeff = -1
         if refine:
@@ -1277,7 +1275,7 @@ def _tactic_3(
 
     @staticmethod
     def _tactic_4(  # noqa: WPS231
-        term: PolyhedralTerm, context: PolyhedralTermList, vars_to_elim: list, refine: bool, no_vars: list[Var]
+        term: PolyhedralTerm, context: PolyhedralTermList, vars_to_elim: list, refine: bool, no_vars: List[Var]
     ) -> PolyhedralTerm:
         logging.debug("************ Tactic 4")
         logging.debug("Vars_to_elim %s \nTerm %s \nContext %s " % (vars_to_elim, term, context))
@@ -1287,8 +1285,8 @@ def _tactic_4(  # noqa: WPS231
         if len(conflict_vars) > 1:
             raise ValueError("Tactic 4 unsuccessful")
         var_to_elim = conflict_vars[0]
-        goal_context: list[PolyhedralTerm] = []
-        useful_context: list[PolyhedralTerm] = []
+        goal_context: List[PolyhedralTerm] = []
+        useful_context: List[PolyhedralTerm] = []
         polarity = -1
         if refine:
             polarity = 1
diff --git a/src/pacti/terms/polyhedra/polyhedral_contract.py b/src/pacti/terms/polyhedra/polyhedral_contract.py
index 09397c3e..167b258e 100644
--- a/src/pacti/terms/polyhedra/polyhedral_contract.py
+++ b/src/pacti/terms/polyhedra/polyhedral_contract.py
@@ -2,24 +2,24 @@
 
 from __future__ import annotations
 
-from typing import Optional, Tuple, TypedDict, Union
+from typing import Dict, List, Optional, Tuple, TypedDict, Union
 
 from pacti.iocontract import IoContract, IoContractCompound, NestedTermList, Var
 from pacti.terms.polyhedra import serializer
 from pacti.terms.polyhedra.polyhedra import PolyhedralTerm, PolyhedralTermList
 
 numeric = Union[int, float]
-ser_pt = dict[str, Union[float, dict[str, float]]]
+ser_pt = Dict[str, Union[float, Dict[str, float]]]
 ser_contract = TypedDict(
     "ser_contract",
-    {"input_vars": list[str], "output_vars": list[str], "assumptions": list[ser_pt], "guarantees": list[ser_pt]},
+    {"input_vars": List[str], "output_vars": List[str], "assumptions": List[ser_pt], "guarantees": List[ser_pt]},
 )
 
 
 class PolyhedralContract(IoContract):
     """IO Contracts with assumptions and guarantees expressed as polyhedral constraints."""
 
-    def rename_variables(self, variable_mappings: list[tuple[str, str]]) -> PolyhedralContract:
+    def rename_variables(self, variable_mappings: List[Tuple[str, str]]) -> PolyhedralContract:
         """
         Rename variables in a contract.
 
@@ -43,14 +43,14 @@ def to_machine_dict(self) -> ser_contract:
         """
         input_vars = [str(x) for x in self.inputvars]
         output_vars = [str(x) for x in self.outputvars]
-        assumptions: list[ser_pt] = [
+        assumptions: List[ser_pt] = [
             {
                 "constant": float(term.constant),
                 "coefficients": {str(k): float(v) for k, v in term.variables.items()},
             }
             for term in self.a.terms
         ]
-        guarantees: list[ser_pt] = [
+        guarantees: List[ser_pt] = [
             {
                 "constant": float(term.constant),
                 "coefficients": {str(k): float(v) for k, v in term.variables.items()},
@@ -81,10 +81,10 @@ def to_dict(self) -> dict:
 
     @staticmethod
     def from_string(
-        assumptions: list[str],
-        guarantees: list[str],
-        input_vars: list[str],
-        output_vars: list[str],
+        assumptions: List[str],
+        guarantees: List[str],
+        input_vars: List[str],
+        output_vars: List[str],
     ) -> PolyhedralContract:
         """
         Create contract from several lists of strings.
@@ -98,11 +98,11 @@ def from_string(
         Returns:
             A polyhedral contract built from the arguments provided.
         """
-        a: list[PolyhedralTerm] = []
+        a: List[PolyhedralTerm] = []
         if assumptions:
             a = [item for x in assumptions for item in serializer.polyhedral_termlist_from_string(x)]
 
-        g: list[PolyhedralTerm] = []
+        g: List[PolyhedralTerm] = []
         if guarantees:
             g = [item for x in guarantees for item in serializer.polyhedral_termlist_from_string(x)]
 
@@ -160,7 +160,7 @@ def from_dict(contract: dict) -> PolyhedralContract:
             guarantees=g,
         )
 
-    def compose(self, other: PolyhedralContract, vars_to_keep: Optional[list[str]] = None) -> PolyhedralContract:
+    def compose(self, other: PolyhedralContract, vars_to_keep: Optional[List[str]] = None) -> PolyhedralContract:
         """Compose polyhedral contracts.
 
         Compute the composition of the two given contracts and abstract the
@@ -222,7 +222,7 @@ class NestedPolyhedra(NestedTermList):
     """A collection of polyhedral termlists interpreted as their disjunction."""
 
     def __init__(  # noqa: WPS612 useless overwritten __init__
-        self, nested_termlist: list[PolyhedralTermList], force_empty_intersection: bool
+        self, nested_termlist: List[PolyhedralTermList], force_empty_intersection: bool
     ):
         """
         Class constructor.
@@ -252,10 +252,10 @@ class PolyhedralContractCompound(IoContractCompound):
 
     @staticmethod
     def from_string(
-        assumptions: list[list[str]],
-        guarantees: list[list[str]],
-        input_vars: list[str],
-        output_vars: list[str],
+        assumptions: List[list[str]],
+        guarantees: List[list[str]],
+        input_vars: List[str],
+        output_vars: List[str],
     ) -> PolyhedralContractCompound:
         """
         Create contract from several lists of strings.
@@ -269,13 +269,13 @@ def from_string(
         Returns:
             A polyhedral contract built from the arguments provided.
         """
-        a: list[PolyhedralTermList] = []
+        a: List[PolyhedralTermList] = []
         if assumptions:
             for termlist_str in assumptions:
                 a_termlist = [item for x in termlist_str for item in serializer.polyhedral_termlist_from_string(x)]
                 a.append(PolyhedralTermList(a_termlist))
 
-        g: list[PolyhedralTermList] = []
+        g: List[PolyhedralTermList] = []
         if guarantees:
             for termlist_str in guarantees:
                 g_termlist = [item for x in termlist_str for item in serializer.polyhedral_termlist_from_string(x)]
diff --git a/src/pacti/terms/polyhedra/serializer.py b/src/pacti/terms/polyhedra/serializer.py
index e810bec2..c7cbaffb 100644
--- a/src/pacti/terms/polyhedra/serializer.py
+++ b/src/pacti/terms/polyhedra/serializer.py
@@ -1,6 +1,6 @@
 """Transformations between polyhedral structures and strings."""
 import re
-from typing import Dict, Tuple, Union
+from typing import Dict, List, Match, Tuple, Union
 
 import numpy as np
 import sympy
@@ -119,8 +119,8 @@ def _lhs_str(term: PolyhedralTerm) -> str:  # noqa: WPS231
 
 
 def polyhedral_term_list_to_strings(  # noqa: WPS231 too much cognitive complexity
-    terms: list[PolyhedralTerm],
-) -> Tuple[str, list[PolyhedralTerm]]:
+    terms: List[PolyhedralTerm],
+) -> Tuple[str, List[PolyhedralTerm]]:
     """
     Convert a list of polyhedral terms into a list of strings, one term at a time.
 
@@ -273,7 +273,7 @@ def _internal_parse_constant(val: str) -> numeric:
     return n
 
 
-def _internal_add_variable(terms: str, variables: dict[str, numeric], v: str, c: str) -> None:
+def _internal_add_variable(terms: str, variables: Dict[str, numeric], v: str, c: str) -> None:
     if v in variables:
         raise (ValueError(f"Multiple coefficients involving the same variable: {v} in: {terms}"))
 
@@ -281,7 +281,7 @@ def _internal_add_variable(terms: str, variables: dict[str, numeric], v: str, c:
     variables.update({v: n})
 
 
-def _internal_parse_variables(variables: dict[str, numeric], terms: str) -> None:
+def _internal_parse_variables(variables: Dict[str, numeric], terms: str) -> None:
     t = internal_variable_pattern.match(terms)
     if not t:
         raise (ValueError(f"Polyhedral variable syntax mismatch: {terms}"))
@@ -297,8 +297,8 @@ def _internal_parse_variables(variables: dict[str, numeric], terms: str) -> None
         variables
 
 
-def _internal_pt_from_canonical_match(m: re.Match[str]) -> PolyhedralTerm:
-    variables: dict[str, numeric] = {}
+def _internal_pt_from_canonical_match(m: Match[str]) -> PolyhedralTerm:
+    variables: Dict[str, numeric] = {}
 
     v = m.group("variable")
     c = m.group("coefficient")
@@ -316,7 +316,7 @@ def _internal_pt_from_canonical_match(m: re.Match[str]) -> PolyhedralTerm:
 # pos: LHS <= RHS
 # neg: -(LHS) <= RHS
 # result is [pos,neg]
-def _internal_pt_from_absolute_less_than_match(m: re.Match[str]) -> list[PolyhedralTerm]:
+def _internal_pt_from_absolute_less_than_match(m: Match[str]) -> List[PolyhedralTerm]:
     s1 = f"{m.group('LHS')} <= {m.group('RHS')}"
     m1 = internal_polyhedral_term_canonical_pattern.match(s1)
     if not m1:
@@ -333,7 +333,7 @@ def _internal_pt_from_absolute_less_than_match(m: re.Match[str]) -> list[Polyhed
 # pos: LHS <= 0
 # neg: -(LHS) <= 0
 # result is [pos,neg]
-def _internal_pt_from_absolute_zero_match(m: re.Match[str]) -> list[PolyhedralTerm]:
+def _internal_pt_from_absolute_zero_match(m: Match[str]) -> List[PolyhedralTerm]:
     s1 = f"{m.group('LHS')} <= 0"
     m1 = internal_polyhedral_term_canonical_pattern.match(s1)
     if not m1:
@@ -350,7 +350,7 @@ def _internal_pt_from_absolute_zero_match(m: re.Match[str]) -> list[PolyhedralTe
 # pos: LHS <= RHS
 # neg: -(LHS) <= -(RHS)
 # result is [pos,neg]
-def _internal_pt_from_equality_match(m: re.Match[str]) -> list[PolyhedralTerm]:
+def _internal_pt_from_equality_match(m: Match[str]) -> List[PolyhedralTerm]:
     s1 = f"{m.group('LHS')} <= {m.group('RHS')}"
     m1 = internal_polyhedral_term_canonical_pattern.match(s1)
     if not m1:
@@ -364,7 +364,7 @@ def _internal_pt_from_equality_match(m: re.Match[str]) -> list[PolyhedralTerm]:
     return [pos, neg]
 
 
-def polyhedral_termlist_from_string(str_rep: str) -> list[PolyhedralTerm]:
+def polyhedral_termlist_from_string(str_rep: str) -> List[PolyhedralTerm]:
     """
     Transform a linear expression into a polyhedral termlist.
 
diff --git a/src/pacti/utils/fileio.py b/src/pacti/utils/fileio.py
index c1a84f00..a4a10850 100644
--- a/src/pacti/utils/fileio.py
+++ b/src/pacti/utils/fileio.py
@@ -2,14 +2,14 @@
 
 import json
 import os
-from typing import Any, Tuple
+from typing import Any, Dict, List, Tuple
 
 from pacti.terms import polyhedra
 
 
 def read_contracts_from_file(  # noqa: WPS231 too much cognitive complexity
     file_name: str,
-) -> Tuple[list[polyhedra.PolyhedralContract], list[str]]:
+) -> Tuple[List[polyhedra.PolyhedralContract], List[str]]:
     """
     Read contracts from a file.
 
@@ -32,7 +32,7 @@ def read_contracts_from_file(  # noqa: WPS231 too much cognitive complexity
         assert isinstance(entry, dict)
         assert "type" in entry
     # we load each contract according to the type
-    contracts = []
+    contracts: List[Any] = []
     names = []
     for entry in file_data:
         if entry["type"] == "PolyhedralContract_machine":
@@ -51,8 +51,8 @@ def read_contracts_from_file(  # noqa: WPS231 too much cognitive complexity
 
 
 def write_contracts_to_file(  # noqa: WPS231 too much cognitive complexity
-    contracts: list[polyhedra.PolyhedralContract],
-    names: list[str],
+    contracts: List[polyhedra.PolyhedralContract],
+    names: List[str],
     file_name: str,
     machine_representation: bool = False,
 ) -> None:
@@ -71,7 +71,7 @@ def write_contracts_to_file(  # noqa: WPS231 too much cognitive complexity
     data = []
     assert len(contracts) == len(names)
     for i, c in enumerate(contracts):
-        entry: dict[str, Any] = {}
+        entry: Dict[str, Any] = {}
         if isinstance(c, polyhedra.PolyhedralContract):
             entry["name"] = names[i]
             if machine_representation:
diff --git a/src/pacti/utils/lists.py b/src/pacti/utils/lists.py
index 9340d4f5..c2aa5891 100644
--- a/src/pacti/utils/lists.py
+++ b/src/pacti/utils/lists.py
@@ -1,9 +1,9 @@
 """Some list operations."""
 
-from typing import Any
+from typing import Any, List
 
 
-def list_intersection(list1: list[Any], list2: list[Any]) -> list[Any]:
+def list_intersection(list1: List[Any], list2: List[Any]) -> List[Any]:
     """
     Intersect two lists.
 
@@ -17,7 +17,7 @@ def list_intersection(list1: list[Any], list2: list[Any]) -> list[Any]:
     return [el for el in list1 if el in list2]
 
 
-def list_diff(list1: list[Any], list2: list[Any]) -> list[Any]:
+def list_diff(list1: List[Any], list2: List[Any]) -> List[Any]:
     """
     Compute difference between lists.
 
@@ -31,7 +31,7 @@ def list_diff(list1: list[Any], list2: list[Any]) -> list[Any]:
     return [el for el in list1 if (el not in list2)]
 
 
-def list_union(list1: list[Any], list2: list[Any]) -> list[Any]:
+def list_union(list1: List[Any], list2: List[Any]) -> List[Any]:
     """
     Compute the union of two lists.
 
@@ -45,7 +45,7 @@ def list_union(list1: list[Any], list2: list[Any]) -> list[Any]:
     return list1 + [el for el in list2 if (el not in list1)]
 
 
-def lists_equal(list1: list[Any], list2: list[Any]) -> bool:
+def lists_equal(list1: List[Any], list2: List[Any]) -> bool:
     """
     Tells whether two lists have the same elements.
 
diff --git a/src/pacti/utils/multiple_composition.py b/src/pacti/utils/multiple_composition.py
deleted file mode 100644
index d516ed58..00000000
--- a/src/pacti/utils/multiple_composition.py
+++ /dev/null
@@ -1,94 +0,0 @@
-"""Support for multiple composition."""
-from __future__ import annotations
-
-from typing import Any, Dict
-
-from pacti.iocontract import IoContract
-
-
-class _Tree:
-    def __init__(self, data: Any = None):
-        self.data = data
-        self.children: set[Any] = set()
-
-    def add_child(self, child: _Tree) -> None:
-        self.children.add(child)
-
-    def get_leafs(self) -> set[_Tree]:
-        leafs = set()
-        if self.children:
-            for child in self.children:
-                leafs.update(child.get_leafs())
-        else:
-            leafs.add(self)
-        return leafs
-
-    def remove_node(self, leaf: Any) -> None:
-        if not self.children:
-            return
-        if leaf in self.children:
-            self.children.remove(leaf)
-            return
-        for child in self.children:
-            child.remove_node(leaf)
-
-    def print_tree(self, level: int = 0, is_last_sibling: bool = True) -> None:
-        prefix = "    " * level
-        if is_last_sibling:
-            prefix += "`-- "
-        else:
-            prefix += "|-- "
-        print(prefix + str(self.data))
-        for i, child in enumerate(self.children):
-            is_last_child = i == len(self.children) - 1
-            child.print_tree(level + 1, is_last_child)
-
-
-def _build_dependency_tree(symbol_dict: Dict) -> _Tree:  # noqa: WPS231 too much cognitive complexity
-    root = _Tree()
-    symbol_nodes = {}
-    for symbol, value in symbol_dict.items():
-        inputs, outputs = value
-        if symbol not in symbol_nodes:
-            symbol_nodes[symbol] = _Tree(symbol)
-            root.add_child(symbol_nodes[symbol])
-        for output in outputs:
-            for dependency, dep_values in symbol_dict.items():
-                if output in dep_values[0]:
-                    if dependency not in symbol_nodes:
-                        symbol_nodes[dependency] = _Tree(dependency)
-                        # root.add_child(symbol_nodes[dependency])
-                    symbol_nodes[symbol].add_child(symbol_nodes[dependency])
-    return root
-
-
-def compose_multiple_contracts(contracts: list[IoContract]) -> IoContract:
-    """
-    Compose several contracts, finding the right order to compose them.
-
-    Args:
-        contracts: list of contracts to be composed.
-
-    Returns:
-        A contract corresponding to the ordered composition of the given contracts.
-    """
-    symbol_dict: dict[str, tuple[list[str], list[str]]] = {}  # noqa: WPS234 complex annotation
-    contracts_dict = {}
-    for i, contract in enumerate(contracts):
-        input_symbols = [v.name for v in contract.inputvars]
-        output_symbols = [v.name for v in contract.outputvars]
-        symbol_dict[f"c{i}"] = (input_symbols, output_symbols)
-        contracts_dict[f"c{i}"] = contract
-
-    dependency_tree: _Tree = _build_dependency_tree(symbol_dict)
-    leaf = dependency_tree.get_leafs().pop()
-    main_contract = contracts_dict[leaf.data]
-    dependency_tree.remove_node(leaf)
-    while dependency_tree is not None:
-        leaf = dependency_tree.get_leafs().pop()
-        if leaf.data is None:
-            break
-        main_contract.compose(contracts_dict[leaf.data])
-        dependency_tree.remove_node(leaf)
-
-    return main_contract


Test patch:
diff --git a/tests/case_studies/space_mission/space_mission_power.py b/tests/case_studies/space_mission/space_mission_power.py
index 4c33b1ad..f67483da 100644
--- a/tests/case_studies/space_mission/space_mission_power.py
+++ b/tests/case_studies/space_mission/space_mission_power.py
@@ -16,21 +16,16 @@
 # %%
 # %matplotlib widget
 
-#from IPython import display
-from base64 import b64decode
+from typing import Tuple
+
+from contract_utils import *
+
+# from IPython import display
 from pacti import write_contracts_to_file
+from pacti.iocontract import Var
 from pacti.terms.polyhedra import *
-from pacti.iocontract import IoContract, Var
-from PIL import Image
-import matplotlib.pyplot as plt
-import os
-import numpy as np
-from matplotlib import patches
-import pdb
-from matplotlib.collections import PatchCollection
-from contract_utils import *
 
-varPrefixes=["t", "soc", "d", "c", "u", "r", "temp"]
+varPrefixes = ["t", "soc", "d", "c", "u", "r", "temp"]
 epsilon = 1e-3
 
 
@@ -44,88 +39,89 @@
 # As summarized in [the qualitative impacts table](#qualitative-impacts), this function affects this viewpoint with impacts that are linear with the duration of the task:
 # - the battery charges proportionally to a generation rate.
 
+
 # %%
 # Parameters:
 # - s: start index of the timeline variables
 # - generation: (min, max) rate of battery charge during the task instance
 # - epsilon: approximately zero
-def CHARGING_power(s: int, generation: tuple[float, float], epsilon: float) -> PolyhedralContract:
-  spec = PolyhedralContract.from_string(
-    input_vars = [
-      f"soc{s}_entry",          # initial battery SOC
-      f"duration_charging{s}",  # variable task duration
-    ],
-    output_vars = [
-      f"soc{s}_exit",           # final battery SOC
-    ],
-    assumptions = [
-      # Task has a positive scheduled duration
-      f"-duration_charging{s} <= 0",
-
-      # Battery SOC must be positive
-      f"-soc{s}_entry <= 0",
-    ],
-    guarantees = [
-      # duration*generation(min) <= soc{exit} - soc{entry} <= duration*generation(max)
-      f" soc{s}_exit - soc{s}_entry - {generation[1]}*duration_charging{s} <= 0",
-      f"-soc{s}_exit + soc{s}_entry + {generation[0]}*duration_charging{s} <= 0",
-
-      # Battery cannot exceed maximum SOC
-      f"soc{s}_exit <= 100.0",
-      
-      # Battery should not completely discharge
-      f"-soc{s}_exit <= 0",
-    ])
-  return spec
+def CHARGING_power(s: int, generation: Tuple[float, float], epsilon: float) -> PolyhedralContract:
+    spec = PolyhedralContract.from_string(
+        input_vars=[
+            f"soc{s}_entry",  # initial battery SOC
+            f"duration_charging{s}",  # variable task duration
+        ],
+        output_vars=[
+            f"soc{s}_exit",  # final battery SOC
+        ],
+        assumptions=[
+            # Task has a positive scheduled duration
+            f"-duration_charging{s} <= 0",
+            # Battery SOC must be positive
+            f"-soc{s}_entry <= 0",
+        ],
+        guarantees=[
+            # duration*generation(min) <= soc{exit} - soc{entry} <= duration*generation(max)
+            f" soc{s}_exit - soc{s}_entry - {generation[1]}*duration_charging{s} <= 0",
+            f"-soc{s}_exit + soc{s}_entry + {generation[0]}*duration_charging{s} <= 0",
+            # Battery cannot exceed maximum SOC
+            f"soc{s}_exit <= 100.0",
+            # Battery should not completely discharge
+            f"-soc{s}_exit <= 0",
+        ],
+    )
+    return spec
+
 
 charging1_power = CHARGING_power(s=2, generation=(3.0, 4.0), epsilon=epsilon)
 print(f"Contract charging1_power:\n\n{charging1_power}")
 
-_ = plot_guarantees(contract=charging1_power,
-                x_var=Var("duration_charging2"),
-                y_var=Var("soc2_exit"),
-                var_values={
-                  Var("soc2_entry"):42,
-                },
-                x_lims=(0,100),
-                y_lims=(0,100))
+_ = plot_guarantees(
+    contract=charging1_power,
+    x_var=Var("duration_charging2"),
+    y_var=Var("soc2_exit"),
+    var_values={
+        Var("soc2_entry"): 42,
+    },
+    x_lims=(0, 100),
+    y_lims=(0, 100),
+)
 
 
 # %% [markdown]
 # ### Power-consuming Tasks (DSN, SBO, TCM)
 
+
 # %%
 # Parameters:
 # - s: start index of the timeline variables
 # - consumption: (min, max) rate of battery discharge during the task instance
-def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> PolyhedralContract:
-  spec = PolyhedralContract.from_string(
-    input_vars = [
-      f"soc{s}_entry",          # initial battery SOC
-      f"duration_{task}{s}",    # variable task duration
-    ],
-    output_vars = [
-      f"soc{s}_exit",           # final battery SOC
-    ],
-    assumptions = [
-      # Task has a positive scheduled duration
-      f"-duration_{task}{s} <= 0",
-
-      # Battery has enough energy for worst-case consumption throughout the task instance
-      f"-soc{s}_entry + {consumption[1]}*duration_{task}{s} <= 0",
-    ],
-    guarantees = [
-      # duration*consumption(min) <= soc{entry} - soc{exit} <= duration*consumption(max)
-      f" soc{s}_entry - soc{s}_exit - {consumption[1]}*duration_{task}{s} <= 0",
-      f"-soc{s}_entry + soc{s}_exit + {consumption[0]}*duration_{task}{s} <= 0",
-
-      # Battery cannot exceed maximum SOC
-      f"soc{s}_exit <= 100.0",
-      
-      # Battery should not completely discharge
-      f"-soc{s}_exit <= 0",
-    ])
-  return spec
+def power_consumer(s: int, task: str, consumption: Tuple[float, float]) -> PolyhedralContract:
+    spec = PolyhedralContract.from_string(
+        input_vars=[
+            f"soc{s}_entry",  # initial battery SOC
+            f"duration_{task}{s}",  # variable task duration
+        ],
+        output_vars=[
+            f"soc{s}_exit",  # final battery SOC
+        ],
+        assumptions=[
+            # Task has a positive scheduled duration
+            f"-duration_{task}{s} <= 0",
+            # Battery has enough energy for worst-case consumption throughout the task instance
+            f"-soc{s}_entry + {consumption[1]}*duration_{task}{s} <= 0",
+        ],
+        guarantees=[
+            # duration*consumption(min) <= soc{entry} - soc{exit} <= duration*consumption(max)
+            f" soc{s}_entry - soc{s}_exit - {consumption[1]}*duration_{task}{s} <= 0",
+            f"-soc{s}_entry + soc{s}_exit + {consumption[0]}*duration_{task}{s} <= 0",
+            # Battery cannot exceed maximum SOC
+            f"soc{s}_exit <= 100.0",
+            # Battery should not completely discharge
+            f"-soc{s}_exit <= 0",
+        ],
+    )
+    return spec
 
 
 # %% [markdown]
@@ -141,14 +137,16 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 dsn1_power = power_consumer(s=1, task="dsn", consumption=(3.8, 4.2))
 print(f"Contract dsn1_power:\n\n{dsn1_power}")
 
-_ = plot_guarantees(contract=dsn1_power,
-                x_var=Var("duration_dsn1"),
-                y_var=Var("soc1_exit"),
-                var_values={
-                  Var("soc1_entry"):80,
-                },
-                x_lims=(0,20),
-                y_lims=(0,80))
+_ = plot_guarantees(
+    contract=dsn1_power,
+    x_var=Var("duration_dsn1"),
+    y_var=Var("soc1_exit"),
+    var_values={
+        Var("soc1_entry"): 80,
+    },
+    x_lims=(0, 20),
+    y_lims=(0, 80),
+)
 
 # %% [markdown]
 # ### SBO Task (Small body observations)
@@ -162,14 +160,16 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 sbo1_power = power_consumer(s=3, task="sbo", consumption=(1.0, 1.4))
 print(f"Contract sbo1_power:\n\n{sbo1_power}")
 
-_ = plot_guarantees(contract=sbo1_power,
-                x_var=Var("duration_sbo3"),
-                y_var=Var("soc3_exit"),
-                var_values={
-                  Var("soc3_entry"):80,
-                },
-                x_lims=(0,100),
-                y_lims=(0,100))
+_ = plot_guarantees(
+    contract=sbo1_power,
+    x_var=Var("duration_sbo3"),
+    y_var=Var("soc3_exit"),
+    var_values={
+        Var("soc3_entry"): 80,
+    },
+    x_lims=(0, 100),
+    y_lims=(0, 100),
+)
 
 # %% [markdown]
 # ### TCM Task (Perform a Trajectory Correction Maneuver)
@@ -188,14 +188,16 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 tcm1_heating_power = power_consumer(s=4, task="tcm_heating", consumption=(0.7, 0.8))
 print(f"Contract tcm1_heating_power:\n\n{tcm1_heating_power}")
 
-_ = plot_guarantees(contract=tcm1_heating_power,
-                x_var=Var("duration_tcm_heating4"),
-                y_var=Var("soc4_exit"),
-                var_values={
-                  Var("soc4_entry"):80,
-                },
-                x_lims=(0,100),
-                y_lims=(0,100))
+_ = plot_guarantees(
+    contract=tcm1_heating_power,
+    x_var=Var("duration_tcm_heating4"),
+    y_var=Var("soc4_exit"),
+    var_values={
+        Var("soc4_entry"): 80,
+    },
+    x_lims=(0, 100),
+    y_lims=(0, 100),
+)
 
 # %% [markdown]
 # #### TCM DeltaV SubTask
@@ -205,14 +207,16 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 tcm1_deltav_power = power_consumer(s=5, task="tcm_deltav", consumption=(0.5, 0.6))
 print(f"Contract tcm1_deltav_power:\n\n{tcm1_deltav_power}")
 
-_ = plot_guarantees(contract=tcm1_deltav_power,
-                x_var=Var("duration_tcm_deltav5"),
-                y_var=Var("soc5_exit"),
-                var_values={
-                  Var("soc5_entry"):80,
-                },
-                x_lims=(0,100),
-                y_lims=(0,100))
+_ = plot_guarantees(
+    contract=tcm1_deltav_power,
+    x_var=Var("duration_tcm_deltav5"),
+    y_var=Var("soc5_exit"),
+    var_values={
+        Var("soc5_entry"): 80,
+    },
+    x_lims=(0, 100),
+    y_lims=(0, 100),
+)
 
 # %% [markdown]
 # #### Composing TCM SubTasks
@@ -220,7 +224,7 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 # Algebraic composition allows us to capture the requirement that a TCM Heating subtask must always precede a TCM DeltaV subtask by composing them.
 
 # %%
-tcm1_power=scenario_sequence(c1=tcm1_heating_power, c2=tcm1_deltav_power, variables=["soc"], c1index=4)
+tcm1_power = scenario_sequence(c1=tcm1_heating_power, c2=tcm1_deltav_power, variables=["soc"], c1index=4)
 print(f"========= tcm1_power\n{tcm1_power}")
 tcm1_power.get_variable_bounds("soc5_exit")
 
@@ -234,12 +238,12 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 # - TCM
 
 # %%
-steps12=scenario_sequence(c1=dsn1_power, c2=charging1_power, variables=["soc"], c1index=1)
+steps12 = scenario_sequence(c1=dsn1_power, c2=charging1_power, variables=["soc"], c1index=1)
 print(f"---- Steps 1,2\n{steps12}")
 steps12.get_variable_bounds("output_soc1")
 
 # %%
-steps123=scenario_sequence(c1=steps12, c2=sbo1_power, variables=["soc"], c1index=2)
+steps123 = scenario_sequence(c1=steps12, c2=sbo1_power, variables=["soc"], c1index=2)
 print(f"---- Steps 1,2,3\n{steps123}")
 print(steps123.get_variable_bounds("soc3_exit"))
 print(steps123.get_variable_bounds("duration_dsn1"))
@@ -247,7 +251,7 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 print(steps123.get_variable_bounds("duration_sbo3"))
 
 # %%
-steps1234=scenario_sequence(c1=steps123, c2=tcm1_power, variables=["soc"], c1index=3)
+steps1234 = scenario_sequence(c1=steps123, c2=tcm1_power, variables=["soc"], c1index=3)
 print(f"---- Steps 1,2,3,4\n{steps1234}")
 print(steps1234.get_variable_bounds("duration_dsn1"))
 print(steps1234.get_variable_bounds("duration_charging2"))
@@ -259,7 +263,7 @@ def power_consumer(s: int, task: str, consumption: tuple[float, float]) -> Polyh
 # #### Power Schedule constraints
 
 # %%
-scenario_power=steps1234.rename_variables([("soc5_exit", "output_soc5")])
+scenario_power = steps1234.rename_variables([("soc5_exit", "output_soc5")])
 print(f"scenario_power={scenario_power}")
 
 # %% tags=["remove_cell"]
diff --git a/tests/test_contains_behavior.py b/tests/test_contains_behavior.py
new file mode 100644
index 00000000..d884f81a
--- /dev/null
+++ b/tests/test_contains_behavior.py
@@ -0,0 +1,62 @@
+import glob
+
+import pytest
+
+from pacti.iocontract import Var
+from pacti.utils import read_contracts_from_file
+
+TEST_DATA_DIR = "tests/test_data/behavior_contracts"
+
+import logging
+
+FORMAT = "%(asctime)s:%(levelname)s:%(name)s:%(message)s"
+logging.basicConfig(filename="../pacti.log", filemode="w", level=logging.DEBUG, format=FORMAT)
+
+behavior_test_instances = glob.glob(TEST_DATA_DIR + "**/*behavior*.json", recursive=True)
+
+x = Var("x")
+y = Var("y")
+for instance in behavior_test_instances:
+    if "test_behavior_1" in instance:
+        contract = instance
+test_success_combinations = {contract: {x: 0, y: 2}}
+test_failure_combinations = {contract: {x: 3, y: 5}}
+
+
+@pytest.mark.parametrize("test_instance", behavior_test_instances)
+def test_contains_behavior_success(test_instance: str) -> None:
+    try:
+        c, _ = read_contracts_from_file(test_instance)
+    except:
+        assert False
+    assert len(c) == 1
+    contract = c[0]
+    try:
+        a_contains = contract.a.contains_behavior(test_success_combinations[test_instance])
+        g_contains = contract.g.contains_behavior(test_success_combinations[test_instance])
+    except:
+        assert False
+    assert a_contains == True
+    assert g_contains == True
+
+
+@pytest.mark.parametrize("test_instance", behavior_test_instances)
+def test_contains_behavior_failure(test_instance: str) -> None:
+    try:
+        c, _ = read_contracts_from_file(test_instance)
+    except:
+        assert False
+    assert len(c) == 1
+    contract = c[0]
+    try:
+        a_contains = contract.a.contains_behavior(test_failure_combinations[test_instance])
+        g_contains = contract.g.contains_behavior(test_failure_combinations[test_instance])
+    except:
+        assert False
+    assert a_contains == False
+    assert g_contains == False
+
+
+if __name__ == "__main__":
+    file = "test_data/behavior_contracts/test_behavior_1.json"
+    test_contains_behavior_success(file)
diff --git a/tests/test_data/behavior_contracts/test_behavior_1.json b/tests/test_data/behavior_contracts/test_behavior_1.json
new file mode 100644
index 00000000..7624490e
--- /dev/null
+++ b/tests/test_data/behavior_contracts/test_behavior_1.json
@@ -0,0 +1,21 @@
+[
+  {
+    "name": "contract",
+    "type": "PolyhedralContract",
+    "data": {
+      "input_vars": [
+        "x"
+      ],
+      "output_vars": [
+        "y"
+      ],
+      "assumptions": [
+        "x <= 2"
+      ],
+      "guarantees": [
+        "2 x + 3 y <= 7",
+        "-3 x + 2 y <= 8"
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/compound_contracts/test_merging_failure_1.json b/tests/test_data/compound_contracts/test_merging_failure_1.json
new file mode 100644
index 00000000..c4027775
--- /dev/null
+++ b/tests/test_data/compound_contracts/test_merging_failure_1.json
@@ -0,0 +1,60 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_0",
+        "y_0"
+      ],
+      "output_vars": [
+        "x_1",
+        "y_1"
+      ],
+      "assumptions": [
+        [
+          "x_0 = 1",
+          "y_0 = 1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "|-x_0 - y_0| <= 1",
+          "x_0 <= 5",
+          "y_0 <= 2",
+          "-x_0 <= 0",
+          "-y_0 <= 0"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_1",
+        "y_1"
+      ],
+      "output_vars": [
+        "x_0",
+        "y_0"
+      ],
+      "assumptions": [
+        [
+          "x_1 = 1",
+          "y_1 = 1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "|-x_0 - y_0| <= 1",
+          "x_0 <= 5",
+          "y_0 <= 2",
+          "-x_0 <= 0",
+          "-y_0 <= 0"
+        ]
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/compound_contracts/test_merging_success_multiagent_1.json b/tests/test_data/compound_contracts/test_merging_success_multiagent_1.json
new file mode 100644
index 00000000..007f6f72
--- /dev/null
+++ b/tests/test_data/compound_contracts/test_merging_success_multiagent_1.json
@@ -0,0 +1,116 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_A_0",
+        "y_A_0",
+        "t_0"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "t_1"
+      ],
+      "assumptions": [
+        [
+          "x_A_0 = 0",
+          "y_A_0 = 0",
+          "t_0 = 0"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_B_0",
+        "y_B_0",
+        "t_0"
+      ],
+      "output_vars": [
+        "x_B_1",
+        "y_B_1",
+        "t_1"
+      ],
+      "assumptions": [
+        [
+          "x_B_0 = 0",
+          "y_B_0 = 2",
+          "t_0 = 0"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_A_0",
+        "y_A_0",
+        "t_0",
+        "x_B_0",
+        "y_B_0"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "t_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "x_A_0 = 0",
+          "y_A_0 = 0",
+          "t_0 = 0",
+          "x_B_0 = 0",
+          "y_B_0 = 2"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0"
+        ]
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/compound_contracts/test_merging_success_multiagent_2.json b/tests/test_data/compound_contracts/test_merging_success_multiagent_2.json
new file mode 100644
index 00000000..adfcb7b8
--- /dev/null
+++ b/tests/test_data/compound_contracts/test_merging_success_multiagent_2.json
@@ -0,0 +1,98 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "current_distance"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "-current_distance <= -1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "x_A_1 - x_B_1 + y_A_1 - y_B_1 <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 - y_A_1 + y_B_1 <= -1"
+        ],
+        [
+          "x_A_1 - x_B_1 - y_A_1 + y_B_1 <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 + y_A_1 - y_B_1 <= -1"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "delta_x",
+        "delta_y",
+        "current_distance"
+      ],
+      "output_vars": [],
+      "assumptions": [
+        [
+          "-current_distance <= -1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-delta_x - delta_y <= -1"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "current_distance",
+        "delta_x",
+        "delta_y"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "-current_distance <= -1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "x_A_1 - x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "x_A_1 - x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ]
+      ]
+    }
+  }
+]
\ No newline at end of file
diff --git a/tests/test_data/compound_contracts/test_merging_success_multiagent_3.json b/tests/test_data/compound_contracts/test_merging_success_multiagent_3.json
new file mode 100644
index 00000000..77c9360c
--- /dev/null
+++ b/tests/test_data/compound_contracts/test_merging_success_multiagent_3.json
@@ -0,0 +1,191 @@
+[
+  {
+    "name": "contract1",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_A_0",
+        "y_A_0",
+        "t_0",
+        "x_B_0",
+        "y_B_0"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "t_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "x_A_0 = 0",
+          "y_A_0 = 0",
+          "t_0 = 0",
+          "x_B_0 = 0",
+          "y_B_0 = 2"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract2",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "current_distance",
+        "delta_x",
+        "delta_y"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "-current_distance <= -1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "x_A_1 - x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "x_A_1 - x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-x_A_1 + x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ]
+      ]
+    }
+  },
+  {
+    "name": "contract3",
+    "type": "PolyhedralContractCompound",
+    "data": {
+      "input_vars": [
+        "x_A_0",
+        "y_A_0",
+        "t_0",
+        "x_B_0",
+        "y_B_0",
+        "current_distance",
+        "delta_x",
+        "delta_y"
+      ],
+      "output_vars": [
+        "x_A_1",
+        "y_A_1",
+        "t_1",
+        "x_B_1",
+        "y_B_1"
+      ],
+      "assumptions": [
+        [
+          "x_A_0 = 0",
+          "y_A_0 = 0",
+          "t_0 = 0",
+          "x_B_0 = 0",
+          "y_B_0 = 2",
+          "-current_distance <= -1"
+        ]
+      ],
+      "guarantees": [
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0",
+          "x_A_1 - x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0",
+          "-x_A_1 + x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0",
+          "x_A_1 - x_B_1 - y_A_1 + y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ],
+        [
+          "-t_0 + t_1 = 1",
+          "|-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1",
+          "|-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1",
+          "x_A_1 <= 5",
+          "y_A_1 <= 2",
+          "-x_A_1 <= 0",
+          "-y_A_1 <= 0",
+          "|-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1",
+          "|-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1",
+          "x_B_1 <= 5",
+          "y_B_1 <= 2",
+          "-x_B_1 <= 0",
+          "-y_B_1 <= 0",
+          "-x_A_1 + x_B_1 + y_A_1 - y_B_1 <= -1",
+          "-delta_x - delta_y <= -1"
+        ]
+      ]
+    }
+  }
+]
diff --git a/tests/test_iocontract.py b/tests/test_iocontract.py
index c97e470d..00a6e33d 100644
--- a/tests/test_iocontract.py
+++ b/tests/test_iocontract.py
@@ -1,3 +1,5 @@
+from typing import List
+
 import pacti.iocontract as iocontract
 from pacti.terms.polyhedra import *
 
@@ -6,7 +8,7 @@ def validate_iocontract(contract: object) -> bool:
     return isinstance(contract, iocontract.IoContract)
 
 
-def create_contracts(num: int = 1) -> list[dict]:
+def create_contracts(num: int = 1) -> List[dict]:
     """
     Creates `num` number of contracts and returns a list of dicts
     """
diff --git a/tests/test_multiple_composition.py b/tests/test_multiple_composition.py
deleted file mode 100644
index 23c57d36..00000000
--- a/tests/test_multiple_composition.py
+++ /dev/null
@@ -1,34 +0,0 @@
-from pacti.terms.polyhedra.polyhedral_contract import PolyhedralContract
-from pacti.utils.multiple_composition import compose_multiple_contracts
-
-
-def test_multiple_composition() -> None:
-    c1 = PolyhedralContract.from_string(
-        assumptions=["x <= 1"], guarantees=["y <= 0"], input_vars=["x"], output_vars=["y"]
-    )
-    c2 = PolyhedralContract.from_string(
-        assumptions=["y <= 0"], guarantees=["z <= 0"], input_vars=["y"], output_vars=["z"]
-    )
-    c3 = PolyhedralContract.from_string(
-        assumptions=["y <= 0"], guarantees=["q <= 0"], input_vars=["y"], output_vars=["q"]
-    )
-    c4 = PolyhedralContract.from_string(
-        assumptions=["q <= 0"], guarantees=["v <= 0"], input_vars=["q"], output_vars=["v"]
-    )
-
-    contract = compose_multiple_contracts([c1, c2, c3, c4])
-
-    if contract.inputvars[0].name == "y" and contract.outputvars[0].name == "z":
-        assert str(contract.a.to_str_list()[0]) == "y <= 0"
-        assert str(contract.g.to_str_list()[0]) == "z <= 0"
-    elif contract.inputvars[0].name == "q" and contract.outputvars[0].name == "z":
-        assert str(contract.a.to_str_list()[0]) == "q <= 0"
-        assert str(contract.g.to_str_list()[0]) == "z <= 0"
-    elif contract.inputvars[0].name == "q" and contract.outputvars[0].name == "y":
-        assert str(contract.a.to_str_list()[0]) == "q <= 0"
-        assert str(contract.g.to_str_list()[0]) == "z <= 0"
-    elif contract.inputvars[0].name == "q" and contract.outputvars[0].name == "v":
-        assert str(contract.a.to_str_list()[0]) == "q <= 0"
-        assert str(contract.g.to_str_list()[0]) == "v <= 0"
-    else:
-        raise ValueError(f"Don't know how to handle this case\n{contract}")
diff --git a/tests/test_polyhedral_compound_contract.py b/tests/test_polyhedral_compound_contract.py
new file mode 100644
index 00000000..f488df26
--- /dev/null
+++ b/tests/test_polyhedral_compound_contract.py
@@ -0,0 +1,51 @@
+import glob
+
+import pytest
+
+from pacti.utils import read_contracts_from_file
+
+TEST_DATA_DIR = "tests/test_data/compound_contracts"
+
+import logging
+
+# from ipdb import set_trace as st
+
+FORMAT = "%(asctime)s:%(levelname)s:%(name)s:%(message)s"
+logging.basicConfig(filename="../pacti.log", filemode="w", level=logging.DEBUG, format=FORMAT)
+
+merging_test_instances = glob.glob(TEST_DATA_DIR + "**/*merging_success*.json", recursive=True)
+
+
+@pytest.mark.parametrize("test_instance", merging_test_instances)
+def test_merging_success(test_instance: str) -> None:
+    try:
+        c, _ = read_contracts_from_file(test_instance)
+    except:
+        assert False
+    assert len(c) == 3
+    expected = c[2]
+    try:
+        obtained = c[0].merge(c[1])
+    except:
+        assert False
+    # st()
+    assert expected == obtained
+
+
+merging_failure_test_instances = glob.glob(TEST_DATA_DIR + "**/*merging_failure*.json", recursive=True)
+
+
+@pytest.mark.parametrize("test_instance", merging_failure_test_instances)
+def test_merging_failure(test_instance: str) -> None:
+    try:
+        c, _ = read_contracts_from_file(test_instance)
+    except:
+        assert False
+    assert len(c) == 2
+    with pytest.raises(ValueError):
+        _ = c[0].merge(c[1])
+
+
+if __name__ == "__main__":
+    file = "test_merging_success_multiagent_3.json"
+    test_merging_success(file)
diff --git a/tests/test_polyhedral_contract.py b/tests/test_polyhedral_contract.py
index 1bd75e2c..afc0779d 100644
--- a/tests/test_polyhedral_contract.py
+++ b/tests/test_polyhedral_contract.py
@@ -52,11 +52,12 @@ def test_composition_failure(test_instance: str) -> None:
         _ = c[0].compose(c[1])
 
 
-composition_unsatisfiable_context_instances = glob.glob(TEST_DATA_DIR + "**/*composition_unsatisfiable_context*.json", recursive=True)
+composition_unsatisfiable_context_instances = glob.glob(
+    TEST_DATA_DIR + "**/*composition_unsatisfiable_context*.json", recursive=True
+)
 
 
-@pytest.mark.parametrize("test_instance",
-                         composition_unsatisfiable_context_instances)
+@pytest.mark.parametrize("test_instance", composition_unsatisfiable_context_instances)
 def test_composition_context(test_instance: str) -> None:
     try:
         c, _ = read_contracts_from_file(test_instance)
diff --git a/tests/test_polyhedral_contract_syntax.py b/tests/test_polyhedral_contract_syntax.py
index d22f7071..1b145083 100644
--- a/tests/test_polyhedral_contract_syntax.py
+++ b/tests/test_polyhedral_contract_syntax.py
@@ -97,8 +97,11 @@ def test_pattern4_contract() -> None:
 
     assert 0 == len(c.g.terms)
 
+
 def test_epsilon_contract() -> None:
-    c = PolyhedralContract.from_string(input_vars=["i"], output_vars=[], assumptions=["|i| <= 1.23456789e-5"], guarantees=[])
+    c = PolyhedralContract.from_string(
+        input_vars=["i"], output_vars=[], assumptions=["|i| <= 1.23456789e-5"], guarantees=[]
+    )
 
     assert 1 == len(c.inputvars)
     assert "i" == c.inputvars[0].name
@@ -121,4 +124,4 @@ def test_epsilon_contract() -> None:
     assert 1.22e-5 < p0.constant
     assert p0.constant < 1.24e-5
 
-    assert 0 == len(c.g.terms)
\ No newline at end of file
+    assert 0 == len(c.g.terms)
diff --git a/tests/test_polyhedral_terms.py b/tests/test_polyhedral_terms.py
index 4d15ae7c..c64a9bc2 100644
--- a/tests/test_polyhedral_terms.py
+++ b/tests/test_polyhedral_terms.py
@@ -1,4 +1,5 @@
 import logging
+from typing import List
 
 import pytest
 
@@ -10,7 +11,7 @@
 logging.basicConfig(filename="../pacti.log", filemode="w", level=logging.DEBUG, format=FORMAT)
 
 
-def to_pts(str_rep_list: list[str]) -> PolyhedralTermList:
+def to_pts(str_rep_list: List[str]) -> PolyhedralTermList:
     return PolyhedralTermList([item for el in str_rep_list for item in polyhedral_termlist_from_string(el)])
 
 
diff --git a/tests/test_py_loaders.py b/tests/test_py_loaders.py
index 40c60347..59adfbf6 100644
--- a/tests/test_py_loaders.py
+++ b/tests/test_py_loaders.py
@@ -1,3 +1,5 @@
+from typing import List
+
 import pytest
 from test_iocontract import validate_iocontract
 
@@ -5,7 +7,7 @@
 from pacti.terms.polyhedra import *
 
 
-def create_contracts(num: int = 1) -> list[dict]:
+def create_contracts(num: int = 1) -> List[dict]:
     """
     Creates `num` number of contracts and returns a list of dicts
     """