Thibaud Michaud authored Nov 17, 2014 and Alexandre Duret-Lutz committed Nov 29, 2014

* src/tgbaalgos/stutter_invariance.hh: Add documentation.

* wrap/python/ajax/spot.in: Adjust to the new interface.
* wrap/python/spot.i: Work around missing support for nested classes.
* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: More
test.

* 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.

Thibaud Michaud authored Nov 17, 2014 and Alexandre Duret-Lutz committed Nov 26, 2014

* bench/stutter/README: Document stutter-invariance benchmarks.

Thibaud Michaud authored Nov 14, 2014 and Alexandre Duret-Lutz committed Nov 26, 2014

* 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/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: Rename to...
* src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh: ... these, and
fix the function names.
* src/tgbaalgos/Makefile.am, src/bin/autfilt.cc,
src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/tgbatest/ltl2tgba.cc:
Adjust all calls.

* src/tgbatest/hoaparse.test: More tests.

* src/tgbatest/hoaparse.test: More test.

* src/tgbatest/hoaparse.test: Add test.

* src/hoaparse/hoascan.ll: Remove superfluous line.
* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* src/tgbatest/hoaparse.test: Test it.

* src/bin/autfilt.cc: Catch exception.
* src/tgbatest/hoaparse.test: Test it.

* src/hoaparse/hoaparse.yy: Improve error reporting
in case labeled edges are mixed with unlabeled edges.
* src/hoaparse/hoascan.ll: Fix handling of nested comments.
* src/tgbatest/hoaparse.test: More coverage.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: More tests.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Add tests.

* src/bin/ltlcross.cc: Here.
* src/tgbatest/ltlcross3.test: Add test case.

* src/hoaparse/parsedecl.hh (hoa_abort): New structure.
* src/hoaparse/hoascan.ll: Throw hoa_abort on --ABORT--.
* src/hoaparse/hoaparse.yy: Deal with this exception.
* src/hoaparse/public.hh: Add a boolean flag to mark aborted automata.
* src/bin/autfilt.cc: Report aborted automata.
* src/tgbatest/hoaparse.test: Add test case.

* src/hoaparse/hoaparse.yy: Allocate state after parsing the entire
header, not right after passing "States:".
* src/tgbatest/hoaparse.test: Reflect improved error message
about initial state.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: More tests.
* src/tgba/acc.hh (operator^=): New method.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: More test.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Add tests.

* src/hoaparse/hoaparse.yy: Improve error recovery,
and fix location tracking in streams.
* src/hoaparse/public.hh: Store the last location so
that the next parse start at the correct position.
* src/bin/autfilt.cc: Stop parsing a stream on irrecoverable errors.
* src/tgbatest/hoaparse.test: Adjust tests.

* src/tgbatest/monitor.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbaalgos/minimize.cc (minimize_monitor): Mark
the output automaton as state-based.
* src/tgba/tgbagraph.hh: Assume automata with 0 acceptance sets are also
state-based.

* src/bin/autfilt.cc, src/bin/dstar2tgba.cc: Do not reference the
formula in --help.

* src/bin/autfilt.cc: Loop over all automata in a file.
* src/hoaparse/public.hh: Turn the parser into an object.
* src/hoaparse/hoaparse.yy: Adjust.

* src/bin/autfilt.cc, src/bin/man/autfilt.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* src/bin/common_post.cc, src/bin/common_post.hh: Adjust.

* src/bin/ltlcross.cc: Add a %H modifier.
* src/tgbatest/ltlcross2.test: Exercise it.

* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
* src/Makefile.am, configure.ac, README: Adjust.
* src/tgbatest/ltl2tgba.cc: Add a -XH option.
* src/tgbatest/hoaparse.test: New file.
* src/tgbatest/Makefile.am: Adjust.
* buddy/src/bddx.h: Add a bdd_from_int() function.

* src/tgbaalgos/hoaf.cc: Do not initialize acc_cond::mark_t with -1U.

* src/dstarparse/dstarscan.ll, src/kripkeparse/kripkescan.ll,
src/neverparse/neverclaimscan.ll, src/tgbaparse/tgbascan.ll:
Distinguish between 1-sized EOL and 2-sized EOL.
* src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Add more tests.
* NEWS: Mention it.
* src/kripkeparse/scankripke.ll: Remove this unused file.

Because src/ltltest/stutter.test is stronger.

* src/tgbatest/stutter_invariant.test: Remove.
* src/tgbatest/Makefile.am: Adjust.