alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
2682 commits 6 branches 0 tags 36 MiB
Commit graph

5 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
f412fee6f3 stutter check: cleanup and add test cases 
* src/ltltest/ltlfilt.test: Add more tests.
* src/ltltest/stutter.test: New test.
* src/ltltest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Catch std::runtime_error.
* src/tgba/tgbasl.hh (make_tgbasl): New function.
* src/tgba/tgbagraph.hh (make_tgba_graph): Add another overload.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Take the algorithm version as an
optional integer, and call getenv() only once.
* bench/stutter/stutter_invariance_randomgraph.cc,
bench/stutter/stutter_invariance_formulas.cc: Simplify using the
above functions.
 2014-11-14 11:11:39 +01:00
Alexandre Duret-Lutz
87b65b9bce relabel: implement relabeling of Boolean subexpressions. 
* src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
multop::boolean_count): New methods.
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
(relabel): Take an optional relabeling_map as parameter.
(relabel_bse): New.
* src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
* src/ltltest/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Add option --relabel-bool.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
* doc/org/ltlfilt.org: Illustrate it.
 2013-09-28 09:02:30 +02:00
Alexandre Duret-Lutz
536e45b342 Arrange multops so that Boolean arguments come first. 
This helps recursive implication checks.  Also order
atomic propositions with strverscmp().

* src/ltlast/formula.hh (formula_ptr_less_than_multop,
is_literal, atomic_prop_cmp): New.
* src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them.
* src/ltlast/multop.cc: Use formula_ptr_less_than_multop.
* src/ltltest/isop.test, src/ltltest/ltlfilt.test,
src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests.
* NEWS: Mention the new order.
 2013-09-26 17:14:58 +02:00
Alexandre Duret-Lutz
372790a489 bin: Ignore empty lines on input. 
* src/bin/common_finput.cc: Here.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
 2013-05-12 17:32:46 +02:00
Alexandre Duret-Lutz
2cab8197e5 ltlfilt: Fix handling --universal, --eventual, and --stutter-invariant. 
* src/bin/ltlfilt.cc: Handle --universal and --eventual.  Match
only LTL formulas with --stutter-invariant.
* src/ltltest/ltlfilt.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.
* NEWS: Mention these bug fixes.
 2013-05-11 11:24:38 +02:00