alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Improve simplification of expr[*0..1]

Browse source 
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-02 16:35:18 +02:00
parent 190d4cfaf1
commit e8527d5ae9
4 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -184,6 +184,10 @@ New in spot 2.3.5.dev (not yet released)
G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd),
and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd).
When working with SERE, the simplification of "expr[*0..1]" was
improved. E.g. {{a[*]|b}[*0..1]} becomes {a[*]|b} instead of
{{a[+]|b}[*0..1]}.
- The new function spot::to_weak_alternating() is able to take an
input automaton with generalized Büchi/co-Büchi acceptance and
convert it to a weak alternating automaton.

5
doc/tl/tl.tex
View file

@ -1560,8 +1560,9 @@ 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}}\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
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}},\,\varepsilon\not\VDash r^\square,\,\text{~and~}j>1\\
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}},\,\varepsilon\VDash r^\square\,\text{~and~}j>1\\
r\STAR{\mvar{i}..\mvar{j}} & \equiv r\phantom{^\square\STAR{1..\mvar{j}}}\quad\text{if}\quad\varepsilon\VDash r\text{~and~}\mvar{j}=1
\end{align*}
where $r^\square$ is recursively defined as follows:
\begin{align*}

2
spot/tl/simplify.cc
View file

@ -1362,6 +1362,8 @@ namespace spot
if (!f.accepts_eword())
return f;
formula h = f[0];
if (f.max() == 1 && h.accepts_eword())
return h;
auto min = 0;
if (f.max() == formula::unbounded())
{

1
tests/core/reduccmp.test
View file

@ -376,6 +376,7 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
{a:b*:c:d*}[]->e, !a | ((!c | (e W !d)) W !b)
{a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
{{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
{(a[*]|b)[*0..1];c}, {{b | a[*]};c}
{a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
{[*]}<>->b, Fb