Python wrapper around the amazing tool ltlcross from Spot library.
The tool compares LTL to automata translators.
The following libraries are needed for bokeh scatter plots (can be used in Jupyter)
pip)pip)python3 -m pip install -U ltlcross_wrapperltlcross_wrapper offers 3 classes:
Modulizer and GoalModulizer split 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. Always use GoalModulizer if one of the compared
tools is GOAL!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)
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.
Some tools need to read the input from (or store the output in) a
temporary file that is different from the one that ltlcross expects.
This file name has to be specified in the command for ltlcross. As
the task will be processed in parallel (unless requested otherwise
with processes=1), we can have a lot of race conditions. For this
purpose, each process created by the Modulizer class set its own
value into an environment variable called $LCW_TMP. You can then
specify tools with commands like
"tool1" : ltl2tgba %f > $LCW_TMP.in.hoa && tool1 $LCW_TMP.in.hoa ...Always use GoalModulizer instead of Modulizer if you need to run
GOAL in parallel. GoalModulizer requires additional parameter
goal_root to specify the path to root directory of GOAL (contains
gc, goal, boot.properties). GoalModulizer uses a unique binary
and a unique shadow folder for each process that runs the task.
The path to the unique binary is stored in environment variable
$LCW_GOAL_BIN which you can use in specification of tools to compare.
The goal_root part of the path should be omitted in the ltlcross
command specification. Specifying GOAL is as simple as
'my_goal_batch` : '$LCW_GOAL_BIN batch "{goals commands}"'If you are using the batch mode of GOAL, you often need to specify the
names of the temporary files in the GOAL command. The $LCW_TMP is
not recognized as a variable inside these commands. Use `echo $LCW_TMP`
which is a nested shell evaluation inside the GOAL command (enclosed in two `).
See an example of complementation performed by GOAL and simplified by
Spot.
tools = {
"piterman": "ltl2tgba -B %f > $LCW_TMP.in && $LCW_GOAL_BIN batch '$temp = complement -m piterman `echo $LCW_TMP.in`; save -c HOAF $temp `echo $LCW_TMP.out;' && autfilt --small --tgba $LCW_TMP.out > %O
"SPOT": "ltl2tgba -B %f | autfilt --complement > %O"
}
m = ltlcross_wrapper.GoalModulizer(goal_root="PATH_TO_GOAL", tools=tools, formula_file="MY_FORMS.ltl")
m.run()TODO: Explain ltlcross options
See the usage notebook. Currently, bokeh scatter plots do not render directly on github so you might consider to see the notebook on nbviewer