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

snf: Fix the handling of bounded repetition.

Browse source 
star_normal_form() used to be called under bounded
repetitions like [*0..4], but some of these rewritings
are only correct for [*0..].  For instance
     (a*|1)[*]      can be rewritten to    1[*]
but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
it would be correct to rewrite the latter as (a[+]|1)[*0..1],
canceling the empty word in a*.

Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
and it cannot either be rewritten to (a[+]|b[+])[*0..1].

This patch introduces a new function to implement
rewritings under bounded repetition.

* src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
New function.
* src/ltlvisit/simplify.cc: Use it.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document the rewritings implemented.
This commit is contained in:
Alexandre Duret-Lutz 2014-05-15 20:06:43 +02:00
parent f431852af9
commit 139f7b49b4
5 changed files with 112 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

44
doc/tl/tl.tex
View file

@ -1469,27 +1469,53 @@ SERE.
Starred subformul\ae{} are rewritten in Star Normal
Form~\cite{bruggeman.96.tcs} with:
\[r\STAR{\mvar{0}..\mvar{j}} \equiv r^\circ\STAR{\mvar{0}..\mvar{j}} \]
\[r\STAR{} \equiv r^\circ\STAR{} \]
where $r^\circ$ is recursively defined as follows:
\begin{align*}
r^\circ &= r\text{~if~} \varepsilon\not\VDash r \\
\eword^\circ &= \0 &
(r_1\CONCAT r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
r\STAR{\mvar{0}..\mvar{j}}^\circ &= r^\circ &
r\STAR{\mvar{i}..\mvar{j}}^\circ &= r^\circ \text{~if~} i=0 \text{~or~} \varepsilon\VDash r&
(r_1\AND r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
(r_1\OR r_2)^\circ &= r_1^\circ \OR r_2^\circ &
(r_1\ANDALT r_2)^\circ &= r_1 \ANDALT r_2
\end{align*}
Note: the original SNF definition~\cite{bruggeman.96.tcs} does not
include \samp{$\FUSION$}, \samp{$\AND$}, and \samp{$\ANDALT$}
operators, and it guarantees that $\forall r,\,\varepsilon\not\VDash
r^\circ$ because $r^\circ$ is stripping all the stars and empty words
that occur in $r$. For instance $\sere{a\STAR{}\CONCAT
b\STAR{}\CONCAT\sere{\1\OR c}}^\circ\STAR{} = \sere{a\OR b\OR
include \samp{$\AND$} and \samp{$\ANDALT$} operators, and it
guarantees that $\forall r,\,\varepsilon\not\VDash r^\circ$ because
$r^\circ$ is stripping all the stars and empty words that occur in
$r$. For instance $\sere{a\STAR{}\CONCAT
b\STAR{}\CONCAT\sere{\eword\OR c}}^\circ\STAR{} = \sere{a\OR b\OR
c}\STAR{}$. Our extended definition still respects this property in
presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but
unfortunately not when the \samp{$\ANDALT$} operator is used.
presence of \samp{$\AND$} operators, but unfortunately not when the
\samp{$\ANDALT$} operator is used.
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}}
\end{align*}
where $r^\square$ is recursively defined as follows:
\begin{align*}
r^\square &= r\text{~if~} \varepsilon\not\VDash r \\
\eword^\square &= \0 &
(r_1\CONCAT r_2)^\square &= r_1\CONCAT r_2\\
r\STAR{\mvar{i}..\mvar{j}}^\square &= r^\square\STAR{\mvar{\max(1,i)}..\mvar{j}} \text{~if~} i=0 \text{~or~} \varepsilon\VDash r &
(r_1\AND r_2)^\square &= r_1^\square\OR r_2^\square \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
(r_1\OR r_2)^\square &= r_1^\square \OR r_2^\square &
(r_1\ANDALT r_2)^\square &= r_1 \ANDALT r_2
\end{align*}
The differences between $^\square$ and $^\circ$ are in the handling
of $r\STAR{\mvar{i}..\mvar{j}}$ and in the handling of $r_1\CONCAT r_2$.
% Indeed $(c\STAR{}\OR\1)\STAR{0..1}$ is not equivalent to
% $(c\STAR{}\OR\1)^\circ\STAR{0..1}\equiv(c\OR\1)\STAR{0..1}\equiv
% 1\STAR{0..1}$ but to
% $(c\STAR{}\OR\1)^\square\STAR{0..1}\equiv(c\PLUS{}\OR\1)\STAR{0..1}$.
% Similarly $(a\STAR{}\CONCAT b\STAR{})\STAR{0..1})$ is definitely not
% equal to $(a\PLUS{}\OR b\PLUS{})\STAR{0..1}).
\subsubsection{Basic Simplifications SERE-LTL Binding Operators}

3
src/ltltest/reduccmp.test
View file

@ -364,6 +364,9 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'
run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v'
run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v'
run 0 $x '{{b*&c*}[*3..5]}<>-> v' '{{b[+]|c[+]}[*0..5]} <>-> v'
# not reduced
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \

23
src/ltlvisit/simplify.cc
View file

@ -106,6 +106,16 @@ namespace spot
old->first->destroy();
}
}
{
snf_cache::iterator i = snfb_cache_.begin();
snf_cache::iterator end = snfb_cache_.end();
while (i != end)
{
snf_cache::iterator old = i++;
old->second->destroy();
old->first->destroy();
}
}
{
f2f_map::iterator i = bool_isop_.begin();
f2f_map::iterator end = bool_isop_.end();
@ -387,6 +397,13 @@ namespace spot
return ltl::star_normal_form(f, &snf_cache_);
}
const formula*
star_normal_form_bounded(const formula* f)
{
return ltl::star_normal_form_bounded(f, &snfb_cache_);
}
const formula*
boolean_to_isop(const formula* f)
{
@ -406,6 +423,7 @@ namespace spot
f2f_map nenoform_;
syntimpl_cache_t syntimpl_;
snf_cache snf_cache_;
snf_cache snfb_cache_;
f2f_map bool_isop_;
};
@ -1081,7 +1099,10 @@ namespace spot
min = 0;
if (min == 0)
{
const formula* s = c_->star_normal_form(h);
const formula* s =
bo->max() == bunop::unbounded ?
c_->star_normal_form(h) :
c_->star_normal_form_bounded(h);
h->destroy();
h = s;
}

55
src/ltlvisit/snf.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Developpement
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -31,6 +31,7 @@ namespace spot
// E°
class snf_visitor: public visitor
{
protected:
const formula* result_;
snf_cache* cache_;
public:
@ -144,21 +145,50 @@ namespace spot
if (!f->accepts_eword())
return f->clone();
if (cache_)
{
snf_cache::const_iterator i = cache_->find(f);
if (i != cache_->end())
return i->second->clone();
}
snf_cache::const_iterator i = cache_->find(f);
if (i != cache_->end())
return i->second->clone();
f->accept(*this);
if (cache_)
(*cache_)[f->clone()] = result_->clone();
(*cache_)[f->clone()] = result_->clone();
return result_;
}
};
// E^□
class snf_visitor_bounded: public snf_visitor
{
public:
snf_visitor_bounded(snf_cache* c): snf_visitor(c)
{
}
void
visit(const bunop* bo)
{
bunop::type op = bo->op();
switch (op)
{
case bunop::Star:
assert(bo->accepts_eword());
result_ = bunop::instance(bunop::Star,
recurse(bo->child()),
std::max(bo->min(), 1U),
bo->max());
break;
}
}
void
visit(const multop* mo)
{
if (mo->op() == multop::Concat)
result_ = mo->clone();
else
this->snf_visitor::visit(mo);
}
};
}
@ -169,5 +199,12 @@ namespace spot
return v.recurse(sere);
}
const formula*
star_normal_form_bounded(const formula* sere, snf_cache* cache)
{
snf_visitor_bounded v(cache);
return v.recurse(sere);
}
}
}

8
src/ltlvisit/snf.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -52,6 +52,10 @@ namespace spot
/// \param cache an optional cache
SPOT_API const formula*
star_normal_form(const formula* sere, snf_cache* cache = 0);
/// A variant of star_normal_form() for r[*0..j] where j < ω.
SPOT_API const formula*
star_normal_form_bounded(const formula* sere, snf_cache* cache = 0);
}
}