* NEWS: mention this fix.
* bench/stutter/stutter_bench.sh, bench/stutter/user.sh: Path to spot
binaries would include an inexistant src directory.
* bench/stutter/stutter_invariance_formulas.cc: Add override qualifier
to satisfy -Wsuggest-override.
* bench/dtgbasat/config.bench: Configuration file sample used by gen.py
* bench/dtgbasat/gen.py: Script that can generate both bench script and
pdf results.
* bench/dtgbasat/stats.sh: Change stat.sh into stat-gen.sh that will be
generated by gen.py script.
* bench/dtgbasat/Makefile.am: Add new files.
* bench/dtgbasat/README: Update README.
* bench/dtgbasat/stat-gen.sh: Add stat script generated by gen.py and
default config.bench file.
* NEWS: Mention the change.
* src/: Rename as ...
* spot/: ... this, adjust all headers to include <spot/...> instead of
"...", and adjust all Makefile.am to search headers from the top-level
directory.
* HACKING: Add conventions about #include.
* spot/sanity/style.test: Add a few more grep to catch cases
that do not follow these conventions.
* .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
debian/rules, doc/Doxyfile.in, doc/Makefile.am,
doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am,
iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
The previous code was sometime doing the work of remove_fin() in
addition to complementing the acceptance conditions. This separate
the two operations clearly. Also the specialized code for
complementing weak automata is now a specialized code for remove_fin()
on weak automata.
* src/twaalgos/dtgbacomp.hh, src/twaalgos/dtgbacomp.cc: Rename as ...
* src/twaalgos/complement.hh, src/twaalgos/complement.cc: ... these.
* src/twaalgos/Makefile.am: Adjust.
* src/twaalgos/complement.hh (dtgba_complement): Rename as ...
(dtwa_complement): ... this, and restrict the purpose to completion
and accetance complementation. Further acceptance simplification
can be done with remove_fin() and to_generalized_buchi().
* src/twaalgos/remfin.cc (remove_fin): Specialize handling of weak
automata using the code that was originally in dtgba_complement().
Also mark the output as state-based when the input has to Inf.
* src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Make sure
scc_filter is always called after to_generalized_buchi().
* bench/stutter/stutter_invariance_randomgraph.cc,
src/bin/ltlcross.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
src/twaalgos/powerset.cc, src/twaalgos/stutter.cc: Adjust usage.
* src/tests/dstar.test, src/tests/ltl2dstar4.test,
src/tests/remfin.test: Adjust expected outputs.
* wrap/python/spot_impl.i: Export dtwa_complement().
Flatten the formula ltl::formula hiearchy into a single ltl::vnode that
has an enumerator to distinguish the types of node, and a common
interface to access children, update reference counts, etc. The
ltl::formula class is now a thin wrapper around an ltl::vnode pointer to
keep track of reference counts automatically. Visitor are not used
anymore; we now have map() and traversor() methods that are more
concise.
This basically fixes#43, but should be followed by some fine tuning
that should now be localized to the formula.hh and formula.cc files.
Some statistics about this patch. I started working on it on Sep 9, had
a first compiling version two weeks later on Sep 22, and it then took 5
days to fixes the ~70 distincts bugs that were introduced during the
conversion. About 13200 lines were modified, and one third of those
were removed.
* src/ltlast/formula.cc, src/ltlast/formula.hh: Complete rewrite,
including what was in separate nearby files.
* src/ltlast/allnodes.hh, src/ltlast/atomic_prop.cc,
src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh,
src/ltlast/bunop.cc, src/ltlast/bunop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlvisit/dump.cc,
src/ltlvisit/dump.hh, src/ltlast/predecl.hh: Delete these files. Their
feature have been merged in formula.hh and formula.cc.
* src/ltlast/visitor.hh, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
src/ltlvisit/dump.hh, src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh:
Delete these files, as we do not use visitors anymore.
* bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, doc/org/tut01.org,
doc/org/tut02.org, doc/org/tut10.org, doc/org/tut22.org,
iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc,
src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.cc,
src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripkeparse/kripkeparse.yy, src/ltlast/Makefile.am,
src/ltlenv/declenv.cc, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
src/ltlparse/ltlparse.yy, src/ltlparse/public.hh,
src/ltlvisit/Makefile.am, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/dot.cc, src/ltlvisit/dot.hh,
src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh,
src/ltlvisit/length.cc, src/ltlvisit/length.hh, src/ltlvisit/mark.cc,
src/ltlvisit/mark.hh, src/ltlvisit/mutation.cc,
src/ltlvisit/mutation.hh, src/ltlvisit/nenoform.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/print.cc, src/ltlvisit/print.hh,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh,
src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh,
src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc,
src/ltlvisit/snf.hh, src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh,
src/parseaut/parseaut.yy, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
src/taalgos/minimize.cc, src/taalgos/tgba2ta.cc, src/tests/bare.test,
src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/isop.test, src/tests/kind.cc, src/tests/length.cc,
src/tests/ltldo.test, src/tests/ltlfilt.test, src/tests/ltlgrind.test,
src/tests/ltlprod.cc, src/tests/ltlrel.cc,
src/tests/parse_print_test.cc, src/tests/parseaut.test,
src/tests/parseerr.test, src/tests/randtgba.cc, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/taatgba.cc,
src/tests/tostring.cc, src/tests/twagraph.cc, src/tests/utf8.test,
src/twa/acc.cc, src/twa/bdddict.cc, src/twa/bdddict.hh,
src/twa/bddprint.cc, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twa.hh
src/twa/twagraph.cc, src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
src/twaalgos/minimize.cc, src/twaalgos/minimize.hh,
src/twaalgos/neverclaim.cc, src/twaalgos/postproc.cc,
src/twaalgos/postproc.hh, src/twaalgos/powerset.cc,
src/twaalgos/powerset.hh, src/twaalgos/randomgraph.cc,
src/twaalgos/remprop.cc, src/twaalgos/remprop.hh, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh,
src/twaalgos/translate.cc, src/twaalgos/translate.hh,
wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
wrap/python/spot_impl.i, wrap/python/Makefile.am,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/formulas.ipynb,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py, wrap/python/tests/randltl.ipynb: Adjust
to use the new interface.
* src/sanity/style.test: Accept more C++11 patterns.
* NEWS: Mention the change.
* doc/org/install.org: New file.
* doc/Makefile.am: Add it.
* doc/org/index.org: Link to it.
* doc/org/setup.org: Add macro for
various version numbers.
* doc/org/tools.org: Update version number.
* NEWS, README, bench/ltl2tgba/README, debian/control,
debian/copyright: Update URLs to website.
* src/tgbaalgos/stutter.cc: Add a new variant of Etessami's check,
closer to his original paper in IPL.
* src/ltltest/stutter.test: Add more tests.
* bench/stutter/user.sh: Include this new variant in the benchmark.
* bench/stutter/stutter_invariance_randomgraph.cc: Update to recent
changes. If an algorithm took more that 30s on an average for a set of
parameters, avoid running it with more states. Take the density and
ap count as parameter. Output all the algorithms on the same line.
Add additional statistics about automata.
* bench/stutter/stutter_invariance_formulas.cc: Update to recent
changes. Output all the algorithms on the same line.
Add additional statistics about automata.
* bench/stutter/stutter_bench.sh: Use a Makefile to manage concurrency.
* bench/stutter/README: Update.
Compared to 1.1.0, -L/-M have been renamed to -M0,-M1.
* bench/ltl2tgba/tools, bench/spin13/README,
bench/spin13/run.sh, doc/org/ltlcross.org,
wrap/python/ajax/spot.in: Adjust all references.
ltl3ba 1.1.0 was released today
* wrap/python/ajax/spot.in: Use -T3 instead of -U.
* wrap/python/ajax/README: Adjust version.
* wrap/python/ajax/ltl2tgba.html: Turn on improved determinism
of ltl3ba by default.
* bench/ltl2tgba/tools, bench/spin13/run.sh: Adjust options.
* bench/spin13/README: Mention the update.
Those where never really publicized because they were slow and we failed
to fix what we hopped to fix with them. They where never used by
default. Getting rid of them will make it easier to cleanup the
simulation code.
* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Remove
the simulation code.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
src/tgbatest/ltl2tgba.cc: Do not call it.
* src/bin/spot-x.cc: Update doc.
* src/tgbatest/sim.test: Delete this file.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/spotlbtt.test, bench/ltl2tgba/tools.sim:
Remove uses to don't care simulation.
the existing -q/--quiet option is renamed to --ignore-errors
* src/bin/ltlfilt.cc: Adjust option.
* src/bin/common_output.cc, src/bin/common_output.hh: Add a
quiet_output.
* bench/dtgbasat/prepare.sh: Rename -q to --ignore-errors..
* src/ltltest/remove_x.test: Use -q.
* NEWS: Mention this change.
* bench/stutter/stutter_bench.sh: Add headers in the CSV files, and also
run stutter_invariance_randomgraph.
* bench/stutter/stutter_invariance_formulas.cc: Remove space from CSV
output.
* bench/stutter/stutter_invariance_randomgraph.cc: Likewise, plus fix
the call to is_stutter_invariant(), and return an average time.
* bench/stutter/stutter.ipynb: Adjust.
* bench/stutter/README: Simplify.
* bench/stutter/Makefile.am: Distribute the script and python notebook.
* bench/stutter/stutter_bench.sh: Collect benchmarks for different
number of atomic propositions in a single csv file.
* bench/stutter/stutter.ipynb: Visualize benchmarks generated by
stutter_bench.sh.
* src/ltlvisit/apcollect.hh,
src/ltlvisit/apcollect.cc (create_atomic_prop_set): New function.
* src/bin/randltl.cc, bench/stutter/stutter_invariance_randomgraph.cc:
Use it.
* src/ltltest/ltlfilt.test: Add more tests.
* src/ltltest/stutter.test: New test.
* src/ltltest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Catch std::runtime_error.
* src/tgba/tgbasl.hh (make_tgbasl): New function.
* src/tgba/tgbagraph.hh (make_tgba_graph): Add another overload.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Take the algorithm version as an
optional integer, and call getenv() only once.
* bench/stutter/stutter_invariance_randomgraph.cc,
bench/stutter/stutter_invariance_formulas.cc: Simplify using the
above functions.
* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh: Using vectors
instead of sets and unordered maps, adding an overload to handle rvalue
references.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Adding
an overload to handle rvalue references.
* bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc: Automata are modified
in-place by is_stutter_invariant so they have to be copied before being
processed.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Use the in-place version of
closure and sl.
* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
Add closure function.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
Add two implementations of "self-loopize" function.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
self-loopize.
* src/tgba/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
closure and sl.
* src/tgbatest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Modify stutter-invariant option to use
automaton-based checking rather than syntactic-based checking.
* src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
Remove is_stutter_insensitive function.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Check if a formula is
stutter-invariant using closure and sl.
* wrap/python/spot.i: Add closure and sl bindings.
* bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
given formulas.
* bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
from random automata.
* bench/stutter/Makefile.am: Add them.
* configure.ac: Add bench/stutter/Makefile.
* bench/Makefile.am: Add stutter subdirectory.
* README: Document bench/stutter directory.
These were used in old experiments, but have not turned useful in
practice. Not worth keeping and maintaining.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Delete.
* bench/scc-stats/, bench/split-product/: Delete.
* configure.ac, src/tgbaalgos/Makefile.am, README, bench/Makefile.am:
Adjust.
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.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Record
statistics about intermediate automata if SPOT_SATLOG is set to some
filename, and display intermediate automata if SPOT_SATSHOW is set.
* bench/dtgbasat/stat.sh, bench/dtgbasat/stats.sh,
bench/dtgbasat/tabl.pl, bench/dtgbasat/tabl1.pl,
bench/dtgbasat/tabl2.pl, bench/dtgbasat/tabl3.pl,
bench/dtgbasat/tabl4.pl: Gather these extra statistics.
