Skip to content
A tool for obtaining LTL formulas from a sample of positive and negative words.
Python Shell
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


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


  • 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)


  • to test on a single example (set of positive and negative traces), runt python 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 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 --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.

You can’t perform that action at this time.