genem-exp

Application 1: Emptiness check of ω-automata in Spot

This directory contains artifacts for the benchmark of application 1 (emptiness check of ω-automata in Spot) in our ATVA’19 submission titled Generic Emptiness Check for Fun and Profit.

This benchmark was run with the development version of Spot that will eventually become Spot 2.8. A tarball of this version is given below. Measurements made in generic-is-empty.ipynb and saved in bench.csv were done on an Intel Core i7-6820HQ CPU (2.70GHz) running Linux. Most of the automata generated in the datasets where generated by the aforementioned development version of Spot; automata from b4.hoa.gz also used ltl2dstar 0.5.4.

The following files are supplied:

• b2.hoa.gz: Automata for the random dataset
• b2b.hoa.gz: Automata for the random-rep dataset
• b3.hoa.gz: Automata for the Rabin dataset
• b4.hoa.gz: Automata for the Streett dataset
• b5.hoa.gz: Automata for the parity-like dataset
• generic-is-empty.ipynb : Jupyter notebook containing Python code for:
  • Python implementation of the is_empty() algorithm from the paper (called is_empty1() in the notebook)
  • Python implementation of the optimizations described in the Application 1 section (called is_empty2() in the notebook)
  • a version of is_empty() that displays a trace of its execution (with intermediate automata), so that one can execute the algorithm on any automaton.
  • code for regenerating the automata from the datasets if the above files are missing
  • code for executing the is_empty1(), is_empty2(), as well as the C++ version of is_empty2() and the previous implementation of that emptiness check, in order to regenerate bench.csv
• bench.csv: Result of the experiments, as a CSV file. Each line correspond to an automaton from one data set. The following columns are used:
  • Python/is_empty1 runtime of is_empty1(), in ms
  • Python/is_empty2 runtime of is_empty2(), in ms
  • C++/is_empty runtime of the C++ implementation, in ms
  • C++/old_is_empty runtime of the former C++ method for generic emptiness check, in ms
  • /result contains TTTT if all emptiness check agree the automaton is empty, FFFF if they all agree it is non empty
  • aut/states number of states in the input automaton
  • aut/edges number of edges in the input automaton
  • aut/sccs number of SCCs in the input automaton
  • aut/ntsccs number of non-trivial SCCs in the input automaton
  • aut/nrsccs number of “non-obviously rejecting” SCCs of the input automaton (an SCC is obviously rejecting if it is trivial or if the checks of lines 7–12 are enough to decide emptiness, in this case no recursion is needed)
  • aut/nrstates number of states in the non-obviously rejecting” SCCs of the input automaton
  • aut/sets number of acceptance sets in the input automaton
  • aut/acc acceptance condition used by the input automaton
  • /bench name of the dataset the automaton belongs to
• generic-is-empty-plot.ipynb : Jupyter notebook containing R code for generating tables and figures from bench.csv.
• spot-2.7.4.dev.tar.gz: The development version of Spot used for this benchmark. This will eventually be released as Spot 2.8.

The easiest way to play with those files is via mybinder . Clicking the previous link will setup a Jupyter instance in the cloud, including a copy of Spot, as well as the necessary Python and R dependencies for the above notebooks.

If you would like to run these notebooks locally on your own installation, please first install the following:

• Make sure you have Python3 with header files (python-dev or libpython3-dev in most Linux distributions)
• Install the scipy and pandas Python packages.
• Install jupyter
• Install R
• Start R and run install.packages(c("tidyverse", "ggplot2", "tables", "tikzDevice", "IRkernel"))
• If you plan to execute generic-is-empty-plot.ipynb to the end, install LaTeX with at least the packages tikz (often shipped by distributions in a texlive-pictures package) and preview (can be called preview-latex-style in some distributions).
• Install spot-2.7.4.dev.tar.gz with ./configure --disable-devel; make -j4; sudo make install.
• Then you should be able to start the notebook server with jupyter notebook.

This site is open source. Improve this page.