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

Trivially reduce [*];f to [*] if f accepts the empty word.

* src/ltlast/multop.cc (instance): Implement the reduction.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.
parent e06b3b79
......@@ -707,17 +707,17 @@ The following rules are all valid with the two arguments swapped.
\0 \CONCAT f &\equiv \0 \\
\1\AND f&\equiv
\begin{cases}
1 &\mathrlap{\text{if~} \varepsilon\VDash f} \\
f &\mathrlap{\text{if~} \varepsilon\nVDash f} \\
1\mathrlap{\text{~if~} \varepsilon\VDash f} \\
f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\
\end{cases} &
\1\ANDALT b &\equiv b &
\1\OR b &\equiv \1 &
\1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
&&
\1\STAR{} \AND f &\equiv f &
\1\STAR{} \OR f &\equiv \1\STAR{} &
\STAR{} \AND f &\equiv f &
\STAR{} \OR f &\equiv \1\STAR{} &
&&
&& \\
\STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
\eword\AND f &\equiv f &
\eword\ANDALT f &\equiv
\begin{cases}
......
......@@ -337,6 +337,44 @@ namespace spot
abs = constant::false_instance();
abs2 = 0;
weak_abs = 0;
// - Concat(Exps1...,FExps2...,1[*],FExps3...,Exps4) =
// Concat(Exps1...,1[*],Exps4)
// If FExps2... and FExps3 all accept [*0].
{
vec::iterator i = v->begin();
formula* os = bunop::one_star();
while (i != v->end())
{
while (i != v->end() && !(*i)->accepts_eword())
++i;
if (i == v->end())
break;
vec::iterator b = i;
// b is the first expressions that accepts [*0].
// let's find more, and locate the position of
// 1[*] at the same time.
bool os_seen = false;
do
{
os_seen |= (*i == os);
++i;
}
while (i != v->end() && (*i)->accepts_eword());
if (os_seen) // [b..i) is a range that contains [*].
{
// Place [*] at the start of the range, and erase
// all other formulae.
(*b)->destroy();
*b++ = os->clone();
for (vec::iterator c = b; c < i; ++c)
(*c)->destroy();
i = v->erase(b, i);
}
}
}
break;
case Fusion:
neutral = constant::true_instance();
......
......@@ -108,6 +108,8 @@ namespace spot
/// - OrRat(Exps1...,1[*],Exps2...) = 1[*]
/// - Concat(Exps1...,0,Exps2...) = 0
/// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...)
/// - Concat(Exps1...,FExps2...,1[*],FExps3...,Exps4) =
/// Concat(Exps1...,1[*],Exps4) if FExps2...FExps3... all accept [*0]
/// - Concat(Exp) = Exp
/// - Fusion(Exps1...1,Exps2...) = Fusion(Exps1...,Exps2...)
/// if at least one exp reject [*0]
......
......@@ -162,6 +162,8 @@ run 0 ../equals '{c*:1:{a;b}:1}!' '{c*:{a;b}}!'
run 1 ../equals '{(a;!a)*:(a;!a)*:b}!' '{(a;!a)*:b}!'
# make sure 1:a* is not reduced to a*.
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[*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