--------------------------------------------------------------------------------
LinDMT: LTLf Model Checking Modulo Theories
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
REQUIREMENTS
--------------------------------------------------------------------------------
LinDMT 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
--------------------------------------------------------------------------------
LinDMT performs LTLf model checking modulo theories.
As input, it requires a DMT specified in a json format, and an LTLf property. 
The precise format of both of these are described in the help page of the web
interface, see
  http://18.117.176.211/lindmt/?p=help

An example call for the running example of the paper is as follows:

 python3 src/lindmt.py -m benchmarks/paper_simple.json -p "(x >= 0) U ( o1 && (x == 4))"

Here the option -m specifies the DMT model, and -p the LTLf property.
This call will produce picture files in the directory out/ that visualize
the DMT, the NFA, and the product construction, respectively.
In addition, if the language of the product automaton is not empty, LinDMT will 
print a witness run to the standard output.


--- BENCHMARK SCRIPT -----------------------------------------------------------

The directory benchmarks contains the examples used in experiments in the paper.
A script to run LinDMT on all of them is provided as well, it can be executed as
follows:

 $ python3 src/run_benchmarks.py
