From abff7eba8e391c321c4e480f2c94973423f16ff5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Jul 2016 16:40:59 +0200 Subject: [PATCH] simplifier: new PSL simplifications {e[*0..j]}<>->f = {e[*1..j]}<>->f {e[*0..j]}[]->f = {e[*1..j]}[]->f Fixes #81. This required a small change to the bounded-star-normal-form to prevent infinite recursion. * spot/tl/simplify.cc: Implement these rules. * doc/tl/tl.tex, NEWS: Document them. * tests/core/reduccmp.test: Add tests, and adjust others. * tests/core/unambig.test: Replace formula that used to generated an ambiguous automaton, but now generates a deterministic one. --- NEWS | 4 +++- doc/tl/tl.tex | 7 +++++-- spot/tl/simplify.cc | 29 +++++++++++++++++++++-------- tests/core/reduccmp.test | 12 ++++++++---- tests/core/unambig.test | 2 +- 5 files changed, 38 insertions(+), 16 deletions(-) diff --git a/NEWS b/NEWS index fedabcada..e64d2eda9 100644 --- a/NEWS +++ b/NEWS @@ -111,9 +111,11 @@ New in spot 2.0.3a (not yet released) implies that "autfilt --check=stutter" will now label all automata, not just deterministic automata. - * New LTL simplification rules: + * New LTL and PSL simplification rules: - if e is pure eventuality and g => e, then e U g = Fg - if u is purely universal and u => g, then u R g = Gg + - {s[*0..j]}[]->b = {s[*1..j]}[]->b + - {s[*0..j]}<>->b = {s[*1..j]}<>->b Python: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 74070a6c2..72fc8f3e7 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1565,7 +1565,8 @@ presence of \samp{$\AND$} operators, but unfortunately not when the We extend the above definition to bounded repetitions with: \begin{align*} - r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{\0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}} + r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}}\text{~and~}\varepsilon\not\VDash r^\square\\ + r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{1..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}}\text{~and~}\varepsilon\VDash r^\square \end{align*} where $r^\square$ is recursively defined as follows: \begin{align*} @@ -1603,6 +1604,7 @@ denoted with $\equiV$ can be disabled by setting the \sere{\STAR{}}\Asuffix f &\equiv \G f\\ \sere{b\STAR{}}\Asuffix f &\equiv f \W \NOT b\\ \sere{b\PLUS{}}\Asuffix f &\equiv f \W \NOT b\\ + \sere{r\STAR{0..\mvar{j}}}\Asuffix f &\equiv \sere{r\STAR{1..\mvar{j}}}\Asuffix f \\ \sere{r\STAR{\mvar{i}..\mvar{j}}}\Asuffix f &\equiV \sere{r}\Asuffix \X( \sere{r}\Asuffix \X(\ldots @@ -1618,6 +1620,7 @@ denoted with $\equiV$ can be disabled by setting the \sere{\STAR{}}\Esuffix f &\equiv \F f\\ \sere{b\STAR{}}\Esuffix f &\equiv f \M b\\ \sere{b\PLUS{}}\Esuffix f &\equiv f \M b\\ + \sere{r\STAR{0..\mvar{j}}}\Esuffix f &\equiv \sere{r\STAR{1..\mvar{j}}}\Esuffix f \\ \sere{r\STAR{\mvar{i}..\mvar{j}}}\Esuffix f &\equiV \sere{r}\Esuffix \X( \sere{r}\Esuffix \X(\ldots @@ -1632,7 +1635,7 @@ denoted with $\equiV$ can be disabled by setting the \sere{r_1\OR r_2}\Esuffix f &\equiV (\sere{r_1}\Esuffix f)\OR(\sere{r_2}\Esuffix f) \end{align*} -Here are basic the rewritings for the weak closure and its negation: +Here are the basic rewritings for the weak closure and its negation: \begin{align*} \sere{r\STAR{}}&\equiv \sere{r}& \nsere{r\STAR{}}&\equiv \nsere{r}\\ diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index ff48fb2ae..d4864de50 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1290,14 +1290,20 @@ namespace spot return f; case op::Star: { + if (!f.accepts_eword()) + return f; formula h = f[0]; - auto min = f.min(); - if (h.accepts_eword()) - min = 0; - if (min == 0) - h = f.max() == formula::unbounded() - ? c_->star_normal_form(h) - : c_->star_normal_form_bounded(h); + auto min = 0; + if (f.max() == formula::unbounded()) + { + h = c_->star_normal_form(h); + } + else + { + h = c_->star_normal_form_bounded(h); + if (h.accepts_eword()) + min = 1; + } return formula::Star(h, min, f.max()); } } @@ -1359,12 +1365,19 @@ namespace spot // b W !s return recurse(formula::binop(op_w, b, ns)); } + // {s[*0..j]}[]->b = {s[*1..j]}[]->b + // {s[*0..j]}<>->b = {s[*1..j]}<>->b + if (min == 0) + return recurse(formula::binop(bindop, + formula::Star(s, 1, max), b)); + if (opt_.reduce_size_strictly) return orig; // {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b // = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b))) // if i>0 and s does not accept the empty word - if (min == 0 || s.accepts_eword()) + assert(min > 0); + if (s.accepts_eword()) return orig; --min; if (max != formula::unbounded()) diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index e9717b988..a423bd6cd 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -395,12 +395,16 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf) {(a;c*;d)|(b;c)}, (a & X{c*;d}) | (b & Xc) !{(a;c*;d)|(b;c)}, (X(!{c*;d}) | !a) & (X!c | !b) (Xc R b) & (Xc W 0), b & XGc -{{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 +{{c*|1}[*0..1]}<>-> v, v | (v M c) +{{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*1..5]} <>-> v +{{b*&c*}[*3..5]}<>-> v, {{b[+]|c[+]}[*1..5]} <>-> v +{((a*;b)+[*0])[*4..6]}!, {((a*;b))[*1..6]}! +# issue 81 +{e[*0..5]}<>->f, {e[*1..5]}<>->f +{e[*0..5]}[]->f, {e[*1..5]}[]->f +{(e+[*0])[*0..5]}[]->f, {e[*1..5]}[]->f # not reduced {a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}! -{((a*;b)+[*0])[*4..6]}!, {((a*;b))[*0..6]}! {c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a EOF diff --git a/tests/core/unambig.test b/tests/core/unambig.test index ea36a8912..bcc1a9b0c 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -42,7 +42,7 @@ do grep -E 'properties:.* (unambiguous|deterministic)' done -for f in FGa '(({p1[*0..1]}[]-> 0) R XFp0)' +for f in FGa '{[*1..4]}<>-> (p1 & (p1 U p0))' do $ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous