Commit graph

7 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
cf91a23711 tests: add some missing "set -e"
* src/ltltest/lbt.test, src/ltltest/utf8.test,
src/tgbatest/dbacomp.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, src/tgbatest/ltlcrossce.test: Add set -e.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
1ab46b0864 postproc: Add option to output Complete automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Tweak set_pref()
to also accept Any|Complete, Small|Complete, or Deterministic|Complete.
* src/bin/common_post.hh, src/bin/common_post.cc: Add option --complete
and set comp.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Pass
comp to set_pref().
* src/tgbaalgos/complete.cc: Preserve state-based acceptance.
* src/tgbatest/dstar.test, src/tgbatest/ltlcross2.test,
src/tgbatest/nondet.test: Augment tests.
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, NEWS: Document.
2013-09-08 20:43:52 +02:00
Alexandre Duret-Lutz
9b82d7557c ltlcross: add a --products=N option
* src/bin/ltlcross.cc: Implement the new option.  Average the product
statistics on all products.
* src/tgbatest/basimul.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, bench/ltl2tgba/tools: Use the new option.
* NEWS: Mention it.
2013-05-12 21:22:46 +02:00
Alexandre Duret-Lutz
eed7e2df8f lbtt: improve the LBTT output
Provide a way to output automata with state-based acceptance.  Also
print the guards using to_lbt_string() for consistency: as a
consequence, atomic proposition that do not match p[0-9]+ are now
double-quoted.

* src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
* src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
* src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
* src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
Add an option --lbtt=t to get the old behavior.
* src/bin/man/ltl2tgba.x: Document the LBTT format we use with
some links and examples.
* src/tgbatest/lbttparse.test: More tests.
* src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
* NEWS: Update.
2013-05-09 21:55:37 +02:00
Alexandre Duret-Lutz
b6d4806dca translate: use compositional suspension on request
This has to be turned on using "-x comp-susp" and other
related options documented in spot-x (7).

* src/tgbaalgos/translate.hh, src/tgbaalgos/translate.cc:
Add support for calling composition-suspension, with
optional simulation, WDBA-minimization, and composition.
* src/bin/spot-x.cc: Document the new options.
* src/bin/man/spot-x.x: Add some bibliography.
* src/tgbatest/ltlcross2.test: Test it.
2013-04-27 10:52:49 +02:00
Alexandre Duret-Lutz
3f61a34bd1 * src/tgbatest/ltlcross2.test: Fix list of tested configurations. 2013-01-22 11:55:03 +01:00
Alexandre Duret-Lutz
f3ef9de0be rename ltlcheck as ltlcross
* src/bin/ltlcheck.cc, src/bin/man/ltlcheck.x,
src/tgbatest/ltlcheck.test, src/tgbatest/ltlcheck2.test: Rename as ...
* src/bin/ltlcross.cc, src/bin/man/ltlcross.x,
src/tgbatest/ltlcross.test, src/tgbatest/ltlcross2.test: ... these.
* NEWS, src/bin/Makefile.am, src/bin/man/Makefile.am,
src/tgbatest/Makefile.am: Adjust.
2012-10-21 13:23:02 +02:00
Renamed from src/tgbatest/ltlcheck2.test (Browse further)