- 04 Jan, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* src/bin/ltl2tgba.cc, src/bin/randaut.cc: Catch exceptions in main loop. * src/tgbatest/ltl2tgba.test, src/tgbatest/randaut.test: Test errors with unknown --dot argument.
-
- 03 Jan, 2015 19 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/dotty.cc: Add option 's' to display SCCs. * src/bin/dstar2tgba.cc, src/bin/common_aoutput.cc: Document it. * src/tgbatest/neverclaimread.test: Test it.
-
Alexandre Duret-Lutz authored
destroy_atomic_prop_set() takes a parameter named 'as', and aparently Swig reuses this name as-is, although it is a Python keyword. * src/ltlvisit/apcollect.hh (destroy_atomic_prop_set): Rename the parameter to please Swig on Arch Linux.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/common_aoutput.hh, src/bin/common_aoutput.cc: Adjust to support three kind of statistics printer, depending on whether the tool input formulas, automata, or nothing. * src/bin/randaut.cc, src/bin/autfilt.cc: Adjust. * src/bin/ltl2tgba.cc: Use the common_aoutput printers. The --csv-escape option disappeared along the way, but it was not honored anyway...
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Move output options handling... * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh:... here. * src/bin/randaut.cc: Use them. * src/tgbatest/randaut.test: Test --name and --stats for randaut.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/ltlgrind.cc: Adjust help text to match other tools.
-
Alexandre Duret-Lutz authored
for consistency with autfilt, randaut, and dstar2tgba * src/bin/ltl2tgba.cc: Here.
-
Alexandre Duret-Lutz authored
for consistency with ltlfilt * src/bin/autfilt.cc, src/bin/randaut.cc: Here.
-
Alexandre Duret-Lutz authored
* src/bin/options.py: New file. * src/bin/Makefile.am: Distribute it. * src/bin/README: New file.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Also accept '-u' for '--uniq'. * src/bin/randaut.cc: Likewise, plus fix the unicity check. * src/tgbatest/uniq.test: Really test it.
-
Alexandre Duret-Lutz authored
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: New files... * src/bin/autfilt.cc: ... extracted from here. * src/bin/Makefile.am: Add them.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/tgba/tgba.hh: Declare a prop_set to specify the types. * src/tgba/tgbagraph.hh: Use prop_set for all copy constructors. * iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc, src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc, src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc, src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/dotty.cc: Specialize for tgba_digraph_ptr. * src/tgba/tgbagraph.hh, src/tgbaalgos/dupexp.cc: Copy properties by default when cloning an automaton. * src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/ltl2tgba.test, src/tgbatest/monitor.test, src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test: Adjust tests.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Add an options parameter. * src/bin/randaut.cc, src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, wrap/python/ajax/spot.in: Use it. * src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/monitor.test, src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test, src/graphtest/tgbagraph.test: Adjust because automata are now output horizontally. * NEWS: Mention the change.
-
- 23 Dec, 2014 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 17 Dec, 2014 7 commits
-
-
Alexandre Duret-Lutz authored
-
Thibaud Michaud authored
* src/bin/autfilt.cc: add option --uniq. * src/bin/randaut.cc: add option --uniq. * src/tgbatest/uniq.test: Test it.
-
Thibaud Michaud authored
* src/bin/autfilt.cc: Use isomorphism_checker. * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh: Wrap are_isomorphic inside a class to keep the canonic version of the first automaton between two calls, and use a more efficient algorithm in case both automata are deterministic. * src/tgbatest/isomorph.test: Add tests for deterministic automata.
-
Thibaud Michaud authored
* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh, src/bin/autfilt.cc: are_isomorphic now uses canonicalize. It returns a bool, because the mapping cannot be deduced easily from the canonicalized automaton. * src/graph/graph.hh: Add equality operator to trans_storage_t for easy comparison of transition vectors. * src/tgba/tgbagraph.hh: Add equality operator to tgba_graph_trans_data and to tgba_digraph. * src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/isomorph.test: Test them.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Support %w. * src/tgbatest/readsave.test: Test it.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add these new options. * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Make it possible to call sl() and sl2() without passing the set of atomic propositions. * src/tgbatest/stutter.test: New file. * src/tgbatest/Makefile.am: Add it.
-
Alexandre Duret-Lutz authored
* src/tgba/tgbagraph.cc (merge_transition): Do it. * src/tgbatest/readsave.test: Test it. * src/bin/autfilt.cc: Fix statistics about the original automaton when using --stats or --name.
-
- 16 Dec, 2014 3 commits
-
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add these new options. * src/tgbatest/readsave.test: Test them.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Implement this new option. * src/tgbatest/readsave.test: Test it.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Here. * src/tgbaalgos/stats.cc: Do not segfault if format is nullptr. * src/tgbatest/readsave.test: Exercise --name, %M, and %m.
-
- 15 Dec, 2014 2 commits
-
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add a --count option. * src/tgbatest/randaut.test: Test autfilt's --count and --states.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add a --states=RANGE option. * src/bin/common_range.cc, src/bin/common_range.hh: Generalize range_parse to allow an optional upper bound.
-
- 11 Dec, 2014 7 commits
-
-
Alexandre Duret-Lutz authored
* src/hoaparse/hoaparse.yy: forward the error messages from lbt_parse(). * src/hoaparse/hoascan.ll: Minor cleanups. * src/tgbatest/lbttparse.test: Test it.
-
Alexandre Duret-Lutz authored
* src/ltlparse/ltlscan.ll: Skip comments. * src/ltltest/ltlfilt.test: Test this. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Here. * src/tgbatest/hoaparse.test: More tests.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add support for %L. * src/tgbatest/hoaparse.test: Test it.
-
Alexandre Duret-Lutz authored
the existing -q/--quiet option is renamed to --ignore-errors * src/bin/ltlfilt.cc: Adjust option. * src/bin/common_output.cc, src/bin/common_output.hh: Add a quiet_output. * bench/dtgbasat/prepare.sh: Rename -q to --ignore-errors.. * src/ltltest/remove_x.test: Use -q. * NEWS: Mention this change.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add option. * src/tgbatest/det.test: Test it.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/are_isomorphic.cc: inline is_isomorphism() into are_isomorphic() so that the reference vector is only sorted once, and both vectors are only allocated once.
-