Prototype to compute distinguishing Hennessy-Milner formulas. Used for the evaluation of arXiv:2307.05265, to be presented at CONCUR 2023. For real-world applications one better uses the counter-examples of the mCRL2 tool ltscompare.
usage: python distinguish.py [-h] [-c] [-v] [-b] [-p] [--logfile LOGFILE] infile1 infile2
Compute a distinguishing HML formula
positional arguments:
infile1 Input LTS 1, input should be Aldebaran format (.aut)
infile2 Input LTS 2, input should be Aldebaran format (.aut)
options:
-h, --help show this help message and exit
-c, --cleaveland
-v, --verbose
-b, --benchmark only output the metrics of the distinguishing formula.
-p, --postprocess
--logfile LOGFILE logfile to write to