116fe8654f
This translator algorithm is seldom used in practice because we work with explicit automata everywhere, and this is only useful to build symbolic automata. Furthermore, the symbolic automata produced by this algorithm are larger (when looked at explicitly) than those produced by ltl2tgba_fm or other explicit translators. The nice side effect of this removal is that we can also remove a lot of supporting classes, that were relying a lot on BDDs. * src/tgba/public.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbatest/bddprod.test, src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: Delete all these files. * bench/ltlcounter/Makefile.am, bench/ltlcounter/README, bench/ltlcounter/plot.gnu, bench/ltlcounter/run, src/tgba/Makefile.am, src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am, src/tgbatest/cycles.test, src/tgbatest/dupexp.test, src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcross.test, src/tgbatest/ltlprod.cc, src/tgbatest/spotlbtt.test, src/tgbatest/wdba.test, src/tgbatest/wdba2.test, src/tgba/tgbaexplicit.hh, wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in, wrap/python/spot.i, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: Adjust.
24 lines
897 B
Text
24 lines
897 B
Text
In the following paper by Rozier & Vardi, a class of LTL formula
|
|
describing counters was used to stress many translators.
|
|
|
|
@InProceedings{ rozier.07.spin,
|
|
author = {Kristin Y. Rozier and Moshe Y. Vardi},
|
|
title = {LTL Satisfiability Checking},
|
|
booktitle = {Proc. the 12th International SPIN Workshop on
|
|
Model Checking of Software (SPIN'07)},
|
|
pages = {149--167},
|
|
year = {2007},
|
|
volume = {4595},
|
|
series = {LNCS},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
For a description of these formulae, you may also see
|
|
http://ti.arc.nasa.gov/m/profile/kyrozier/benchmarking_scripts/node5.html
|
|
|
|
This benchmark used this familly of formulae to plot the performance
|
|
of the ltl2tgba_fm algorithm. Studying the behaviour of ltl2tgba_fm
|
|
on this class of formulae helped us to improve the translation.
|
|
|
|
Execute "./run" to compute the raw numbers, then execute
|
|
"gnuplot plot.gnu" to plot the figures.
|