* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New argument
to disable the "jump to the accepting level if the entering
state as an accepting self-loop" optimization.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Check
the degen-lowinit option and pass it on to degeneralize().
* src/bin/spot-x.cc: Document it.
* src/tgbatest/degenlskip.test: Add some tests.
* src/tgbatest/ltl2ta.test: Update value. We output less
accepting states now.
... and use it to sort transitions.
* src/graph/graph.hh: Adjust storage of source index. Provide
remove_dead_transitions_(), sort_transitions_() and
chain_transitions_() methods.
* src/tgba/tgbagraph.cc (merge_transitions): Rewrite using
above methods.
* src/tgba/tgbagraph.hh: Add a comparison operator for
transitions.
* src/tgbatest/degenlskip.test, src/tgbatest/det.test,
src/tgbatest/ltl2ta.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Adjust expected transition order in test
cases.
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.
This involves reimplementing some algorithms using tgba_digraph, and
implementing an explicit product that takes two tgba_digraphs and
produces a tgba_digraph.
* src/tgbaalgos/product.cc, src/tgbaalgos/product.hh: New files.
* src/tgbaalgos/Makefile.am: Adjust.
* src/bin/ltlcross.cc, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc: Update to use scc_info and/or tgba_digraph.
The bug was reported by Joachim Klein.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Reduce P(a M b) to P(a & b), not to P(a).
* src/tgbatest/ltlcross.test: Test Joachim's formula.
* src/tgbatest/ltl2ta.test: Adjust some expected values.
* NEWS: Mention the bug.
Again instead of calling ltl2tgba dozen of times with different options
for various formulas, this implements a single executable that reads
formulas from a file, translate them using the different setups, and
dump statistics for comparison. Valgrind now only has to be started
once.
* src/tgbatest/checkta.cc: New file.
* src/tgbatest/Makefile.am: Use it.
* src/tgbatest/ltl2ta.test: Rewrite using checkta.
* src/tgbatest/ltl2tgba.cc: Remove a unused variable.
* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case that is improved
by this.
* src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.test: Adjust.
* src/tgbaalgos/sccfilter.cc: Compute useless variable SCC-wise, then
renumber the useful variables so that they can be shared between SCCs.
* src/tgbatest/sccsimpl.test, src/tgbatest/ltl2ta.test: Adjust test
cases.
* src/ta/tgta.hh, src/ta/tgta.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/ta/tgtaproduct.cc,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/emptinessta.hh, src/taalgos/emptinessta.hh,
src/taalgos/emptinessta.cc, src/taalgos/tgba2ta.hh,
src/taalgos/tgba2ta.cc: rename tgbta to tgta
in this source files.
* src/ta/tgbtaexplicit.hh, src/ta/tgbtaproduct.hh, src/ta/tgbta.cc,
src/ta/tgbtaproduct.cc, src/ta/tgbta.hh, src/ta/tgbtaexplicit.cc:
Rename as...
* src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
src/ta/taproduct.hh, src/ta/tgtaexplicit.cc: ... these.
* src/taalgos/sba2ta.hh, src/taalgos/sba2ta.cc: deleted because
the implementation of all the transformations beteween TGBA and
the different forms of TA are new implemented in src/taalgos/tgba2ta.hh
and src/taalgos/tgba2ta.cc.
* src/tgbatest/ltl2tgba.cc: rename the options of commands that build
the different forms of TA.
* src/ta/ta.hh: BUG Fix
* src/ta/Makefile.am, src/tgbatest/ltl2ta.test: impacts of this renaming
* src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/taproduct.cc,src/ta/taproduct.hh,
src/taalgos/dotty.cc, src/taalgos/emptinessta.cc,
src/taalgos/emptinessta.hh, src/taalgos/minimize.cc,
src/taalgos/reachiter.cc, src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Impacts of the
implementation of a new variant of TA, called STA, which involve a
Single-pass emptiness check. The new options (-in and -lv) added to
build the new variants of TA allow to add two artificial states:
1- an initial artificial state to have an unique initial state (-in)
2- a livelock artificial state which has no successors in order to
obtain the new form of TA which requires only a Single-pass emptiness-
check: STA (-lv).
