GitLab

* src/bin/autfilt.cc: Support %w.
* src/tgbatest/readsave.test: Test it.

* 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.

* 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.

* src/bin/autfilt.cc: Add these new options.
* src/tgbatest/readsave.test: Test them.

* src/bin/autfilt.cc: Implement this new option.
* src/tgbatest/readsave.test: Test it.

* 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.

* src/bin/autfilt.cc: Add a --count option.
* src/tgbatest/randaut.test: Test autfilt's --count and --states.

* 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.

* src/hoaparse/hoaparse.yy: forward the error messages
from lbt_parse().
* src/hoaparse/hoascan.ll: Minor cleanups.
* src/tgbatest/lbttparse.test: Test it.

* src/ltlparse/ltlscan.ll: Skip comments.
* src/ltltest/ltlfilt.test: Test this.
* NEWS: Mention it.

* src/bin/autfilt.cc: Here.
* src/tgbatest/hoaparse.test: More tests.

* src/bin/autfilt.cc: Add support for %L.
* src/tgbatest/hoaparse.test: Test it.

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.

* src/bin/autfilt.cc: Add option.
* src/tgbatest/det.test: Test it.

* 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.

This is probably the worse grammar I wrote: the LBTT format is designed
to be scanned with scanf, and very inconvenient to parse with
bison/flex.  Here the scanner basically has to emulate a parser to
classify the different INTs as tokens with different types.

* src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules for LBTT.
* src/hoaparse/parsedecl.hh: Add a way to reset the parser between each
automata.
* src/tgbatest/hoaparse.test, src/tgbatest/lbttparse.test: Add more
tests.

* src/priv/accmap.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/ltl2tgba.cc, src/tgbatest/tgbaread.cc: Do not pass any
environment parameter to parse acceptance sets.  This is not used
anymore since we moved to int-labeled acceptance sets.

* src/tgbaalgos/are_isomorphic.cc (is_isomorphism): Do not copy
trans_storage_t elements as they contain more than what we use.
Remap the states of a1 before the sort, not during the sort.
(are_trivially_different): Also catch the case where the
number of acceptance sets are different.
* src/tgbaalgos/are_isomorphic.hh: Improve doxygen.

* src/bin/autfilt.cc: Do not use -I for --are-isomorphic.
Fix --help.
* src/tgbatest/isomorph.test: Adjust to use --are-isomorphic, and speed
it up 5-fold.

Thibaud Michaud authored Dec 09, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

* src/tgbaalgos/are_isomorphic.cc: Here.

Thibaud Michaud authored Dec 09, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

* src/bin/autfilt.cc: Here.

Thibaud Michaud authored Dec 09, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

* src/bin/autfilt.cc: Return with exit code 1 if no match found.
* src/tgbaalgos/are_isomorphic.cc,src/tgbatest/degenlskip.test
src/tgbatest/explpro2.test,src/tgbatest/explpro3.test
src/tgbatest/explpro4.test,src/tgbatest/explprod.test
src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test
src/tgbatest/tripprod.test: Use exit status to check for output
emptiness instead of 'test -n'.
* src/tgbatest/isomorph.test: Simplify test.

Thibaud Michaud authored Dec 09, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

* src/tgbatest/degenlskip.test, src/tgbatest/explpro2.test
src/tgbatest/explpro3.test, src/tgbatest/explpro4.test
src/tgbatest/explprod.test, src/tgbatest/neverclaimread.test
src/tgbatest/tripprod.test, src/tgbatest/readsave.test: Here.

Thibaud Michaud authored Dec 08, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

* src/bin/autfilt.cc: Here.
* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh:
Here.

Thibaud Michaud authored Dec 03, 2014 and Alexandre Duret-Lutz committed Dec 10, 2014

And add the corresponding --isomorphic=FILENAME option to autfilt.

* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh:
New.
* src/tgbaalgos/Makefile.am: Add it.
* src/bin/autfilt.cc: Add --isomorphic option.
* src/tgbatest/isomorph.test: Test it.
* src/tgbatest/Makefile.am: Add it.

* src/tgba/tgba.hh, src/tgba/tgba.cc (set_named_prop): Add a template
version.
(get_named_prop): Hide the old version, and supply a template version
that casts.
* src/bin/ltlcross.cc, src/hoaparse/hoaparse.yy, src/tgbaalgos/hoa.cc,
src/tgbaalgos/product.cc: Adjust usage.

* src/hoaparse/hoaparse.yy: Store the automaton name.
* src/tgbaalgos/hoa.cc: Output it if it exists.
* src/tgbatest/hoaparse.test: Adjust tests.

* src/tgbaalgos/hoa.cc: Here.

* src/bin/randaut.cc: Fix memory leak.
* src/bin/autfilt.cc: Add a --merge-transitions option.
* src/tgbatest/readsave.test: Rewrite using randaut and autfilt.

This fixes #6.

* src/graph/graph.hh: Rename the old transitions() as
transition_vector(), and implement a new transitions() that iterates
only on non-dead transitions.
* src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc, src/graph/ngraph.hh:
Adjust wrappers.
* src/hoaparse/hoaparse.yy, src/tgbaalgos/complete.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/randomize.cc, src/tgbaalgos/safety.cc: Adjust calls.

* src/bin/autfilt.cc: Implement the --product option.
* src/tgbatest/explprod.cc, src/tgbatest/tripprod.cc: Delete.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
src/tgbatest/tripprod.test: Rewrite using autfilt --product.

* iface/ltsmin/kripke.test: Fix detection of divine's ltsmin option.
* iface/ltsmin/finite.test: Likewise.  Also extra the Spins test
into...
* iface/ltsmin/finite2.test: ... this new file, so that we
can test the divine and spins interfaces independently.
* iface/ltsmin/Makefile.am: Distribute finite2.test and finite.pm.
* iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc: Adjust function names.

Thibaud Michaud authored Nov 03, 2014 and Alexandre Duret-Lutz committed Dec 07, 2014

* configure.ac, iface/Makefile.am: Adjust.
* iface/dve2/finite.test, iface/dve2/.gitignore, iface/dve2/Makefile.am,
iface/dve2/README, iface/dve2/beem-peterson.4.dve,
iface/dve2/dve2check.test, iface/dve2/defs.in, iface/dve2/finite.dve,
iface/ltsmin/finite.test, iface/dve2/kripke.test, iface/dve2/dve2.cc,
iface/dve2/dve2.hh, iface/dve2/dve2check.cc: Move to iface/ltsmin.
* iface/ltsmin/.gitignore, iface/ltsmin/Makefile.am,
iface/ltsmin/README, iface/ltsmin/beem-peterson.4.dve,
iface/ltsmin/check.test, iface/ltsmin/defs.in, iface/ltsmin/finite.dve,
iface/ltsmin/finite.test, iface/ltsmin/kripke.test,
iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc: Factorize dve2 and spins interface in
iface/ltsmin/
* iface/ltsmin/elevator2.1.pm, iface/ltsmin/finite.pm: Test promela
models.
* README: Document iface/ltsmin/ directory.

* src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh: Delete.
* src/tgbaalgos/gtec/Makefile.am: Adjust.

Conflicts:
	NEWS
	configure.ac
	src/kripketest/bad_parsing.test
	src/ltltest/reduccmp.test
	src/neverparse/neverclaimscan.ll
	src/tgba/futurecondcol.cc
	src/tgba/tgbasafracomplement.cc
	src/tgbaalgos/hoa.cc
	src/tgbaalgos/ltl2tgba_fm.cc
	src/tgbatest/neverclaimread.test
	src/tgbatest/readsave.test

* NEWS, configure.ac, doc/org/tools.org: Bump version number.

* src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Use Perl for the unix2dos conversion.

* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/reduc0.test: Add a regression test.
* src/ltltest/reduccmp.test: Adjust test cases for its removal.
* NEWS: Mention it.