Commit abff7eba authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent d5b2de7f
......@@ -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:
......
......@@ -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}\\
......
......@@ -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())
......
......@@ -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
......
......@@ -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
......
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