Skip to content

Latest commit

 

History

History
34 lines (25 loc) · 2.09 KB

README.md

File metadata and controls

34 lines (25 loc) · 2.09 KB
Raw

traces2LTL

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

  • setup a virtualenvironment for python 3.6 (link) and activate it (workon ...)
  • run pip install -r requirements.txt to qinstall all necessary python packages available from pip
  • install Z3 with python bindings (link)

Running

  • to test on a single example (set of positive and negative traces), runt python experiment.py with --test_dt_method or --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.py with --test_dt_method or --test_sat_method and 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_method with no additional parameters takes the traces from traces/generatedTest and produces results in experiments/test/
  • additionally, to make sure everything runs as it should one can run pytest

Experiment Trace File Format

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.