* src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent
optional parameter, like for the to_string() function.
* src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the
handling of full_parent.
(to_spin_string_visitor): Handle full_parent.
reduce_visitor::visit(binop).
* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_):
Move this method...
(recurse_eu): ... outside as a separate function. Likewise for
the universal/eventual result struct.
(reduce_visitor::visit(binop)): Call recurse_eu() once to replace
two calls to is_eventual and is_universal, thus replacing two
recursions by one.
* src/ltlvisit/syntimpl.cc (eventual_universal_visitor): Use
a union to store the eventual and universal properties as two
bit in a bit-field, and "AND" both of them at once.
(eventual_universal_visitor::recurse_un,
eventual_universal_visitor::recurse_ev): Replace these
two functions by ...
(eventual_universal_visitor::recurse_): ... this one, that
returns both bits as an unsigned.
* src/tgbatest/ltl2tgba.cc (main): Either replay the accepting
run or print it, but do not do both.
* src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR
when we expect the run to be displayed.
* src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A
variable (the upcoming GCC 4.6 would warn about it) and set opt_ec
to 1 if -A is used without -e.
* src/tgbaalgos/reducerun.hh (tgba_run): Predeclare as a struct
since this is what it is.
* src/tgbatest/randtgba.cc (main): Avoid using "i" with two
different type in the same loop.
* src/kripke/fairkripke.hh, src/kripke/fairkripke.cc,
* src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and
document the Kripke interface. I have tested it by updating
checkpn to use it.
before some optional operations (like more optimizations, or a
product).
* src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last
automaton computed, not just the automaton when we degeneralized
it. We may have applied other algorithms since the original
degeneralization.
options -C and -CR for that.
* src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
whether we want the accepting run to be printed or replayed.
* src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
ltl2ba.
* src/neverparse/neverclaimparse.yy: Accept multiple labels
for the same state. Honor accepting states. Forward parse
error from the parser used for guards. Accept "false" as a
single instruction for a state.
* src/neverparse/neverclaimscan.ll: Recognize "false" specifically,
and remove the ";" hack.
* src/tgba/tgbaexplicit.cc
(tgba_explicit_string::~tgba_explicit_string): Adjust not to
destroy a state twice.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_string::add_state_alias): New function.
* src/tgbatest/defs.in (SPIN, LTL2BA): New variables.
* src/tgbatest/neverclaimread.test: Check error messages for
syntax errors in guards. Make sure we can read the output
of `spin -f' and `ltl2ba -f' on a few test formulae.
* src/neverclaimparse/: New directory.
* src/neverclaimparse/fmterror.cc: New file. Print a formatted parse
error on a output stream.
* src/neverclaimparse/neverclaimparse.yy: New file. Parser declaration
for Bison.
* src/neverclaimparse/neverclaimscan.ll: New file. Scanner declaration
for Flex.
* src/neverclaimparse/public.hh: New file. Public header for external
use.
* src/neverclaimparse/parsedecl.hh: New file. Header file for
Flex-Bison interaction.
* src/neverclaimparse/Makefile.am: New Makefile.
* src/tgbatest/neverclaimread.cc: New file. Test program for the
never claim parser.
* src/tgbatest/neverclaimread.test: New file. Test script for the
never claim parser.
* src/tgbatest/Makefile.am: Adjust.
* configure.ac : Adjust.
* README: Adjust.
* src/tgbaparse/tgbaparse.yy (line): Fix computation of line number
for error messages when parsing conditions.
* src/tgbatest/readsave.test: Check the syntax position of syntax errors
in the diagnostics. Use ltl2tgba instead of readsave.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove readsave.
We do that because the declaration of this type, which is local to
src/tgba/tgbasafracomplement.cc has a member in an anonymous
namespace, and some versions of g++-4.2 issue a very annoying
warning about this legitimate code. See Bug 29365 on GCC's
Bugzilla. Report by Silien Hong <silien.hong@lip6.fr>.
* src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not
forward declare.
(tgba_safra_complement): Use void* instead of
safra_tree_automaton*.
* src/tgba/tgbasafracomplement.cc: static_cast void* to
safra_tree_automaton* anywhere needed.
* src/neverclaimparse/: New directory.
* src/neverclaimparse/fmterror.cc: New file. Print a formatted parse
error on a output stream.
* src/neverclaimparse/neverclaimparse.yy: New file. Parser declaration
for Bison.
* src/neverclaimparse/neverclaimscan.ll: New file. Scanner declaration
for Flex.
* src/neverclaimparse/public.hh: New file. Public header for external
use.
* src/neverclaimparse/parsedecl.hh: New file. Header file for
Flex-Bison interaction.
* src/neverclaimparse/Makefile.am: New Makefile.
* src/tgbatest/neverclaimread.cc: New file. Test program for the
never claim parser.
* src/tgbatest/neverclaimread.test: New file. Test script for the
never claim parser.
* src/tgbatest/Makefile.am: Adjust.
* configure.ac : Adjust.
* README: Adjust.
clone for M.
* src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove
the stronger rules for R and M. They were wrong.
* src/ltltest/reduccmp.test: Test a simpple counterexample.
* src/ltlvisit/reduce.cc (reduce_visitor): Add the following
implication rewriting rules:
a M (b M c) = a M c if a implies b.
a M (b R c) = a M c if a implies b.
a R (b R c) = a R c if a implies b.
a R (b M c) = b M c if b implies a.
a M (b M c) = b M c if b implies a.
The latter rule was fixed from an incorrectly copied&pasted
rule for a M (b R c) = b R c if b implies a (this is wrong).
* src/ltltest/reduccmp.test: Add more tests.
* src/ltlvisit/basicreduce.cc: Perform the following reductions:
(a R b) | Gb = a R b
(a M b) | Gb = a R b
(a U b) & Fb = a U b
(a W b) & Fb = a U b
* src/ltltest/reduccmp.test: Test them.
* src/ltlvisit/basicreduce.cc: Perform the following reductions:
(a U b) & (c W b) = (a & c) U b
(a W b) & (c W b) = (a & c) W b
(a R b) | (c M b) = (a | c) R b
(a M b) | (c M b) = (a | c) M b
* src/ltltest/reduccmp.test: Test them.
* src/ltlvisit/basicreduce.cc: Perform the following reductions.
a R (b & F(a)) = a M b
a M (b & F(a)) = a M b
a R Fa = Fa
a M Fa = Fa
a R b & Fa = a M b
a R b & a M c = a M (b & c)
a M b & a M c = a M (b & c)
* src/ltltest/reduccmp.test: More tests.
* src/ltlvisit/basicreduce.cc: Perform the following reductions.
a U (b | Ga) = a W b
a W (b | Ga) = a W b
a U b | Ga = a W b
a U b | a W c = a W (b | c)
a W b | a W c = a W (b | c)
a U Ga = Ga
a W Ga = Ga
* src/ltltest/reduccmp.test: More tests.
