ltlcross-wrapper 0.6.1

Python wrapper around tool ltlcross from Spot library

ltlcross wrapper

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

Requires

• 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

Installation

python3 -m pip install -U ltlcross_wrapper

Usage

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.

Modulizer

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)
mp.run()

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

m.resume()

instead of m.run(). 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

m.recompute()

By default, all intermediate files will be created in directory modular.parts 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