The goal is to learn an LTL formula that separates set of positive (P) and negative (N) traces. The resulting formula should be a model for every trace in P and should not be a model for any of the traces from N. There are two methods in this repository - one that encodes the problem as a satisfiability of Boolean formula and gives it to Z3 solver, and the other that is based on decision tree learning.
Webdemo is available at flie.mpi-sws.org
- setup a virtualenvironment for python 3.6 (link) and activate it (
workon ...) - run
pip install -r requirements.txtto qinstall all necessary python packages available from pip - install Z3 with python bindings (link)
- to test on a single example (set of positive and negative traces), runt
python experiment.pywith--test_dt_methodor--test_sat_method(or both) and with the path to the file with the example provided as an argument--traces - to test on set of examples, one can run
python measureSolvingTime.pywith--test_dt_methodor--test_sat_methodand with the path to the folder containing the examples provided as an argument--test_traces_folder - running
python measureSolvingTime.py --test_dt_method --test_sat_methodwith no additional parameters takes the traces fromtraces/generatedTestand produces results inexperiments/test/ - additionally, to make sure everything runs as it should one can run
pytest
Experiment traces file consists of:
- accepted traces
- rejected traces
- operators that a program can use
- max depth to explore
- the expected formula that describes this trace
An example trace looks like this
1,1;1,0;0,1::1 and means that there are two variables (x0 and x1) whose values in different timesteps are
- x0 : 1,(1,0)*
- x1: 1,(0,1)*
The value after separator :: denotes the start of lasso that is being repeated forever. If it is missing, it assumes that the whole sequence is repeated indefinitely.