From 05ed3def008393a2a5718b323362f63eb898712c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 May 2014 20:06:43 +0200 Subject: [PATCH] snf: Fix the handling of bounded repetition. 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. --- doc/tl/tl.tex | 44 ++++++++++++++++++++++++------- src/ltltest/reduccmp.test | 3 +++ src/ltlvisit/simplify.cc | 23 +++++++++++++++- src/ltlvisit/snf.cc | 55 ++++++++++++++++++++++++++++++++------- src/ltlvisit/snf.hh | 8 ++++-- 5 files changed, 112 insertions(+), 21 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b843ff41e..784f204b2 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -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} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index cfa5de45c..0ff861728 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -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}))*}!' \ diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index e3b6d018d..1bfce7c6b 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -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_; }; @@ -1080,7 +1098,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; } diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index 35447316f..ab7619c72 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -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); + } + } } diff --git a/src/ltlvisit/snf.hh b/src/ltlvisit/snf.hh index b62dc1e48..0b868e3a3 100644 --- a/src/ltlvisit/snf.hh +++ b/src/ltlvisit/snf.hh @@ -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); } }