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.
* AUTHORS: Add Thibaud.
* NEWS: Mention ltlgrind and ltlcross --grind.
* src/ltlvisit/mutation.hh, src/ltlvisit/mutation.cc:
Use an enum instead of #define. Rename get_mutations()
into mutate(). Other minor cosmetic changes.
* src/bin/ltlgrind.cc: Adjust.
* src/bin/ltlcross.cc: Slight changes the the output
* doc/org/ltlcross.org, doc/org/ltlgrind.org: Minor
rewordings and fix for org-mode syntax.
* src/ltltest/ltlcrossgrind.test,
src/ltltest/ltlgrind.test: Fix copyright year.
This was never actually used and we have a new implementation of
alternating automata coming.
* src/saba/, src/sabaalgos/, src/sabatest/: Remove.
* src/Makefile.am, configure.ac, README: Adjust.
* NEWS: Mention it.
This is a huge patch, that took over a month to complete. The bit sets
are currently restricted to what 'unsigned can store', but it should be
easy to extend it to 'uint64_t' should we need it.
* NEWS: Update.
* src/tgba/acc.hh: New file.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
* src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete. The KV
complementation is too slow to be used in practice, and I somehow broke
it during the conversion to bitsets. The tgba->sgba conversion was only
used for the KV complementation, and should be better redone on
tgba_digraph_ptr should it be needed again.
* src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh,
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/ta/tgta.cc,
src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc,
src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/Makefile.am, src/tgbatest/complementation.cc,
src/tgbatest/complementation.test, src/tgbatest/degenlskip.test,
src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test,
src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test,
src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc,
src/tgbatest/readsave.test, src/tgbatest/sim.test,
src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
iface/dve2/dve2.cc: Adjust or use to the new acceptance interface.
Reported by Joachim Klein.
* src/neverparse/neverclaimparse.yy: Store labels and the
location of their first definition in a global map to catch
redefinitions.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention it.
Suggested by Joachim Klein.
* wrap/python/ajax/ltl2tgba.html: New option.
* wrap/python/ajax/protocol.txt, NEWS: Document it.
* wrap/python/ajax/spot.in: Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.
The specifications are at http://adl.github.io/hoaf/
* src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/tgbatest/ltl2tgba.cc: Add option to output HOA.
* NEWS: Mention it.
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.
Fortunately was only enabled with the
ltl_simplifier_options::favor_event_univ option, which cannot yet be
turned on from the command-line tools.
* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/eventuniv.test: Adjust.
* NEWS: Mention the bug.
* src/ltlvisit/simplify.cc: Remove two incorrect rules, and
partially disable another one.
* doc/tl/tl.tex: Reflect the change.
* src/ltltest/reduccmp.test: Likewise.
* src/ltltest/equals.cc: Add safety checks to catch such errors in the
future.
* NEWS: Mention the bug.
* src/taalgos/tgba2ta.cc: Do not assume the input is an sba.
* src/tgbatest/ltl2ta2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention the fix.
