--------------------------------------------------------------------------------
Monitoring arithmetic properties (prototype for AAAI'23)
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
REQUIREMENTS
--------------------------------------------------------------------------------
The tool requires Python3 and the following libraries:
 - bindings to the Z3 SMT solver (package "z3")
 - bindings to the CVC5 SMT solver, see
   https://github.com/cvc5/cvc5
 - visualization library Matplotlib (package "matplotlib")
 - NetworkX for network visualization (package "networkx")
 - PyParsing module to process input (package "pyparsing")
 
On a Debian-like system all except for CVC5 can be installed by
 $ sudo apt-get install python3-z3
 $ sudo apt-get install python3-networkx
 $ sudo apt-get install python3-matplotlib
 $ sudo apt-get install python3-pyparsing

--------------------------------------------------------------------------------
USAGE
--------------------------------------------------------------------------------

Both the trace and the property can be supplied as command line arguments:

 $ python3 arithmonitor.py -t "[(x = 0, y = 0)(x = 1.5, y = 1)(x = 2, y = 2)(x = 9, y = 2)]" -p "(x' >= x) U (x == 3)"

Here the option -t specifies the trace as a sequence of variable-value pairs,
and -p the LTLf property to be checked.
Alternatively, the trace can be supplied in a json file, cf. the files in the 
examples/ directory. An example call is as follows, which asserts that whenever
the request variable "req" is set and the temperature "temp" has a value at most
30, then in the next step the control flag "control" is set. 

 $ python3 arithmonitor.py -t examples/temperature.json -p "G ( ((req != 1) || (temp <= 30)) || (control' == 1))"

Note that in the files also the type of each variable gets specified, while in
the command line call the type is assumed to be rational if values contain "."s
and integer otherwise.

The LTLf properties are to be specified as follows:
 - temporal operators are X, F, G, and U
 - boolean operators are && and ||
 - literals are comparisons of arithmetic expressions, using the comparison 
   operators ==, !=, <, <=, >, >=
 - arithmetic expressions may involve constants and trace variables, which can 
   possibly be followed by a ' character to indicate 1-step lookahead. Moreover,
   the arithmetic operators + and - can be used.

The example files also list some examples for properties that can be checked.