Because this parser is not specific to HOA anymore.
* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
src/parseaut/public.hh, src/hoaparse/hoascan.ll,
src/tests/hoaparse.test: Rename to...
* src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
src/hoaparse/public.hh, src/parseaut/scanaut.ll,
src/tests/parseaut.test: ... these, and also adjust the name internally.
For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
automaton_stream_parser, and hoa_parse() has become parse_aut().
* NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh, src/bin/common_conv.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
src/tests/complementation.cc, src/tests/ltl2tgba.cc,
src/tests/readsave.test, wrap/python/ajax/spot.in,
wrap/python/spot.py, wrap/python/spot_impl.i,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
Adjust.
* src/twaalgos/lbtt.hh (print_lbtt): Take a const char* opt argument.
* src/twaalgos/lbtt.cc: Use it, select state-based
vs. transition-based using automaton property, and implement output
for generalized state-based acceptance.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/dstar2tgba.cc: Adjust usage. We do not need to handle
--lbtt=t as a special case anymore.
* src/tests/lbttparse.test, wrap/python/spot.py,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
Adjust.
This actually performs three related changes, but separating them
would be quite inconvenient.
1) rename tostring.hh to print.hh a welcome side-effect is that
I could fix several files that included this file for not reason.
2) de-overload some of the to_string functions, and rename them
as follow:
to_string -> print_psl, print_sere, str_psl, str_sere
to_utf8_string -> print_utf8_psl, print_utf8_sere,
str_utf8_psl, str_utf8_sere
to_spin_string -> print_spin_ltl, str_spin_ltl
to_wring_string -> print_wring_ltl, str_wing_ltl
to_lbt_string -> print_lbt_ltl, str_lbt_ltl
to_latex_string -> print_latex_psl, str_latex_psl
to_sclatex_string -> print_sclatex_psl, str_sclatex_psl
Now it is clearer what these functions do, and their restrictions.
3) all those print_* functions now take the stream to write onto
as their first argument. This fixes#88.
* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Rename into...
* src/ltlvisit/print.cc, src/ltlvisit/print.hh: ... those, and make
the changes listed above.
* doc/org/tut01.org, src/bin/common_output.cc,
src/bin/common_trans.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/randltl.cc, src/ltlparse/ltlparse.yy,
src/ltlvisit/Makefile.am, src/ltlvisit/mark.cc,
src/ltlvisit/relabel.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/snf.cc, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
src/taalgos/tgba2ta.cc, src/tests/equalsf.cc, src/tests/ltl2tgba.cc,
src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/reduc.cc,
src/tests/syntimpl.cc, src/tests/tostring.cc, src/twa/bdddict.cc,
src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
src/twa/twagraph.cc, src/twaalgos/compsusp.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/neverclaim.cc, src/twaalgos/remprop.cc,
src/twaalgos/stats.cc, wrap/python/ajax/spot.in, wrap/python/spot.py,
wrap/python/spot_impl.i: Adjust.
* src/bin/common_trans.cc: Skip leading directories, and
do not require that the prefix is followed by space of 0.
* src/tests/ltldo.test: Add a test.
* doc/org/ltlcross.org: Update.
This is particularly important for src/tests/satmin.test, where ltl2tgba
might be killed while writing a huge temporary file used for SAT-based
minimization. Before this patch, the temporary files would remain in
src/tests/satmin.dir/, easily overflowing the 100GB limit of the docker
containers we use on the build farm.
* src/bin/common_setup.cc: Catch termination signals for all tools,
even those that do not yet clear temporary files.
* configure.ac: Check for sigaction.
This way -S means --state-based-acc like with other tools
producing automata. This fixes#82.
* src/bin/randaut.cc: Rename -S as -Q, rename --state-acc as
--state-based-acc (with --sbacc as a synonym), and declare -S as the
short version of --state-based-acc.
* doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org,
src/tests/isomorph.test, src/tests/randaut.test,
src/tests/randtgba.test, src/tests/readsave.test, src/tests/uniq.test,
wrap/python/tests/randaut.ipynb: Adjust all calls to randaut.
* src/bin/randaut.cc: Replace the --acc-type and --acc-sets
options by a more general --acceptance option, that take either
an acceptance formula, or an acceptance name parametred by ranges.
Also accept a range for the number of atomic propositions.
* src/twaalgos/randomgraph.cc (random_acceptance): Move...
* src/twa/acc.cc, src/twa/acc.hh (random): ... here.
(parse_acc_code): Generalize to accept ranges instead of
numbers whenever sensible, and accept a 'random' acceptance.
* src/tests/randaut.test: Adjust tests and add more.
* wrap/python/tests/randaut.ipynb: Adjust call to randaut.
* doc/org/satmin.org: Document the new DTωA-minimization procedure.
* doc/org/tools.org: Fix link.
* src/bin/autfilt.cc: Pass -S to sat_minimize().
* src/twa/twagraph.hh: (state_acc_sets) New method.
* src/twaalgos/dotty.cc: Use it to correctly display co-Büchi automata.
* src/twaalgos/dtbasat.cc: Set the deterministic property on the result.
* src/twaalgos/dtgbasat.cc: Likewise, and preprocess the input automaton
in sat_minimize().
* src/twaalgos/dtgbasat.hh: Fix documentation, and take the state-based
information as an argument.
* src/twaalgos/postproc.cc: Do not call simulation-based reduction
on non-separated acceptances.
* src/tests/satmin2.test: Use -S rather than 'state-based'.
* NEWS: Update.
This is still missing tests.
* src/bin/autfilt.cc: Add a --sat-minimize option.
* src/misc/optionmap.cc, src/misc/optionmap.hh: Allow passing strings.
* src/twa/acc.cc, src/twa/acc.hh: Add helper functions needed
by the SAT-encoder.
* src/twaalgos/complete.hh: Typos.
* src/twaalgos/dtbasat.hh: Adjust comment.
* src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Generalize
to take the target acceptance as input.
* src/twaalgos/postproc.cc, src/tests/ltl2tgba.cc: Adjust calls.
* src/twaalgos/sbacc.cc, src/twaalgos/sbacc.hh: Don't pass
the pointer by reference.
* src/tests/acc.cc, src/tests/acc.test: More tests
for the acceptance helper function.
and make it easier to extend and use.
* src/twaalgos/postproc.hh, src/twaalgos/translate.cc,
src/twaalgos/translate.hh: Incorporate the Unambiguous option
with the other preferences. It's cleaner this way, and the
previous setup did not work well with Python.
* src/bin/ltl2tgba.cc: Adjust to this change.
* wrap/python/spot.py (translate): Rewrite.
* wrap/python/tests/automata.ipynb: Adjust existing cases, and
add more as well as some comments.
Producing state-based acceptance is now part of the postprocessing
routines. That means we can more easily simplify automata with
state-based acceptance (using autfilt -S --small --high, for instance)
and as as side-effect, ltl2tgba can produce GBA. However the result of
ltl2tgba -S is often larger than that of ltl2tgba -B.
* src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Implement
the SBAcc option.
* src/bin/common_post.cc, src/bin/common_post.hh: Implement -S.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltldo.cc: Adjust.
* src/tests/sim3.test: Augment test case.
* NEWS, doc/org/ltl2tgba.org, doc/org/autfilt.org: Document it -S.
* doc/org/.dir-locals.el, doc/org/init.el.in: Use 'B' instead of 'b' for
default Dot output.
* doc/org/oaut.org: Adjust.
* NEWS, doc/org/ltl2tgba.org: Document -U.
* src/bin/common_post.cc, src/bin/ltl2tgba.cc: Fix location of help text
for -U.
* src/bin/common_aoutput.cc: Add --check=unambiguous.
* src/twa/twa.hh: New unambiguous property.
* src/twaalgos/hoa.cc: Print it.
* src/twaalgos/ltl2tgba_fm.cc: Set it.
* src/twaalgos/isunamb.cc, src/twaalgos/isunamb.hh
(check_unambiguous): New function.
* src/tests/unambig.test: More tests.
* src/twaalgos/isunamb.hh, src/twaalgos/isunamb.cc: New files.
* src/twaalgos/Makefile.am: Add them.
* src/tests/unambig.test: New file.
* src/tests/Makefile.am: Add it.
* src/bin/ltlcross.cc: Record whether each produced automaton is
ambiguous.
* src/bin/autfilt.cc: Add a --is-unambiguous option.
* NEWS: Mention it.
* src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/ltl2tgba_fm.cc: Implement
generation of unambiguous automata.
* src/tests/ltl2tgba.cc: Add option -fu to test it.
* src/bin/common_post.cc: Adjust the group of options so we can easily
add more from ltl2tgba.cc.
* src/bin/ltl2tgba.cc: Add support for -U and --unambigous.
* src/twaalgos/translate.cc, src/twaalgos/translate.hh: Add support
for Unambiguous.
* src/tests/ltlcross.test, src/tests/ltlcross2.test: Test both
bin/ltl2tgba and tgbatest/ltl2tgba.
* NEWS: Mention the change.
This currently only allows extra check for stutter invariance.
* src/bin/common_aoutput.cc: Add check option,
and test stutter invariance.
* src/twaalgos/stutter.cc, src/twaalgos/stutter.hh
(check_stutter_invariance): New function.
* src/tests/stutter-tgba.test: Test it.
* src/twaalgos/dotty.cc: Add an option (e) to force elliptic shape, and
a heuristic to choose between circle and ellipse by default.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document 'e'.
* src/taalgos/dotty.cc: Ignore 'e'.
* wrap/python/spot.py (setup): Do not force circular states. The
default should be fine.
* src/tests/det.test, src/tests/dstar.test, src/tests/monitor.test,
src/tests/neverclaimread.test, src/tests/readsave.test,
src/tests/sccdot.test, src/tests/tgbagraph.test: Adjust expected
results.
* NEWS: Adjust.
* src/twaalgos/dotty.cc: Add option 'B'.
* src/taalgos/dotty.cc: Ignore it.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it.
* wrap/python/spot.py (setup): Use it by default, and rewrite
the function to be a bit more flexible.
* wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb,
wrap/python/tests/piperead.ipynb, wrap/python/tests/randaut.ipynb,
wrap/python/tests/testingaut.ipynb: Use setup() everywhere.
Now that we support any type of omega-accetpance, not just "Generalized
Büchi", it is time to move away from GB and replace it by "ω", written
just w in ASCII.
This just change the name of the tgba class. This part has to be done
by hand because the word "tgba" occurs in many contexts and a mass
replacement would be wrong.
This will be followed by some automatic renaming of all the derived
types and more.
* src/bin/autfilt.cc, src/bin/randaut.cc, src/kripke/fairkripke.hh,
src/ta/tgta.cc, src/ta/tgta.hh, src/tgba/fwd.hh, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbagraph.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/are_isomorphic.cc, src/tgbaalgos/cleanacc.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/dupexp.hh, src/tgbaalgos/hoa.cc,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stutter.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.py,
wrap/python/spot_impl.i: Rename the tgba class into twa.
* src/bin/ltlfilt.cc: Implement it.
* src/bin/common_output.cc, src/bin/common_output.hh: export the
stream_formula function.
* src/ltltest/ltlfilt.test: Test it.
* src/ltlvisit/relabel.hh: Make it possible to clear the
relabeling map.
* NEWS, doc/org/ltlfilt.org: Mention --define.
Add these two options as an answer to comments in
https://github.com/adl/hoaf/issues/39
* src/bin/autfilt.cc: Add those options. Also
make --keep-state use --remove-unreachable-states
instead of the less efficient --remove-dead-states
by default.
* src/tgbatest/readsave.test: Test them.
* src/tgbaalgos/dotty.cc: Add option 'o'.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it.
* src/taalgos/dotty.cc: Ignore this option.
* src/tgbatest/readsave.test: Test it.
Fixes#72.
* src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add
a Generic output type, and call to_generalized_buchi() if
this type is not selected.
* src/tgbatest/remfin.test: Add some tests.
* src/bin/autfilt.cc: Add a --generic option, and set it
by default.
* 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.
