IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
I would like to discuss some possible improvements in the test script (tests/test.py):
I think the tests should be sandboxed (i.e. they should run in a specific folder that will be destroyed after the execution of the tests). It is a bit inconvenient that the script creates many files in the current directory every time it is executed. If I forget to enter a new temporary folder before running the tests then the folder I am in gets completely filled with .res files.
I think the script should build and install the project before running the tests. If you forget to build and install imitator before running the tests, then their result is meaningless. This would also be aligned with the semantics of dune runtest, which makes sure that the project is built before running the tests.
I would like to discuss some possible improvements in the test script (
tests/test.py):I think the tests should be sandboxed (i.e. they should run in a specific folder that will be destroyed after the execution of the tests). It is a bit inconvenient that the script creates many files in the current directory every time it is executed. If I forget to enter a new temporary folder before running the tests then the folder I am in gets completely filled with
.resfiles.I think the script should build and install the project before running the tests. If you forget to build and install
imitatorbefore running the tests, then their result is meaningless. This would also be aligned with the semantics ofdune runtest, which makes sure that the project is built before running the tests.