Commit 11568666 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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 88da1ad8
...@@ -181,6 +181,10 @@ New in spot 1.2.5a (not yet released) ...@@ -181,6 +181,10 @@ New in spot 1.2.5a (not yet released)
* Bug fixes: * 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 - When the automaton resulting from the translation of a positive
formula is deterministic, ltlcross will compute its complement formula is deterministic, ltlcross will compute its complement
to perform additional checks against other translations of the 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: ...@@ -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\\ \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}& \sere{b;r}&\equiV b\AND\X\sere{r}&
\nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\ \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\
\sere{b\STAR{};r}&\equiv b\W\sere{r}& % These two would be correct only if $r$ is satisfiable.
\nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\ % \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})& \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}) \\ \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}& \sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}&
......
#! /bin/sh #! /bin/sh
# Copyright (C) 2013 Laboratoire de Recherche et # Copyright (C) 2013, 2014 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -24,3 +24,9 @@ set -e ...@@ -24,3 +24,9 @@ set -e
run 0 ../reduc 0 'XFa & FXa' 'XFa' run 0 ../reduc 0 'XFa & FXa' 'XFa'
run 0 ../reduc 0 '(Xf W 0) | X(f W 0)' 'XGf' 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}}'
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
# Check LTL reductions # Check LTL reductions
. ./defs || exit 1 . ./defs || exit 1
set -e set -e
cat >common.txt <<EOF cat >common.txt <<EOF
...@@ -375,14 +376,14 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf) ...@@ -375,14 +376,14 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
{a:b*:c:d*}<>->e, a & ((c & (e M d)) M b) {a:b*:c:d*}<>->e, a & ((c & (e M d)) M b)
{a|b*|c|d*}<>->e, ((a | c) & e) | (e M b) | (e M d) {a|b*|c|d*}<>->e, ((a | c) & e) | (e M b) | (e M d)
{{[*0]|a};b;{[*0]|a};c;e[*]}<>->f, {{[*0]|a};b;{[*0]|a}}<>->X(c&(f|X(f M e))) {{[*0]|a};b;{[*0]|a};c;e[*]}<>->f, {{[*0]|a};b;{[*0]|a}}<>->X(c&(f|X(f M e)))
{a;b[*];c[*];e;f*}, a & X(b W (c W e)) {a;b[*];c[*];e;f*}, a & X({b*;c*;e})
{a;b*;(a* && (b;c));c*}, a & X(b W {a[*] && {b;c}}) {a;b*;(a* && (b;c));c*}, a & X({b*;(a* && (b;c))})
{a;a;b[*2..];b}, a & X(a & X(b & X(b & Xb))) {a;a;b[*2..];b}, a & X(a & X(b & X(b & Xb)))
!{a;a;b[*2..];b}, !a | X(!a | X(!b | X(!b | X!b))) !{a;a;b[*2..];b}, !a | X(!a | X(!b | X(!b | X!b)))
!{a;b[*];c[*];e;f*}, !a | X(!b M (!c M !e)) !{a;c[*];e;f*}, !a | X!{c[*];e}
!{a;b*;(a* && (b;c));c*}, !a | X(!b M !{a[*] && {b;c}}) !{a;b*;(a* && (b;c));c*}, !a | X(!{b*;(a* && (b;c))})
{(a;c*;d)|(b;c)}, (a & X(c W d)) | (b & Xc) {(a;c*;d)|(b;c)}, (a & X{c*;d}) | (b & Xc)
!{(a;c*;d)|(b;c)}, (X(!c M !d) | !a) & (X!c | !b) !{(a;c*;d)|(b;c)}, (X(!{c*;d}) | !a) & (X!c | !b)
(Xc R b) & (Xc W 0), b & XGc (Xc R b) & (Xc W 0), b & XGc
{{c*|1}[*0..1]}<>-> v, {{c[+]|1}[*0..1]}<>-> v {{c*|1}[*0..1]}<>-> v, {{c[+]|1}[*0..1]}<>-> v
{{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*0..5]} <>-> v {{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*0..5]} <>-> v
......
...@@ -1592,10 +1592,10 @@ namespace spot ...@@ -1592,10 +1592,10 @@ namespace spot
// Some term does not accept the empty word. // Some term does not accept the empty word.
unsigned end = mo->size() - 1; unsigned end = mo->size() - 1;
// {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
// = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂})) // = b₁&X(b₂&X({e₁;f₁;e₂;f₂}))
// !{b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
// = !b₁|X(!b₂|X(!b₃ M !{e₁;f₁;e₂;f₂})) // = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂}))
// if e denotes a term that accepts [*0] // if e denotes a term that accepts [*0]
// and b denotes a Boolean formula. // and b denotes a Boolean formula.
while (mo->nth(end)->accepts_eword()) while (mo->nth(end)->accepts_eword())
...@@ -1604,9 +1604,7 @@ namespace spot ...@@ -1604,9 +1604,7 @@ namespace spot
while (start <= end) while (start <= end)
{ {
const formula* r = mo->nth(start); const formula* r = mo->nth(start);
const bunop* es = is_KleenStar(r); if (r->is_boolean() && !opt_.reduce_size_strictly)
if ((r->is_boolean() && !opt_.reduce_size_strictly)
|| (es && es->child()->is_boolean()))
++start; ++start;
else else
break; break;
...@@ -1652,21 +1650,6 @@ namespace spot ...@@ -1652,21 +1650,6 @@ namespace spot
tail = tail =
multop::instance(multop::And, e, 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(); mo->destroy();
result_ = recurse_destroy(tail); 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!
Please register or to comment