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

Implement 11 rewritings for []->.

Browse source 
* src/ltlvisit/simplify.cc: Here.
* doc/tl/tl.tex: Document then.
* src/ltlast/bunop.hh (as_KleenStar): New helper function.
* src/ltltest/reduccmp.test: Add more tests.
* src/ltltest/reduc.cc: Also display the resulting formula
without reduce_size_stricly.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-26 17:13:56 +02:00
parent 6eb830c8ae
commit 6f46345c3a
5 changed files with 291 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

32
doc/tl/tl.tex
View file

@ -1183,7 +1183,7 @@ would invalidate the results stored in the caches).
This is implemented by the `\verb|ltl_simplifier::negative_normal_form|`
method.
A formula in negative normal form can only have only have negation
A formula in negative normal form can only have negation
operators ($\NOT$) in front of atomic properties, and does not use any
of the $\XOR$, $\IMPLIES$ and $\EQUIV$ operators. The following
rewriting arrange any PSL formula into negative normal form.
@ -1256,7 +1256,7 @@ The goals in most of these simplification are to:
limit the sources of indeterminism.
\end{itemize}
\subsection{Basic Simplifications}
\subsection{Basic Simplifications}\label{sec:basic-simp}
These simplifications are enabled with
\verb|ltl_simplifier_options::reduce_basics|'. A couple of them may
@ -1431,6 +1431,34 @@ that occur in $r$. For instance $\sere{a\STAR{}\CONCAT
presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but
unfortunately not when the \samp{$\ANDALT$} operator is used.
\subsubsection{Basic Simplifications SERE-LTL Binding Operators}
The following rewritings are applied to the operators $\Asuffix$ and
$\Esuffix$. They assume that $b$, denote a Boolean formula.
As noted at the beginning for section~\ref{sec:basic-simp}, rewritings
denoted with $\equiV$ can be disabled by setting the
\verb|ltl_simplifier_options::reduce_size_strictly|' option to
\texttt{true}.
\begin{align*}
\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{\mvar{i}..\mvar{j}}}\Asuffix f &\equiV
\sere{r}\Asuffix \X(
\sere{r}\Asuffix \X(\ldots
\Asuffix\X(r\STAR{\mvar{1}..\mvar{j-i+1}})))
\text{~if~}i\ge 1\text{~and~}\varepsilon\not\VDash r\\
\sere{r\CONCAT \STAR{}}\Asuffix f &\equiv \sere{r}\Asuffix \G f\\
\sere{r\CONCAT b\STAR{}}\Asuffix f &\equiV \sere{r}\Asuffix (f\AND \X(f \W \NOT b)) \text{~if~}\varepsilon\not\VDash r\\
\sere{\STAR{}\CONCAT r}\Asuffix f &\equiV \G(\sere{r}\Asuffix f)\\
\sere{b\STAR{}\CONCAT r}\Asuffix f &\equiV (\NOT b)\R(\sere{r}\Asuffix f) \text{~if~}\varepsilon\not\VDash r\\
\sere{r_1\CONCAT r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix\X(\sere{r_2}\Asuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
\sere{r_1\FUSION r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix(\sere{r_2}\Asuffix f)\\
\sere{r_1\OR r_2}\Asuffix f &\equiV (\sere{r_1}\Asuffix f)\AND(\sere{r_2}\Asuffix f)
\end{align*}
\subsection{Simplifications for Eventual and Universal Formul\ae}
\label{sec:eventunivrew}

13
src/ltlast/bunop.hh
View file

@ -186,6 +186,19 @@ namespace spot
return is_bunop(f, bunop::Star);
}
/// \brief Cast \a f into a bunop if it is a Star[0..].
///
/// Return 0 otherwise.
inline
bunop*
is_KleenStar(const formula* f)
{
if (bunop* b = is_Star(f))
if (b->min() == 0 && b->max() == bunop::unbounded)
return b;
return 0;
}
}
}
#endif // SPOT_LTLAST_BUNOP_HH

11
src/ltltest/reduc.cc
View file

@ -209,6 +209,7 @@ main(int argc, char** argv)
int length_f1_before = spot::ltl::length(f1);
std::string f1s_before = spot::ltl::to_string(f1);
std::string f1l;
spot::ltl::formula* input_f = f1;
f1 = simp_size->simplify(input_f);
@ -222,11 +223,11 @@ main(int argc, char** argv)
else
{
spot::ltl::formula* maybe_larger = simp->simplify(input_f);
f1l = spot::ltl::to_string(maybe_larger);
if (!simp->are_equivalent(input_f, maybe_larger))
{
std::cerr << "Incorrect reduction (reduce_size_strictly=0) from `"
<< f1s_before << "' to `" << spot::ltl::to_string(f1)
<< "'." << std::endl;
<< f1s_before << "' to `" << f1l << "'." << std::endl;
exit_code = 3;
}
maybe_larger->destroy();
@ -253,8 +254,10 @@ main(int argc, char** argv)
if (!f2 && (!hidereduc || (length_f1_after > length_f1_before)))
{
std::cout << length_f1_before << " " << length_f1_after
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
<< std::endl;
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'";
if (f1l != "" && f1l != f1s_after)
std::cout << " or (w/o rss) to '" << f1l << "'";
std::cout << std::endl;
}
if (f2)

16
src/ltltest/reduccmp.test
View file

@ -290,8 +290,22 @@ for x in ../reduccmp ../reductaustr; do
'{{r1*&r2*}:{b1&&b2}} <>-> x'
run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}} <>-> x' \
'{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}} <>-> x'
run 0 $x '{a&b&c*}|->!Xb' '{(a&&b)|((a&&b):c*)}|-> X!b'
run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
run 0 $x '{[*]}[]->b' 'Gb'
run 0 $x '{a;[*]}[]->b' 'Gb | !a'
run 0 $x '{[*];a}[]->b' 'G(b | !a)'
run 0 $x '{a;b;[*]}[]->c' '!a | X(!b | Gc)'
run 0 $x '{a;a;[*]}[]->c' '!a | X(!a | Gc)'
run 0 $x '{s[*]}[]->b' 'b W !s'
run 0 $x '{s[+]}[]->b' 'b W !s'
run 0 $x '{s[*2..]}[]->b' '!s | X(b W !s)'
run 0 $x '{a;b*;c;d*}[]->e' '!a | X(!b R ((e & X(e W !d)) | !c))'
run 0 $x '{a:b*:c:d*}[]->e' '!a | ((!c | (e W !d)) W !b)'
run 0 $x '{a|b*|c|d*}[]->e' '(e | !(a | c)) & (e W !b) & (e W !d)'
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
'{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'
# not reduced
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
'{a;(b[*2..4];c*;([*0]+{d;e}))*}!'

227
src/ltlvisit/simplify.cc
View file

@ -1772,11 +1772,236 @@ namespace spot
}
}
}
case binop::UConcat:
if (!opt_.reduce_basics)
break;
if (bunop* bu = is_Star(a))
{
// {[*]}[]->b = Gb
if (a == bunop::one_star())
{
a->destroy();
result_ = recurse_destroy(unop::instance(unop::G, b));
return;
}
formula* s = bu->child();
unsigned min = bu->min();
unsigned max = bu->max();
// {s[*]}[]->b = b W !s if s is Boolean.
// {s[+]}[]->b = b W !s if s is Boolean.
if (s->is_boolean() && max == bunop::unbounded && min <= 1)
{
formula* ns = // !s
unop::instance(unop::Not, s->clone());
result_ = // b W !s
binop::instance(binop::W, b, ns);
bu->destroy();
result_ = recurse_destroy(result_);
return;
}
if (opt_.reduce_size_strictly)
break;
// {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())
break;
--min;
if (max != bunop::unbounded)
max -= min; // j-i+1
// Don't rewrite s[1..].
if (min == 0)
break;
formula* tail = // {s[*1..j-i]}[]->b
binop::instance(binop::UConcat,
bunop::instance(bunop::Star,
s->clone(), 1, max),
b);
for (unsigned n = 0; n < min; ++n)
tail = // {s}[]->X(tail)
binop::instance(binop::UConcat,
s->clone(),
unop::instance(unop::X, tail));
result_ = tail;
bu->destroy();
result_ = recurse_destroy(result_);
return;
}
else if (multop* mo = is_Concat(a))
{
unsigned s = mo->size() - 1;
formula* last = mo->nth(s);
// {r;[*]}[]->b = {r}[]->Gb
if (last == bunop::one_star())
{
result_ = binop::instance(binop::UConcat,
mo->all_but(s),
unop::instance(unop::G, b));
mo->destroy();
result_ = recurse_destroy(result_);
return;
}
formula* first = mo->nth(0);
// {[*];r}[]->b = G({r}[]->b)
if (first == bunop::one_star())
{
result_ =
unop::instance(unop::G,
binop::instance(binop::UConcat,
mo->all_but(0),
b));
mo->destroy();
result_ = recurse_destroy(result_);
return;
}
if (opt_.reduce_size_strictly)
break;
// {r;s[*]}[]->b = {r}[]->(b & X(b W !s))
// if s is Boolean and r does not accept [*0];
if (bunop* l = is_KleenStar(last)) // l = s[*]
if (l->child()->is_boolean())
{
formula* r = mo->all_but(s);
if (!r->accepts_eword())
{
formula* ns = // !s
unop::instance(unop::Not, l->child()->clone());
formula* w = // b W !s
binop::instance(binop::W, b->clone(), ns);
formula* x = // X(b W !s)
unop::instance(unop::X, w);
formula* d = // b & X(b W !s)
multop::instance(multop::And, b, x);
result_ = // {r}[]->(b & X(b W !s))
binop::instance(binop::UConcat, r, d);
mo->destroy();
result_ = recurse_destroy(result_);
return;
}
}
// {s[*];r}[]->b = !s R ({r}[]->b)
// if s is Boolean and r does not accept [*0];
if (bunop* l = is_KleenStar(first))
if (l->child()->is_boolean())
{
formula* r = mo->all_but(0);
if (!r->accepts_eword())
{
formula* ns = // !s
unop::instance(unop::Not, l->child()->clone());
formula* u = // {r}[]->b
binop::instance(binop::UConcat, r, b);
result_ = // !s R ({r}[]->b)
binop::instance(binop::R, ns, u);
mo->destroy();
result_ = recurse_destroy(result_);
return;
}
}
// {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b))
// if r₁, r₂, r₃ do not accept [*0].
if (!mo->accepts_eword())
{
unsigned count = 0;
for (unsigned n = 0; n <= s; ++n)
count += !mo->nth(n)->accepts_eword();
assert(count > 0);
if (count == 1)
break;
// Let e denote a term that accepts [*0]
// and let f denote a term that do not.
// A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b
// in which count==2 will be grouped
// as follows: r₁ = e₁;f₁;e₂;e₃
// r₂ = f₂;e₄
// this way we have
// {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b
// where r₁ and r₂ do not accept [*0].
unsigned pos = s + 1;
// We compute the r formulas from the right
// (i.e., r₂ before r₁.)
multop::vec* r = new multop::vec;
do
r->insert(r->begin(), mo->nth(--pos)->clone());
while (r->front()->accepts_eword());
formula* tail = // {r₂}[]->b
binop::instance(binop::UConcat,
multop::instance(multop::Concat, r),
b);
while (--count)
{
multop::vec* r = new multop::vec;
do
r->insert(r->begin(), mo->nth(--pos)->clone());
while (r->front()->accepts_eword());
// If it's the last block, take all leading
// formulae as well.
if (count == 1)
while (pos > 0)
{
r->insert(r->begin(), mo->nth(--pos)->clone());
assert(r->front()->accepts_eword());
}
tail = // X({r₂}[]->b)
unop::instance(unop::X, tail);
tail = // {r₁}[]->X({r₂}[]->b)
binop::instance(binop::UConcat,
multop::instance(multop::Concat, r),
tail);
}
mo->destroy();
result_ = recurse_destroy(tail);
return;
}
}
else if (opt_.reduce_size_strictly)
{
break;
}
else if (multop* mo = is_Fusion(a))
{
// {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b))
unsigned s = mo->size();
formula* tail = b;
do
{
--s;
tail = binop::instance(binop::UConcat,
mo->nth(s)->clone(), tail);
}
while (s != 0);
mo->destroy();
result_ = recurse_destroy(tail);
return;
}
else if (multop* mo = is_OrRat(a))
{
// {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b)
unsigned s = mo->size();
multop::vec* v = new multop::vec;
for (unsigned n = 0; n < s; ++n)
{
formula* x = // {r₁}[]->b
binop::instance(binop::UConcat,
mo->nth(n)->clone(), b->clone());
v->push_back(x);
}
mo->destroy();
b->destroy();
result_ = recurse_destroy(multop::instance(multop::And, v));
return;
}
break;
case binop::Xor:
case binop::Equiv:
case binop::Implies:
case binop::EConcat:
case binop::UConcat:
case binop::EConcatMarked:
// No simplification... Yet?
break;