* src/bin/common_post.cc: Handle the options
for BA/TGBA/Monitor as well as Complete/SBAcc here,
and in the same group. Rename "Translation intent"
and "Optimization level" to "Simplification goal" and
"Simplification level" so that it makes sense even
in autfilt.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc: Remove common code.
* doc/org/autfilt.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org: Adjust sed invocations.
These now become twa_run::reduce, twa_run::replay, and
twa_run::as_twa.
* src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh,
src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh: Delete.
* src/twaalgos/Makefile.am: Adjust.
* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh: Move
the above functions here, as method of twa_run.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
wrap/python/ajax/spotcgi.in, iface/ltsmin/modelcheck.cc: Adjust.
* NEWS: List the renamings.
This simplify all laters invocations, because we do not have to pass
the automaton the run was generated on.
This fixes#113 by allowing the __str__ function to be implemented on
runs.
* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (twa_run):
Store the automaton.
(prin_twa_run): Rewrite as an overloaded <<.
* src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh (reduce_run):
Do not like the automaton as a parameter.
* src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh (replay_twa_run):
Likewise.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/complementation.cc, src/tests/ikwiad.cc,
src/tests/randtgba.cc, src/twaalgos/gtec/ce.cc, src/twaalgos/gv04.cc,
src/twaalgos/magic.cc, src/twaalgos/ndfs_result.hxx,
src/twaalgos/se05.cc, src/twaalgos/projrun.cc: Adjust.
* wrap/python/ajax/spotcgi.in: Add a __str__ function to twa_run_ptr.
* wrap/python/spot_impl.i: Adjust.
Fixes#114.
* src/parseaut/public.hh: Add support for a trust_hoa option.
* src/parseaut/parseaut.yy: If trust_hoa is set, recognize the
"inherently-weak" and "stutter-invariant" properties.
* src/bin/common_conv.cc, src/bin/common_conv.hh (read_automaton):
Move...
* src/bin/common_hoaread.cc, src/bin/common_hoaread.hh: ... in this
new file, that also handle the --trust-hoa option.
* src/bin/Makefile.am: Add them.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/bin/ltldo.cc: Use them.
* src/tests/parseaut.test, src/tests/ltldo.test: Adjust, and test
--trust-hoa=no.
* src/tests/complement.test, src/tests/prodor.test,
src/tests/sbacc.test: Adjust.
* wrap/python/spot.py (automata): Add option trust_hoa.
* NEWS: Update.
* src/parseaut/public.hh, src/parseaut/parseaut.yy: Make it easier to
pass new options to the parser.
* src/tests/ikwiad.cc, wrap/python/spot.py: Adjust.
This occured when parsing the HOA automaton generated by Rabinizer3 for
a very long LTL formula with many nested U. State labels could easily
be more than 40k characters.
* src/parseaut/scanaut.ll: Fix that.
* src/tests/parseaut.test: New test case.
* NEWS: Mention the fix.
* src/tests/unambig.test: New test case. Reported by Ming-Hsien Tsai.
* src/twaalgos/sccfilter.cc: Always create an initial state.
* src/twaalgos/isunamb.cc: Speed up on empty languages.
* NEWS, THANKS: Update.
This is a bug:
% ltlfilt -f 'a W b' --unabbreviate=WR
a U (b | (a W b))
* src/tl/unabbrev.cc: Here.
* src/tests/unabbrevwm.test: Harden test case.
* wrap/python/tests/randltl.ipynb: Adjust expected output.
* NEWS: Mention the fix.
This additionally fixes#107.
* src/bin/ltlgrind.cc: Fix handling for FILEANAME/COL. Document FORMAT
in --help. Assume -F for arguments given without options.
* src/tests/ltlgrind.test: Add two tests.
* NEWS: Mention this.
This is motivated by an email from Fanda.
* src/bin/common_post.cc, src/bin/common_post.hh: Add variables to
detect when level or pref are sets.
* src/bin/autfilt.cc: Adjust default for pref/sets.
* src/tests/readsave.test: Add test cases.
* NEWS: Mention it.
* src/twaalgos/randomgraph.cc: Replace an assertion by an exception.
* src/bin/randaut.cc: Diagnose -Q0.
* src/tests/randaut.test: Test it.
* NEWS: Mention the bug.
* src/twaalgos/sccfilter.hh,
src/twaalgos/sccfilter.cc (scc_filter_states): Remove useless acceptance
marks while preserving state-based acceptance. Add a new argument
to specify if all useless mark have to be removed, like for scc_filter.
* src/twaalgos/simulation.cc: Use the new parameter.
* src/twaalgos/postproc.cc: Likewise. Also call do_scc_filter even
after WDBA simplification to cleanup trivial SCCs. Preserve state-based
acceptance for weak automata.
* src/tests/readsave.test: Add one test.
* src/tests/dstar.test, src/tests/prodor.test, src/tests/remfin.test,
src/tests/sim3.test, wrap/python/tests/automata.ipynb,
wrap/python/tests/piperead.ipynb: Adjust expected output.
* NEWS: Mention the change.
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().
* src/twaalgos/postproc.hh: Allow the formula not to be specified. The
code already support that, as it is called with an explicit nullptr in
autfilt (for example), but not requiring the nullptr is better for the
Python bindings.
* src/twaalgos/complete.cc, src/twaalgos/complete.hh
(tgba_complete, tgba_complete_here): Rename as...
(complete, complete_here): ... these. Also fix useless output of
acceptance marks on transition leading to the sink when the automaton
does not use state-based acceptance.
* src/tests/ikwiad.cc, src/twaalgos/dtgbacomp.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/postproc.cc,
src/twaalgos/product.cc: Adjust.
* wrap/python/spot_impl.i: Export these function.
* wrap/python/tests/automata.ipynb: Test spot.complete().
It was only needed with Swig versions older than what we have now.
* src/misc/common.hh: Here.
* src/misc/bitvect.hh, src/misc/common.hh, src/ta/taexplicit.hh,
src/ta/taproduct.hh, src/tl/simplify.hh, src/twa/bdddict.hh,
src/twa/taatgba.hh, src/twa/twaproduct.hh: Use = delete directly.
* src/twaalgos/dupexp.cc, src/twaalgos/dupexp.hh: Rename to...
* src/twaalgos/copy.cc, src/twaalgos/copy.hh: ... these.
Get rid of dupexp_bfs, rename dupexp_dfs as copy, and add
an option to preserve named states.
* src/twaalgos/Makefile.am, src/tests/dupexp.test,
src/tests/ikwiad.cc, src/tests/sccsimpl.test,
src/twa/twagraph.hh, src/twaalgos/dot.cc,
src/twaalgos/stutter.cc, wrap/python/spot_impl.i: Adjust.
* NEWS: Mention this change.
* src/twa/bddprint.cc: Do not store a global shared_ptr to the bdddict
used for printing (a simple pointer is enough), otherwise it risks being
the last shared_ptr to be destroyed, and it might be destroyed after the
unicity maps of the formulas.
False/True are problematic in Python, and I don't like that the
enum is op::False but the constructor formula::ff(). So let's
just use ff and tt everywhere, and also eword instead of EmptyWord.
* src/ltlast/formula.hh (False, True, EmptyWord, AP, is_false, is_true):
Rename to...
(ff, tt, eword, ap, is_ff, is_tt): ... these.
* iface/ltsmin/ltsmin.cc, src/ltlast/formula.cc,
src/ltlvisit/apcollect.cc, src/ltlvisit/dot.cc, src/ltlvisit/mark.cc,
src/ltlvisit/mutation.cc, src/ltlvisit/print.cc,
src/ltlvisit/relabel.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc, src/ltlvisit/unabbrev.cc,
src/twa/acc.cc, src/twa/acc.hh, src/twa/formula2bdd.cc,
src/twaalgos/gtec/gtec.cc, src/twaalgos/hoa.cc, src/twaalgos/ltl2taa.cc,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/neverclaim.cc,
src/twaalgos/product.cc, src/twaalgos/remfin.cc, src/twaalgos/safety.cc,
src/tests/parseerr.test, src/tests/utf8.test, wrap/python/spot.py:
Adjust.
This is actually an attempt to workaround what might be a compiler bug.
(valgrind complains about some uninitialized memory being read on this
line).
* src/ltlvisit/simplify.cc: Here.
