Skip to main content

Python wrapper around tool ltlcross from Spot library

Project description

ltlcross wrapper

Python wrapper around the amazing tool ltlcross from Spot library. The tool compares LTL to automata translators.


  • Spot
  • Python >= 3.6

The following libraries are needed for bokeh scatter plots (can be used in Jupyter)

  • bokeh (installs automatically by pip)
  • colorcet (installs automatically by pip)
  • jupyter_bokeh for rendering the plots in JupyterLab


python3 -m pip install -U ltlcross_wrapper


ltlcross_wrapper offers 2 classes:

  • Modulizersplits a big ltlcross task into smaller ones, execute the small tasks in parallel, and merge the intermediate results into one final .csv, .log, and _bogus.ltl files.
  • ResAnalyzer parses the results of ltlcross, and implements several functions to analyze and visualize the results, mainly in Jupyter notebooks.


We need to specify the tools and file(s) with formulas which ltlcross should use. The tools are given as a dict whose items are pairs (name, ltlcross_cmd) where ltlcross_cmd is COMMANDFMT from man ltlcross.

tools = {"LTL3HOA"    : "ltl3hoa -d -x -i -p 2 -f %f > %O",
         "SPOT"       : "ltl2tgba"

Typical usage of Modulizer follows.

m = Modulizer(tools, formulas.ltl)

The above command splits the file formulas.ltl into several files with 2 formulas each, and uses 4 processes to run ltlcross on these small files in parallel. The number of processes can be controlled by setting processes in both the constructor and the function run(). The number of formulas in each small file can be changed by setting chunk_size in the constructor.

If a previous computation was interrupted for some reason, consider using


instead of The function m.resume() will skip computing the small tasks for which it already finds an .csv file with the result.

You can delete the final results and intermediate files, and rerun the computation by


By default, all intermediate files will be created in directory and the merged files modular.csv, modular.log, modular_bogus.ltl will be created in the current directory. The base modular can be changed to new_name simply by setting name=new_name. Otherwise, each filename/dirname can be changed by setting out_res_file, out_log_file, out_bogus_file, and tmp_dir.

TODO: Explain ltlcross options

Results' Analyzer

See the usage notebook. Currently, bokeh scatter plots do not render directly on github so you might consider to see the notebook on nbviewer

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for ltlcross-wrapper, version 0.6.1
Filename, size File type Python version Upload date Hashes
Filename, size ltlcross_wrapper-0.6.1-py3-none-any.whl (19.5 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size ltlcross_wrapper-0.6.1.tar.gz (18.1 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page