* 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.
(No test, this is just a simple backport of a fix from the development
branch, where it is tested.)
* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* NEWS: Mention it.
* 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/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/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: 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/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.
* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh:
Add option to generate a complete deterministic automaton.
* src/tgbatest/randtgba.cc: Test it.
The ltl_to_tgba_fm() translation function was using a hash_map of
maps (ugh!) to merge transitions on output. However recent libstd++
changed the implementation of hash_map (a.k.a. unordered_map) causing
transitions to be output in a different order. This
implementation-dependent order caused the ltl2ta.test to fail because
the BA->TA transformation can produce TA of different sizes if you
simply change the order of transitions in the input BA! This does not
sound like a nice property for the BA->TA transformation, but Ala Eddine
isn't sure how to fix it yet. In the meantime, this patch makes sure
ltl_to_tgba_fm() will return the same output regardless of the
implementation of hash_map.
The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
and with gcc-snapshot (5.0.0 20141016) on Debian.
* src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
using a std::vector and std::sort instead of nested maps tables.
* src/tgbatest/ltl2ta.test: Adjust sizes to the new order.
* NEWS: Mention the fix.
The ltl_to_tgba_fm() translation function was using a hash_map of
maps (ugh!) to merge transitions on output. However recent libstd++
changed the implementation of hash_map (a.k.a. unordered_map) causing
transitions to be output in a different order. This
implementation-dependent order caused the ltl2ta.test to fail because
the BA->TA transformation can produce TA of different sizes if you
simply change the order of transitions in the input BA! This does not
sound like a nice property for the BA->TA transformation, but Ala Eddine
isn't sure how to fix it yet. In the meantime, this patch makes sure
ltl_to_tgba_fm() will return the same output regardless of the
implementation of hash_map.
The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
and with gcc-snapshot (5.0.0 20141016) on Debian.
* src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
using a std::vector and std::sort instead of nested maps tables.
* NEWS: Mention the fix.
* src/tgba/tgbasafracomplement.cc: Here. Beside being more efficient,
the use of std::swap instead of an assignment also protects us from a
bug recently introduced in the development version of G++.
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=63698
