Index of /~adl/spin15

	Name	Last modified	Size	Description
	Parent Directory		-
	README	2021-05-20 16:05	2.5K
	bench_formulas.csv.gz	2021-05-20 16:05	1.9M
	bench_randgraph.csv.gz	2021-05-20 16:05	911K
	ltl-user-bench.csv	2021-05-20 16:05	475
	spot-1.99b.tar.gz	2021-05-20 16:05	11M
	stutter-bench.pdf	2021-05-20 16:05	5.3M

These files contain benchmarking data for the submission
  "Practical Stutter-Invariance Checks for ω-Regular Languages",
written by Thibaud Michaud and Alexandre Duret-Lutz.

The stutter-bench.pdf contains a description and some graphical
exploration of the data in the CSV files.

To recreate the CSV files, use the following commands:

# Download the development version of Spot and unpack it
wget http://www.lrde.epita.fr/~adl/spin15/spot-1.99b.tar.gz
tar zxvf spot-1.99b.tar.gz
cd spot-1.99b
# Configure Spot and build it
./configure --prefix ~/usr --disable-debug --enable-optimization --disable-python
make -j4
# Run the benchmark
cd bench/stutter
make -j4
./stutter_bench.sh -j4

(Adjust all the -j4 options to the number of cores you want to use.)

If you are interested into the latest development version of Spot
(i.e., not using *exactly* the version we used for this benchmark),
head over to
   https://gitlab.lrde.epita.fr/spot/spot/wikis/DevSnapshots


If you are interested in using the ltlfilt tool to decide
stutter-invariance of some LTL formulas, you can read some
documentation at https://spot.lrde.epita.fr/ltlfilt.html

UPDATE: Since 2018, you can check stutter-invariance
online using the "study" tab of https://spot.lrde.epita.fr/app/

What is not documented is how to select the stutter-invariance check
algorithm to use.  By default "ltlfilt --stutter-invariant" uses the
cl(A)*cl(!A) approach, but you can define the SPOT_STUTTER_CHECK
environment variable to a number between 0 and 9 to select the
algorithm to use (the meaning of these numbers is the same as used in
the CSV files, and is documented in stutter-bench.pdf).

So
   SPOT_STUTTER_CHECK=0 ltlfilt --stutter-check -f 'F(a & X(!a & b))'
will run a check using Etessami's τ function (this was our former
only implementation), while
   SPOT_STUTTER_CHECK=8 ltlfilt --stutter-check -f 'F(a & X(!a & b))'
runs the cl(A)*cl(!A) approach (this is the new default implementation).


The distribution also includes also a tool called "autfilt" that
can filter and transform automata.  In particular it has three
options
   --instut
   --instut=2
   --destut
that respectively apply the algorithms defined as sl(), sl_2() and
cl() in the paper, on any given automaton given (the automaton can be
written as a never claim, in LBTT's format, or in the Hanoi Omega
Automata format).  These options, combined with other services (like
--intersect to decide whether the language of two automata have a
common word) allow to experiment with the different steps of the
constructions.