Commit 7619a5a0 by Alexandre Duret-Lutz

### simplify: remove an incorect SERE simplification

* 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.
parent 2731c9be
 ... ... @@ -6,6 +6,10 @@ New in spot 1.2.5a (not yet released) * Bug fixes: - Remove one incorrect simplification rule for PSL discovered via checks on random formulaes. (The bug was very unlikely to trigger on non-random formulas, because it requires a SERE with an entire subexpression that is unsatisfiable.) - When the automaton resulting from the translation of a positive formula is deterministic, ltlcross will compute its complement to perform additional checks against other translations of the ... ...
 ... ... @@ -1570,8 +1570,9 @@ Here are basic the rewritings for the weak closure and its negation: \nsere{r_1;r_2}&\equiv \nsere{r_1}\AND\nsere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2\\ \sere{b;r}&\equiV b\AND\X\sere{r}& \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\ \sere{b\STAR{};r}&\equiv b\W\sere{r}& \nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\ % These two would be correct only if $r$ is satisfiable. % \sere{b\STAR{};r}&\equiv b\W\sere{r}& % \nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\ \sere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{b\AND \X(b\ldots}_{\mathclap{i\text{~occurences of~}b}}\AND\X\sere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r})& \nsere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\ldots}_{\mathclap{i\text{~occurences of~}\NOT b}}\OR\X\nsere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r}) \\ \sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}& ... ...
 #! /bin/sh # Copyright (C) 2013 Laboratoire de Recherche et # Copyright (C) 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. ... ... @@ -24,3 +24,9 @@ set -e run 0 ../reduc 0 'XFa & FXa' 'XFa' run 0 ../reduc 0 '(Xf W 0) | X(f W 0)' 'XGf' # Two incorrect reductions. Those used # to reduce respectively to a W (b && !b) and !a M (b || !b). # But both are wrong. The reduction {a*;r} = a W r seems only # valid if r has a non-empty language. run 0 ../reduc 0 '{a[*];{b && !b}}' run 0 ../reduc 0 '!{a[*];{b && !b}}'
 ... ... @@ -355,14 +355,14 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)' run 0$x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \ '{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))' run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))' run 0$x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})' run 0 $x '{a;b[*];c[*];e;f*}' 'a & X({b*;c*;e})' run 0$x '{a;b*;(a* && (b;c));c*}' 'a & X({b*;(a* && (b;c))})' run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))' run 0$x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))' run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))' run 0$x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})' run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)' run 0$x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)' run 0 $x '!{a;c[*];e;f*}' '!a | X!{c[*];e}' run 0$x '!{a;b*;(a* && (b;c));c*}' '!a | X(!{b*;(a* && (b;c))})' run 0 $x '{(a;c*;d)|(b;c)}' '(a & X{c*;d}) | (b & Xc)' run 0$x '!{(a;c*;d)|(b;c)}' '(X(!{c*;d}) | !a) & (X!c | !b)' run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc' run 0$x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v' run 0 \$x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v' ... ...
 ... ... @@ -1621,10 +1621,10 @@ namespace spot // Some term does not accept the empty word. unsigned end = mo->size() - 1; // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂})) // !{b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // = !b₁|X(!b₂|X(!b₃ M !{e₁;f₁;e₂;f₂})) // {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // = b₁&X(b₂&X({e₁;f₁;e₂;f₂})) // !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂})) // if e denotes a term that accepts [*0] // and b denotes a Boolean formula. while (mo->nth(end)->accepts_eword()) ... ... @@ -1633,9 +1633,7 @@ namespace spot while (start <= end) { const formula* r = mo->nth(start); const bunop* es = is_KleenStar(r); if ((r->is_boolean() && !opt_.reduce_size_strictly) || (es && es->child()->is_boolean())) if (r->is_boolean() && !opt_.reduce_size_strictly) ++start; else break; ... ... @@ -1681,21 +1679,6 @@ namespace spot tail = multop::instance(multop::And, e, tail); } // {b*;f} = b W {f} // !{b*;f} = !b M !{f} else { const bunop* es = is_KleenStar(e); assert(es); const formula* c = es->child()->clone(); if (doneg) tail = binop::instance(binop::M, unop::instance(unop::Not, c), tail); else tail = binop::instance(binop::W, c, tail); } } mo->destroy(); result_ = recurse_destroy(tail); ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!