6459877a1a
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and document the api. * spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section. * tests/python/stutter-inv-states.ipynb: Rename as ... * tests/python/stutter-inv.ipynb: ... this, and add more comments. * tests/Makefile.am, doc/org/tut.org: Adjust renaming. * bench/stutter/stutter_invariance_randomgraph.cc, bench/stutter/stutter_invariance_formulas.cc, bench/stutter/Makefile.am: Make it compile again. * bin/autfilt.cc: Call inplace variants. * NEWS: Mention the overhaul. |
||
|---|---|---|
| .. | ||
| .gitignore | ||
| Makefile.am | ||
| README | ||
| stutter.ipynb | ||
| stutter_bench.sh | ||
| stutter_invariance_formulas.cc | ||
| stutter_invariance_randomgraph.cc | ||
| user.sh | ||
This benchmark measures the performance of different algorithms to
check if a property is stutter-invariant. When the benchmark is run
on formulas, the translation time is not included in the measured
time.
To reproduce the benchmark run
% ./stutter_bench.sh -j8
(Adjust -j8 to the number of cores you have.)
This should create three files:
- bench_formulas.csv
running stutter checks on LTL formulas, but without including
LTL translation time.
- bench_randgraph.csv
unning stutter checks on deterministic TGBA, without including
complementation time.
- ltl-user-bench.csv
running stutter checks on LTL formulas, from the user point
of view, i.e., timing the whole "ltlfilt" run.