* doc/org/index.org, doc/org/tut.org: New files.
* doc/Makefile.am: Add them.
* doc/org/setup.org: Adjust HOME link.
* doc/org/tools.org: Adjust UP link.
* debian/spot-doc.doc-base: The root is now index.html.
This addresses one item in #14.
* doc/org/tut10.org: New file.
* doc/Makefile.am: Add it.
* src/twaalgos/translate.hh: Fix inclusion of types from
postprocessor.
* wrap/python/spot.py (translate): Fix typo in doc string.
This fixes#61, and addresses one item of #14.
* src/ltlvisit/relabel.hh: Use a map rather than a unordered_map,
because the Swig binding for unordered_map do not seem functional.
* wrap/python/spot_impl.i: Adjust.
* wrap/python/tests/relabel.py: New file.
* wrap/python/tests/Makefile.am: Add it.
* doc/org/tut02.org: New file.
* doc/Makefile.am: Add it.
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.
The difficulty is not the example, but setting up org-mode to allow
Python and C++ example that use the local libraries, not those
installed system-wide.
* doc/org/.dir-locals.el: Rename as...
* doc/org/.dir-locals.el.in: ... this, so we can easily define
PYTHONPATH and other environment variables.
* doc/org/init.el.in: Enable C++, and make sure but Python
and C++ use the local libraries.
* doc/org/g++wrap.in, doc/org/tut01.org: New files.
* doc/Makefile.am, configure.ac: Adjust.
* wrap/python/spot.py (to_str): Take a parenth argument.
* 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 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.
* 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.
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.
* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh
(determine_unknown_acceptance): New function to call explicitly
in case one want to know whether the accepting/rejecting status
of all SCCs regardless of the acceptance.
* src/twaalgos/dotty.cc src/twaalgos/sccfilter.cc,
src/twaalgos/sccfilter.hh: Use it.
* src/tests/unambig.test, src/tests/sccdot.test: Add more tests.
* doc/org/oaut.org: Adjust doc for --dot=s, orange is not output
anymore.
* 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/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.
It makes more sense to assume that the removed set cannot be visited.
* src/tgbaalgos/mask.cc: Flip a Boolean.
* src/tgbatest/maskacc.test: Adjust test case.
* doc/org/autfilt.org: Add an example.
* src/tgba/tgbagraph.cc (purge_dead_states): Using a DFS to compute a
topological order, allowing to remove useless using a second
pass (instead of iterating the passes until there is nothing to remove).
* src/tgbaalgos/remfin.cc: Call purge_dead_states().
* src/tgbatest/remfin.test, src/tgbatest/det.test: Adjust expected
output.
* doc/org/autfilt.org: Update example.
Fixes#62.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Add call to
prop_state_based_acc() when building an automaton with state-based
acceptance.
* src/tgbatest/satmin2.test: New test.
* doc/org/satmin.org: Update.
This implement several new options for --dot in order to
allow emptiness sets to be output as colored ⓿ or ❶...
Also add a SPOT_DOTDEFAULT environment variable.
* NEWS, src/bin/man/spot-x.x, src/bin/common_aoutput.cc,
src/bin/dstar2tgba.cc: Document the new options.
* doc/org/.dir-locals.el, doc/org/init.el.in: Setup
SPOT_DOTEXTRA and SPOT_DOTDEFAULT for all documents.
* doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/satmin.org: Adjust to this new setup.
* src/misc/escape.cc, src/misc/escape.hh (escape_html): New function.
* src/tgba/acc.cc, src/tgba/acc.hh (to_text, to_html): New method.
* src/tgbaalgos/dotty.cc: Implement the new options.
* src/tgbatest/readsave.test, wrap/python/tests/automata.ipynb: More
tests.
* wrap/python/spot.py: Make sure the default argument for
dotty_reachable is None, so that SPOT_DOTDEFAULT is honored.
Because scc_info does not perform a full emptiness check, it is not
always able to tell whether an SCC is accepting if the acceptance
condition use Fin primitives. This introduce is_rejecting_scc() in
addition to to is_accepting_scc(). Only one of them may be true, but
they can both be false if scc_info has no idea whether the SCC is
accepting.
* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
is_rejecting_scc().
* src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc,
src/tgbaalgos/sccfilter.cc: Use it.
* src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc()
to color SCCs.
* doc/org/oaut.org: Document the colors used.
* src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust
tests.
* src/tgbatest/sccdot.test: New test case.
* src/tgbatest/Makefile.am: Add it.
Fixes#56.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/dstar2tgba.cc: Implement it.
* src/bin/autfilt.cc, src/bin/ltl2tgba.cc, src/bin/ltldo.cc,
src/bin/randaut.cc: Fix main() to catch exceptions from the
constructor of the automaton printer as well.
* src/tgbatest/randaut.test: Add a test case.
* doc/org/oaut.org: Document it.
Also get rid of the lbt_parser, and fix the LBT support of the HOA
parser.
* doc/org/ltlcross.org, doc/org/ltldo.org: Update.
* src/bin/common_trans.cc, src/bin/common_trans.hh: Add support for
%O, and keep %T,%N,%H as hidden aliases without disabling them.
* src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tgbatest/ltl2tgba.cc:
Call hoa_parse instead of lbt_parse.
* src/hoaparse/hoaparse.yy: Improve error reporting from LBT.
* src/hoaparse/hoascan.ll: Fix typos preventing parsing of
LBT files with more than 10 states.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: Delete the lbt
parser.
* src/tgbatest/lbttparse.test: Adjust the expected error message.
* NEWS: Update.
Get rid of the output in Spot's format.
This finally fixes#1.
* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh: Delete.
* src/tgbaalgos/Makefile.am: Adjust.
* src/ltlvisit/contain.cc: Remove useless includes.
* src/bin/dstar2tgba.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh: Remove the "Spot" output.
* doc/org/dstar2tgba.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/oaut.org: Update doc.
* NEWS: Mention that Spot i/o is gone.
* src/tgbatest/randtgba.cc: Output in HOA.
* src/tgbatest/randtgba.test: Use randaut instead of
randtgba.
* wrap/python/spot.i: Do not provide binding for save.hh
* src/bin/common_trans.cc, src/bin/common_trans.hh: New files,
extracted from...
* src/bin/ltlcross.cc: ... here, so that ltldo can use them.
* src/bin/ltldo.cc: New file.
* src/bin/Makefile.am: Adjust.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Make
it possible to add new statistics.
* doc/org/ltldo.org: New file.
* doc/Makefile.am, doc/org/tools.org: Adjust.
* src/bin/man/ltldo.x: New file.
* src/bin/man/Makefile.am: Adjust.
* src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x: Mention ltldo(1).
* src/tgbatest/ltldo.test, src/tgbatest/ltldo2.test: New files.
* src/tgbatest/Makefile.am: Add them.
* NEWS: Mention ltldo.
