GitLab

* src/ltltest/reduccmp.test: Reorder the test added by the
previous patches.  Some are not supposed to be reduced by
reductaustr.

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/syntimpl.cc (syntactic_implication): Do not
create visitors if arguments are constant.

* src/ltlvisit/simpfg.cc: Typo.
* src/ltltest/reduccmp.test: Add more tests.

help output.

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

* src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
these new operators.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
* src/ltltest/reduccmp.test: Add new tests for W and M.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Add support for W and M.
* src/tgbatest/ltl2neverclaim.test: Test never claim output
using LBTT, this is more thorough.  Also we cannot use -N
any more in the spotlbtt.test.
* src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
* src/tgbatest/ltl2neverclaim.test: Test W and M, and use
-DS instead of -N, because lbtt-translate does not want
to translate these operators for tools that masquerade as Spin.

appropriate.

* wrap/python/spot.i (spot::scc_filter): Make it available.
* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
Use the "full" option unless the show_degen_png or
show_never_claim are set.  Also reduce_scc the default.

* src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy,
src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use
token types for %destructor and %printer.  Remove the yylex hack,
since %name-prefix is now honored by Bison.  Also remove the
useless <token> type.  Suggested by Akim Demaille.

* src/ltlparse/fmterror.cc (format_parse_errors): Count columns
starting at 1.  Older Bison used to start at 0 but changed to
match the GNU Coding Standards.
* src/ltltest/parseerr.test: Add a test case.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse):
Disable this rule unconditionally.
* src/ltltest/reduccmp.test: Adjust tests.

degeneralization.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the
list of acceptance condition in the reverse order.  The order is
still arbitrary, but the bdd_satone() call seems to output the
acceptance conditions that are more used first, and this helps the
degeneralization process.

* src/ltlparse/ltlparse.yy: Change the precedence of "->" and
"<->" so that "a & b -> c" is interpreted as "(a & b) -> c"
instead of "a & (b -> c)".  The new interpretation is more
intuitive, and matches that of LBTT.

original paper by Somenzi and Bloem.  Reported by Ruediger Ehlers.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Do not
forget to free the initial state after usage.

by default in scc_filter().

Doing so helps the degeneralization algorithm, because it will
have more opportunity to be in an accepting level when it reaches
the accepting SCCs.

* src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
remove_all_useless argument.
(filter_iter::process_link): Use the flag to decide whether to
filter acceptance conditions going to accepting SCCs.
(scc_filter): Take a remove_all_useless argument and pass it to
filter_iter.
* src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
and document the function.
* src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
for remove_all_useless=false and add -R3f for
remove_all_useless=true.
* src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
the degeneralization worse than -R3.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace
the FG(a)|FG(b) == FG(a|b) rule by the above more generic one.
Add the dual rule for G(a)&G(b), as we had none (this one won't
improve anything in the translation, but it is more symmetric
this way).  Also simplify some pointer checks.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set
cycle_start_ to start in the accepting layer of the degeneralized
automaton if the initial state has an accepting self-loop.
Otherwise, starts at the level of the first acceptance condition
as previously.
(tgba_sba_proxy::get_init_state): Use cycle_start_.
* src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so
that we can use it in tgba_sba_proxy::tgba_sba_proxy.
(tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state):
Declare.
* src/tgbatest/ltl2tgba.test: More tests.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move
the optimization step added by the previous patch outside the
before the bddtrue check, so that it also applies to accepting
states in SBA.

an acceptance condition on all outgoing transitions.

This was motivated by experiments from Rüdiger Ehlers, showing
that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
U (b U c)'".  With this change and the previous one, it is no
longer the case.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
a pointer to the source automaton and...
(tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
optimization step to gather the acceptance conditions common
to all outgoing transitions of the destination state, and pretend
they are on the current (ingoing) transition.
(tgba_tba_proxy::succ_iter): Pass the
source automaton to the constructed iterator.
* src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
* src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.

* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions.  I realized this while looking at experiments from
Rüdiger Ehlers.

* src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi
is the BibTex entry used as comment, because some version of sed
will choke on non-ascii character and cause sanity/style.test to
fail.

This is actually the third time I fix random_graph().  On
2007-02-06 I changed the function not to generated dead states,
but in a way that made it non-deterministic.  On 2010-01-20 I made
the function deterministic again, but it started to generate dead
states as a side effect.  This time, I'm making sure that dead
states won't come again with a test-case that we should have had
from the beginning.

* src/tgbaalgos/randomgraph.cc (random_graph): Add an extra
indirection array, state_randomizer[], so that we can reorder
states indices after a random selection without actually changing
the value of the indices used by unreachable_states and
nodes_to_process.
* src/tgbatest/randtgba.test: New file.
* src/tgbatest/Makefile.am: Add randtgba.test.

* wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by
configure.
(os.system): Cleanup stale files only when the form has been
submitted.
(list options): Keep track of the selected value.
(draw_acc_run|print_acc_run): set ec=0 to detect if it has been
later set or not.  Fix error message when using generalized
automata with degeneralized emptiness checks.
* wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@.

* wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new.
(svg_output, reduce_langcout): Add these new options.
(render_dot): Support svg_output.

* NEWS, configure.in: Bump version to 0.5.