Generate tests & improve code quality of multiagent case study

Tests

Please extract tests for Pacti from your case study. To do this, use the following statement:

from pacti import write_contracts_to_file

Then, supposing that contracts c1 and c2 are two contracts, and c3 is the result of composition (or other operation), say

write_contracts_to_file([c1, c2, c3], ["contract1", "contract2", "contract3"], "file_name.json")

This will place the three contracts in the file file_name.json. Afterwards, move this file to

tests/test_data/polyhedral_contracts/test_composition_success_<description_or_number>.json

In this file name, you can replace "composition" with "merging" or "quotient." The word "success" means that the test framework will expect three contracts in the file. The first two are arguments of the operation and the third is the result. The word "success" can be replaced by "failure." In this case, the framework will expect two contracts in the file. The framework will expect Pacti to say that there was a problem computing this operation.

If you place two contracts in a test file, and you name the file

test_refinement_<description_or_number>.json

the test framework will test that the first argument is a refinement of the second.

After you add your test to the folder tests/test_data/polyhedral_contracts/, it will be executed when you run make test.

Code quality

In the file duties.py, replace the line

PY_SRC_PATHS = (Path(_) for _ in ("src", "tests", "case_studies"))

with

PY_SRC_PATHS = (Path(_) for _ in ("case_studies/<your case_study>"))

Make sure the following commands give zero errors:

make check-jn-quality
check-jn-types
check-quality
check-types

The first two address jupyter notebooks. The other two analyze your python code.

When analyzing code quality, the linter will sometime say that a linter will make changes. Running the command

make format

may lower the number of violations.

@iincer I am trying to create the tests for the PolyhedralContractCompounds and I am getting the following error message:

from pacti import write_contracts_to_file

write_contracts_to_file([c_dynA, c_dynB, c_combined_dynamics], ["contract1", "contract2", "contract3"], "test_merging_success_multiagent_1.json")

Trace:

---------------------------------------------------------------------------
ValueError                                Traceback (most recent call last)
/var/folders/mg/93xdfdss4rl7sxk1y7hmwrhr0000gn/T/ipykernel_25215/792808115.py in <module>
      1 from pacti import write_contracts_to_file
      2 
----> 3 write_contracts_to_file([c_dynA, c_dynB, c_combined_dynamics], ["contract1", "contract2", "contract3"], "test_merging_success_multiagent_1.json")

~/Documents/Research/pacti/src/pacti/utils/fileio.py in write_contracts_to_file(contracts, names, file_name, machine_representation)
     90 
     91         else:
---> 92             raise ValueError("Unsupported argument type")
     93         data.append(entry)
     94 

ValueError: Unsupported argument type

The three contracts are PolyhedralContractCompounds of the following form (Note that they are just compounds because they will be merged with a compound in the next step).

Dynamics Contract Robot A:
InVars: [x_A_0, y_A_0, t_0]
OutVars:[x_A_1, y_A_1, t_1]
A: [
  x_A_0 = 0.0
  y_A_0 = 0.0
  t_0 = 0.0
]
G: [
  -t_0 + t_1 = 1.0
  |-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1.0
  |-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1.0
  x_A_1 <= 5.0
  y_A_1 <= 2.0
  -x_A_1 <= 0.0
  -y_A_1 <= 0.0
]

Dynamics Contract Robot B:
InVars: [x_B_0, y_B_0, t_0]
OutVars:[x_B_1, y_B_1, t_1]
A: [
  x_B_0 = 0.0
  y_B_0 = 2.0
  t_0 = 0.0
]
G: [
  -t_0 + t_1 = 1.0
  |-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1.0
  |-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1.0
  x_B_1 <= 5.0
  y_B_1 <= 2.0
  -x_B_1 <= 0.0
  -y_B_1 <= 0.0
]

Combined Dynamics:
InVars: [x_A_0, y_A_0, t_0, x_B_0, y_B_0]
OutVars:[x_A_1, y_A_1, t_1, x_B_1, y_B_1]
A: [
  x_A_0 = 0.0
  y_A_0 = 0.0
  t_0 = 0.0
  x_B_0 = 0.0
  y_B_0 = 2.0
]
G: [
  -t_0 + t_1 = 1.0
  |-x_A_0 + x_A_1 - y_A_0 + y_A_1| <= 1.0
  |-x_A_0 + x_A_1 + y_A_0 - y_A_1| <= 1.0
  x_A_1 <= 5.0
  y_A_1 <= 2.0
  -x_A_1 <= 0.0
  -y_A_1 <= 0.0
  |-x_B_0 + x_B_1 - y_B_0 + y_B_1| <= 1.0
  |-x_B_0 + x_B_1 + y_B_0 - y_B_1| <= 1.0
  x_B_1 <= 5.0
  y_B_1 <= 2.0
  -x_B_1 <= 0.0
  -y_B_1 <= 0.0
]

It seems like the issue is somewhere here with the type of the merged contract. I create the two original contracts using PolyhedralContractCompound.from_string and they pass the type check but then for the merged contract c_combined_dynamics I get the following:

type(c_combined_dynamics)
Out[9]:
pacti.iocontract.compundiocontract.IoContractCompound

What the write_contracts_to_file code is checking for:

isinstance(c_combined_dynamics, PolyhedralContractCompound)
Out[11]:
False

By the way, should compundiocontract be compoundiocontract?

I am also having issues with running the code quality checks.

I replaced

PY_SRC_PATHS = (Path(_) for _ in DIR_SEARCH)

with

PY_SRC_PATHS = (Path(_) for _ in ("case_studies/multiagent_coordination"))

and then running make check-jn-quality gives this trace:

(base) ➜  pacti git:(update_multiagent) ✗ make check-jn-quality
pdm run duty check-jn-quality 
Inside an active virtualenv /Users/josefinegraebener/opt/anaconda3, reusing it.
✗ Checking notebook quality (1)
  > nbqa flake8 --ignore=D100,WPS226,WPS421,WPS111,BLK100  --config=config/flake8.ini case_studies/evaluating_perception/simple_script.ipynb case_studies/evaluating_perception/evaluating_classification_algorithms 2.ipynb case_studies/evaluating_perception/case_study_new.ipynb case_studies/evaluating_perception/simple_evaluating_perception.ipynb case_studies/evaluating_perception/case_study.ipynb case_studies/evaluating_perception/simple_script 2.ipynb case_studies/evaluating_perception/lower_bounds.ipynb case_studies/evaluating_perception/saved_results.ipynb case_studies/evaluating_perception/recompute.ipynb case_studies/digital_signal_processing/dsp_wl.ipynb case_studies/multiagent_coordination/multiagent_for_tests.ipynb case_studies/multiagent_coordination/multiagent.ipynb case_studies/biocircuit_specifications/specification_based_synthetic_biology.ipynb case_studies/space_mission/tests.ipynb case_studies/space_mission/space_mission_3viewpoints.ipynb case_studies/space_mission/analysis_results2.ipynb case_studies/space_mission/space_mission.ipynb case_studies/space_mission/3dploy.ipynb case_studies/space_mission/space_mission_navigation.ipynb case_studies/space_mission/analysis_results1.ipynb case_studies/space_mission/space_mission_power.ipynb case_studies/space_mission/analysis_results.ipynb case_studies/space_mission/power-range.ipynb case_studies/space_mission/space_mission_science.ipynb case_studies/space_mission/space_mission_thermal.ipynb case_studies/space_mission/power.ipynb case_studies/mars_entry_descent_landing/mars_edl_3rd_encoding.ipynb case_studies/mars_entry_descent_landing/mars_edl_2nd_encoding.ipynb case_studies/mars_entry_descent_landing/mars-edl-ranges.ipynb case_studies/mars_entry_descent_landing/mars_edl_2nd_encoding-with-gap.ipynb case_studies/mars_entry_descent_landing/mars_edl-1st-encoding.ipynb case_studies/uav_topologies_generation/topologies.ipynb docs/getting_started.ipynb docs/_case_studies/evaluating_perception/simple_script.ipynb docs/_case_studies/evaluating_perception/evaluating_classification_algorithms 2.ipynb docs/_case_studies/evaluating_perception/case_study_new.ipynb docs/_case_studies/evaluating_perception/simple_evaluating_perception.ipynb docs/_case_studies/evaluating_perception/case_study.ipynb docs/_case_studies/evaluating_perception/simple_script 2.ipynb docs/_case_studies/evaluating_perception/lower_bounds.ipynb docs/_case_studies/evaluating_perception/saved_results.ipynb docs/_case_studies/evaluating_perception/recompute.ipynb docs/_case_studies/digital_signal_processing/dsp_wl.ipynb docs/_case_studies/digital_signal_processing/dsp_wl_backup.ipynb docs/_case_studies/multiagent_coordination/multiagent.ipynb docs/_case_studies/biocircuit_specifications/specification_based_synthetic_biology.ipynb docs/_case_studies/uav_topologies_generation/topologies.ipynb
  No such file or directory: case_studies/evaluating_perception/evaluating_classification_algorithms

make: *** [check-jn-quality] Error 1

Why is it still checking the other case studies?

Hi Josefine, the directory search is best controlled via the variable DIR_SEARCH There you can specify what sources should be used.

Sorry for the outdated description in the issue :-(

It seems like the issue is somewhere here with the type of the merged contract. I create the two original contracts using PolyhedralContractCompound.from_string and they pass the type check but then for the merged contract c_combined_dynamics I get the following:
type(c_combined_dynamics)
Out[9]:
pacti.iocontract.compundiocontract.IoContractCompound
What the write_contracts_to_file code is checking for:
isinstance(c_combined_dynamics, PolyhedralContractCompound)
Out[11]:
False
By the way, should compundiocontract be compoundiocontract?

Yes, thank you for debugging this! I made a change that should address the issue.

When creating the tests, two out of the three tests pass, but I am getting an error trace for my third test. I am not sure how to debug this. Do you have an idea what the issue might be? The json file:

[
  {
    "name": "contract1",
    "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": "contract2",
    "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": "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"
        ]
      ]
    }
  }
]

This is the trace.

(base) ➜  pacti git:(update_multiagent) ✗ make test coverage
pdm run duty test 
Inside an active virtualenv /Users/josefinegraebener/opt/anaconda3, reusing it.
✗ Running tests (1)
  > pytest -c config/pytest.ini -n auto -k "" tests
  ============================= test session starts ==============================
  platform darwin -- Python 3.9.13, pytest-7.2.0, pluggy-1.0.0
  Using --randomly-seed=2217590834
  rootdir: /Users/josefinegraebener/Documents/Research/pacti/config, configfile: pytest.ini
  plugins: anyio-3.5.0, xdist-3.0.2, randomly-3.12.0, cov-4.0.0
  gw0 [60] / gw1 [60] / gw2 [60] / gw3 [60]
  s...................F........s.s............................             [100%]
  =================================== FAILURES ===================================
  _ test_merging_success[tests/test_data/compound_contracts/test_merging_success_multiagent_3.json] _
  [gw0] darwin -- Python 3.9.13 /Users/josefinegraebener/opt/anaconda3/bin/python

  test_instance = 'tests/test_data/compound_contracts/test_merging_success_multiagent_3.json'

      @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
  >       assert expected == obtained
  E       assert <pacti.terms.polyhedra.polyhedral_contract.PolyhedralContractCompound object at 0x7faaa82b7e20> == <pacti.terms.polyhedra.polyhedral_contract.PolyhedralContractCompound object at 0x7faac88f8d00>

  tests/test_polyhedral_compound_contract.py:29: AssertionError
  =============================== warnings summary ===============================
  ../../../opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214
  ../../../opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214
  ../../../opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214
  ../../../opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214
  ../../../opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214
    /Users/josefinegraebener/opt/anaconda3/lib/python3.9/site-packages/xdist/plugin.py:214: DeprecationWarning: The --rsyncdir command line argument and rsyncdirs config variable are deprecated.
    The rsync feature will be removed in pytest-xdist 4.0.
      config.issue_config_time_warning(warning, 2)

  -- Docs: https://docs.pytest.org/en/stable/how-to/capture-warnings.html

  ---------- coverage: platform darwin, python 3.9.13-final-0 ----------
  Name                                               Stmts   Miss Branch BrPart     Cover
  ---------------------------------------------------------------------------------------
  src/pacti/iocontract/compundiocontract.py            108     34     60     12    63.10%
  src/pacti/iocontract/iocontract.py                   274     69     86     18    68.06%
  src/pacti/terms/polyhedra/plots.py                   132    111     42      1    12.64%
  src/pacti/terms/polyhedra/polyhedra.py               619    101    251     28    80.80%
  src/pacti/terms/polyhedra/polyhedral_contract.py      87     31     68      6    61.94%
  src/pacti/terms/polyhedra/serializer.py              203     31    116     19    80.56%
  src/pacti/utils/errors.py                              3      0      0      0   100.00%
  src/pacti/utils/fileio.py                             49     26     22      3    45.07%
  src/pacti/utils/lists.py                               9      1      6      0    93.33%
  src/pacti/utils/multiple_composition.py               67      9     36      3    84.47%
  tests/test_examples.py                                15      0      0      0   100.00%
  tests/test_iocontract.py                              17      0      4      0   100.00%
  tests/test_multiple_composition.py                    21     10      8      1    41.38%
  tests/test_polyhedral_compound_contract.py            32     11      0      0    65.62%
  tests/test_polyhedral_contract.py                    112     35      4      1    67.24%
  tests/test_polyhedral_contract_syntax.py              91      0      0      0   100.00%
  tests/test_polyhedral_terms.py                        82      1      4      1    97.67%
  tests/test_py_loaders.py                              24      0      8      0   100.00%
  ---------------------------------------------------------------------------------------
  TOTAL                                               1945    470    715     93    72.14%

  =========================== short test summary info ============================
  FAILED config/test_polyhedral_compound_contract.py::test_merging_success[tests/test_data/compound_contracts/test_merging_success_multiagent_3.json] - assert <pacti.terms.polyhedra.polyhedral_contract.PolyhedralContractCompoun...
  ============= 1 failed, 56 passed, 3 skipped, 5 warnings in 5.33s ==============

make: *** [test] Error 1

The error is saying that the merged contract is not equivalent to the stored value. To know more about why it considers them different, you could go to compoundiocontract.py. I'd suggest looking at the definition of __eq__ and perhaps modifying it so that it prints data related to this error...

 >       assert expected == obtained
  E       assert <pacti.terms.polyhedra.polyhedral_contract.PolyhedralContractCompound object at 0x7faaa82b7e20> == <pacti.terms.polyhedra.polyhedral_contract.PolyhedralContractCompound object at 0x7faac88f8d00>

I dug a little deeper in the __eq__ function for this test and the contracts look the same to me, I saw that it checks for equality using <=, but that doesn't seem to work. This is the output:

ipdb> expected.a == obtained.a
True
ipdb> expected.g == obtained.g
True
ipdb> expected == obtained
False
ipdb> expected <= obtained
*** TypeError: '<=' not supported between instances of 'PolyhedralContractCompound' and 'PolyhedralContractCompound'

If the assumptions and guarantees are the same, shouldn't the contracts be the same?

One possible difference is the input and output variables. Below is the equality check. Even the order matters because we are comparing lists.

    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
        )

Where do you get that code from? In compundiocontract.py I see the __eq__ function as:

    def __eq__(self, other: object) -> bool:
        if not isinstance(other, type(self)):
            raise ValueError()
        return self <= other <= self

But looking at your function makes sense as this is likely to be the issue:

ipdb> expected.inputvars == obtained.inputvars
False
ipdb> expected.outputvars == obtained.outputvars
False
ipdb> expected.inputvars
[<Var x_A_0>, <Var y_A_0>, <Var t_0>, <Var x_B_0>, <Var y_B_0>, <Var current_distance>, <Var delta_x>, <Var delta_y>]
ipdb> expected.outputvars
[<Var x_A_1>, <Var y_A_1>, <Var t_1>, <Var x_B_1>, <Var y_B_1>]
ipdb> obtained.inputvars
[<Var current_distance>, <Var delta_x>, <Var delta_y>, <Var x_A_0>, <Var y_A_0>, <Var t_0>, <Var x_B_0>, <Var y_B_0>]
ipdb> obtained.outputvars
[<Var x_A_1>, <Var y_A_1>, <Var x_B_1>, <Var y_B_1>, <Var t_1>]

Either the order should not matter - or the order needs to be deterministic.

Exactly, the code is here: https://github.com/FormalSystems/pacti/blob/471bc1ac92a997ce66f85f4159d7cbf24cb3edc8/src/pacti/iocontract/compundiocontract.py#L246-L253

Either the order should not matter - or the order needs to be deterministic.

I agree: the choice now was to make it deterministic. We don't want to generate different results with different runs of the same code (exception: I don't know if some LP algs we are using have randomness). It would be good to know why we are getting different variable order.

Ahh I was looking at the NestedTermList. I am confused that it isn't deterministic, I thought that had been fixed a while ago, but maybe that fix wasn't made for the compound contract? I don't know why the order is different.

I just looked at the merging code for IoContractCompound. The function is deterministic. However, it depends on the order in which operations are made. c1.merge(c2) may have a different input/output variable order than c2.merge(c1). Is it possible that this is the issue? I agree that this is a very strong notion of equality, but Pacti's results may depend on variable order; this is the reason it's implemented like that.

Yes that was it! Thanks.

pacti-org / pacti

Generate tests & improve code quality of multiagent case study #228

Tests

Code quality