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

Trivially reduce f;f to f[*2], f[*1..3];f to f[*2..4], etc.

* src/ltlast/multop.cc (instance): Implement the reduction.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Add a test.
parent 4a775a17
......@@ -687,7 +687,7 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
\0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
\eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
f\STAR{0}&\equiv \eword \\
f\STAR{0}&\equiv \eword &
f\STAR{1}&\equiv f\\
\end{align*}
......@@ -697,9 +697,6 @@ The following rules are all valid with the two arguments swapped.
%\samp{$\FUSION$}.)
\begin{align*}
f\AND f &\equiv f&
f\ANDALT f &\equiv f &
f\OR f &\equiv f \\
\0\AND f &\equiv \0 &
\0\ANDALT f &\equiv \0 &
\0\OR f &\equiv f &
......@@ -715,22 +712,33 @@ The following rules are all valid with the two arguments swapped.
\1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
&&
\STAR{} \AND f &\equiv f &
\STAR{} \OR f &\equiv \1\STAR{} &
\STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
&&
\STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
\eword\AND f &\equiv f &
\eword\ANDALT f &\equiv
\begin{cases}
\eword &\mathrlap{\text{if~} \varepsilon\VDash f} \\
\0 &\mathrlap{\text{if~} \varepsilon\nVDash f} \\
\mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
\0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
\end{cases} &
&&
\eword \FUSION f &\equiv \0 &
\eword \CONCAT f &\equiv f\\
f\AND f &\equiv f&
f\ANDALT f &\equiv f &
f\OR f &\equiv f&
&&
f\CONCAT f&\equiv f\STAR{2}\\
b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
&&
&&
b_1:b_2 &\equiv b_1\ANDALT b_2\\
b_1:b_2 &\equiv b_1\ANDALT b_2 &
f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}}\\
&&
&&
&&
&&
\mathllap{f\STAR{\mvar{i}..\mvar{j}}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
\end{align*}
\section{SERE-LTL Binding Operators}
......
......@@ -501,6 +501,75 @@ namespace spot
v->swap(tmp);
}
}
else if (op == Concat)
{
// Perform an extra loop to merge starable items.
// f;f -> f[*2]
// f;f[*i..j] -> f[*i+1..j+1]
// f[*i..j];f -> f[*i+1..j+1]
// f[*i..j];f[*k..l] -> f[*i+k..j+l]
i = v->begin();
while (i != v->end())
{
vec::iterator fpos = i;
formula* f;
unsigned min;
unsigned max;
bool changed = false;
if (bunop* is = is_Star(*i))
{
f = is->child();
min = is->min();
max = is->max();
}
else
{
f = *i;
min = max = 1;
}
++i;
while (i != v->end())
{
formula* f2;
unsigned min2;
unsigned max2;
if (bunop* is = is_Star(*i))
{
f2 = is->child();
if (f2 != f)
break;
min2 = is->min();
max2 = is->max();
}
else
{
f2 = *i;
if (f2 != f)
break;
min2 = max2 = 1;
}
if (min2 == bunop::unbounded)
min = bunop::unbounded;
else if (min != bunop::unbounded)
min += min2;
if (max2 == bunop::unbounded)
max = bunop::unbounded;
else if (max != bunop::unbounded)
max += max2;
(*i)->destroy();
i = v->erase(i);
changed = true;
}
if (changed)
{
formula* newfs = bunop::instance(bunop::Star, f->clone(),
min, max);
(*fpos)->destroy();
*fpos = newfs;
}
}
}
}
vec::size_type s = v->size();
......
......@@ -111,6 +111,8 @@ namespace spot
/// - Concat(Exps1...,FExps2...,1[*],FExps3...,Exps4) =
/// Concat(Exps1...,1[*],Exps4) if FExps2...FExps3... all accept [*0]
/// - Concat(Exp) = Exp
/// - Concat(Exps1...,E,E[*i..j],E[*k..l],Exps2...) =
/// Concat(Exps1...,E[*1+i+k..j+l],Exps2...) and similar forms
/// - Fusion(Exps1...1,Exps2...) = Fusion(Exps1...,Exps2...)
/// if at least one exp reject [*0]
/// - Fusion(Exps1...,0,Exps2...) = 0
......
......@@ -164,6 +164,7 @@ run 1 ../equals '{(a;!a)*:(a;!a)*:b}!' '{(a;!a)*:b}!'
run 1 ../equals '{(1:a*);b}!' '{a*;b}!'
run 0 ../equals '{z;a*;b*;*;c;d;*;b*;e;a*;*;b*}' '{z;[*];c;d;[*];e;[*]}'
run 0 ../equals '{((a;b)|[*0]);[*];c}!' '{[*];c}!'
run 0 ../equals '{a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}' '{a[*3..];b[+];c[*6..8]}'
run 0 ../equals '{a[*0]}' '{[*0]}'
run 0 ../equals '{a[*..]}' '{a[*]}'
......
Supports Markdown
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