diff --git a/NEWS b/NEWS index 654eb11d2..5d5eac861 100644 --- a/NEWS +++ b/NEWS @@ -67,7 +67,14 @@ New in spot 1.99a (not yet released) either by Divine (as patched by the LTSmin people) or by Spins (the LTSmin compiler for Promela). - - LTL formulas can include /* comments */. + - LTL/PSL formulas can include /* comments */. + + - PSL SEREs support a new operator [:*i..j], the iterated fusion. + [:*i..j] is to the fusion operator ':' what [*i..j] is to the + concatenation operator ';'. For instance (a*;b)[:*3] is the + same as (a*;b):(a*;b):(a*;b). The operator [:+], is syntactic + sugar for [:*1..], and corresponds to the operator ⊕ introduced + by Dax et al. (ATVA'09). - GraphViz output now uses an horizontal layout by default. The --dot option of the various command-line tools takes an diff --git a/doc/tl/spotltl.sty b/doc/tl/spotltl.sty index ead5536db..b8178ee6b 100644 --- a/doc/tl/spotltl.sty +++ b/doc/tl/spotltl.sty @@ -8,11 +8,11 @@ \newcommand{\ffalse}{\bot} \newcommand{\eword}{\varepsilon} % empty word, denoted by [*0] in PSL -% These three are not declared as operator +% These three are not declared as operators \newcommand{\F}{\mathsf{F}} % eventually \newcommand{\G}{\mathsf{G}} % always \newcommand{\X}{\mathsf{X}} % next -% The \mathbin tell TeX to adjust spacing for binary operators +% The \mathbin tells TeX to adjust spacing for binary operators \newcommand{\M}{\mathbin{\mathsf{M}}} % strong release \newcommand{\R}{\mathbin{\mathsf{R}}} % release \newcommand{\U}{\mathbin{\mathsf{U}}} % until @@ -25,9 +25,11 @@ % Star-like PSL operators \newcommand{\SereStar}[1]{^{\star#1}} +\newcommand{\SereFStar}[1]{^{\mathsf{:}\star#1}} \newcommand{\SereEqual}[1]{^{=#1}} \newcommand{\SereGoto}[1]{^{\to#1}} \newcommand{\SerePlus}{^+} +\newcommand{\SereFPlus}{^{\mathsf{:}+}} \newcommand{\SereFusion}{\mathbin{\mathsf{:}}} \newcommand{\SereConcat}{\mathbin{\mathsf{;}}} \newcommand{\SereOr}{\cup} @@ -45,5 +47,3 @@ %\newcommand{\seqXM}{\seqX} \newcommand{\triggers}{\boxright} \newcommand{\triggersX}{\boxRight} - - diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index d04d72b33..b791586c5 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -92,6 +92,7 @@ \newcommand{\EQUAL}[1]{\texttt{[=#1]}} \newcommand{\GOTO}[1]{\texttt{[->#1]}} \newcommand{\PLUS}{\texttt{[+]}} +\newcommand{\FPLUS}{\texttt{[:+]}} \newcommand{\eword}{\texttt{[*0]}} \newcommand{\Esuffix}{\texttt{<>->}} @@ -599,14 +600,22 @@ denote arbitrary SERE. NLM intersection\footnotemark & $f\AND g$ \\ concatenation & $f\CONCAT g$ \\ fusion & $f\FUSION g$ \\ - bounded repetition & $f\STAR{\mvar{i}..\mvar{j}}$ + bounded ;-iter. & $f\STAR{\mvar{i}..\mvar{j}}$ & $f\STAR{\mvar{i}:\mvar{j}}$ & $f\STAR{\mvar{i} to \mvar{j}}$ & $f\STAR{\mvar{i},\mvar{j}}$\\ - \llap{un}bounded repetition & $f\STAR{\mvar{i}..}$ + \llap{un}bounded ;-iter. & $f\STAR{\mvar{i}..}$ & $f\STAR{\mvar{i}:}$ & $f\STAR{\mvar{i} to}$ & $f\STAR{\mvar{i},}$\\ + bounded :-iter. & $f\FSTAR{\mvar{i}..\mvar{j}}$ + & $f\FSTAR{\mvar{i}:\mvar{j}}$ + & $f\FSTAR{\mvar{i} to \mvar{j}}$ + & $f\FSTAR{\mvar{i},\mvar{j}}$\\ + \llap{un}bounded :-iter. & $f\FSTAR{\mvar{i}..}$ + & $f\FSTAR{\mvar{i}:}$ + & $f\FSTAR{\mvar{i} to}$ + & $f\FSTAR{\mvar{i},}$\\ \end{tabular} \end{center} @@ -657,6 +666,26 @@ $a$ is an atomic proposition. \text{or} & \mvar{i}>0 \land (\exists k\in\N,\, (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} \VDash f\STAR{\mvar{i-1}..}))\\ + \end{cases}\\ + \sigma\VDash f\FSTAR{\mvar{i}..\mvar{j}}& \iff + \begin{cases} + \text{either} & \mvar{i}=0 \land \mvar{j}=0 \land \sigma\VDash\1 \\ + \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\, + (\sigma^{0..k}\VDash f) \land (\sigma^{k..} + \VDash f\FSTAR{\mvar{0}..\mvar{j-1}}))\\ + \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\, + (\sigma^{0..k}\VDash f) \land (\sigma^{k..} + \VDash f\FSTAR{\mvar{i-1}..\mvar{j-1}}))\\ + \end{cases}\\ + \sigma\VDash f\FSTAR{\mvar{i}..} & \iff + \begin{cases} + \text{either} & \mvar{i}=0 \land \sigma\VDash\1 \\ + \text{or} & \mvar{i}=0 \land (\exists k\in\N,\, + (\sigma^{0..k}\VDash f) \land (\sigma^{k..} + \VDash f\FSTAR{\mvar{0}..}))\\ + \text{or} & \mvar{i}>0 \land (\exists k\in\N,\, + (\sigma^{0..k}\VDash f) \land (\sigma^{k..} + \VDash f\FSTAR{\mvar{i-1}..}))\\ \end{cases} \end{align*}} @@ -668,6 +697,29 @@ operands are Boolean formulas. regardless of the value of $f$ and $g$. For instance $a\STAR{}\FUSION b\STAR{}$ is actually equivalent to $a\STAR{}\CONCAT\sere{a\ANDALT b}\CONCAT b\STAR{}$. +\item The $\FSTAR{\mvar{i}..}$ and $\FSTAR{\mvar{i}..\mvar{j}}$ operators are + iterations of the $\FUSION$ operator just like + The $\STAR{\mvar{i}..}$ and $\STAR{\mvar{i}..\mvar{j}}$ are + iterations of the $\CONCAT$ operator. More graphically: + \begin{align*} + f\STAR{\mvar{i}..\mvar{j}} &= + \underbrace{f\CONCAT f\CONCAT \ldots \CONCAT f}_{\text{between $\mvar{i}$ and $\mvar{j}$ copies of $f$}} & + f\FSTAR{\mvar{i}..\mvar{j}} &= + \underbrace{f\FUSION f\FUSION \ldots \FUSION f}_{\text{between $\mvar{i}$ and $\mvar{j}$ copies of $f$}}\\ + \intertext{with the convention that} + f\STAR{0..0} &= \eword & + f\FSTAR{0..0} &= \1 + \end{align*} +\item The $\FSTAR{\mvar{i}..}$ and $\FSTAR{\mvar{i}..\mvar{j}}$ + operators are not defined in PSL. While the bounded iteration can + be seen as syntactic sugar on $\FUSION$, the unbounded version + really is a new operator. + + $\FSTAR{1..}$, for which we define the $\FPLUS$ syntactic sugar + below, actually corresponds to the $^\oplus$ operator introduced + by~\citet{dax.09.atva}. With this simple addition, it is possible + to define a subset of PSL that expresses exactly the + stutter-invariant $\omega$-regular languages. \end{itemize} \subsection{Syntactic Sugar} @@ -687,24 +739,28 @@ it for output. $b$ must be a Boolean formula. \begin{align*} f\STARALT &\equiv f\STAR{0..}\\ f\STAR{} &\equiv f\STAR{0..} & - f\PLUS{} &\equiv f\STAR{1..} & + f\FSTAR{} &\equiv f\FSTAR{0..} & f\EQUAL{} &\equiv f\EQUAL{0..} & f\GOTO{} &\equiv f\GOTO{1..1} \\ f\STAR{..} &\equiv f\STAR{0..} & - && + f\FSTAR{..} &\equiv f\FSTAR{0..} & f\EQUAL{..} &\equiv f\EQUAL{0..} & f\GOTO{..} &\equiv f\GOTO{1..} \\ f\STAR{..\mvar{j}} &\equiv f\STAR{0..\mvar{j}} & - && + f\FSTAR{..\mvar{j}} &\equiv f\FSTAR{0..\mvar{j}} & f\EQUAL{..\mvar{j}} &\equiv f\EQUAL{0..\mvar{j}} & f\GOTO{..\mvar{j}} &\equiv f\GOTO{1..\mvar{j}} \\ f\STAR{\mvar{k}} &\equiv f\STAR{\mvar{k}..\mvar{k}} & - && + f\FSTAR{\mvar{k}} &\equiv f\FSTAR{\mvar{k}..\mvar{k}} & f\EQUAL{\mvar{k}} &\equiv f\EQUAL{\mvar{k}..\mvar{k}} & f\GOTO{\mvar{k}} &\equiv f\GOTO{\mvar{k}..\mvar{k}} \\ - \STAR{} &\equiv \1\STAR{0..} & - \PLUS{} &\equiv \1\STAR{1..} \\ - \STAR{\mvar{k}} &\equiv \1\STAR{\mvar{k}..\mvar{k}} & + f\PLUS{} &\equiv f\STAR{1..} & + f\FPLUS{} &\equiv f\FSTAR{1..} +\end{align*} +\begin{align*} +\STAR{\mvar{k}} &\equiv \1\STAR{\mvar{k}..\mvar{k}} & +\STAR{} &\equiv \1\STAR{0..} & +\PLUS{} &\equiv \1\STAR{1..} \end{align*} \subsection{Trivial Identities (Occur Automatically)} @@ -720,6 +776,14 @@ $b_1$, $b_2$ are assumed to be Boolean formulas. 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{1}&\equiv f\\ + b\FSTAR{0..\mvar{j}} &\equiv \1 & + b\FSTAR{\mvar{i}..\mvar{j}} &\equiv b \text{~if~}i>0 \\ + \eword\FSTAR{0..\mvar{j}} &\equiv \1& + \eword\FSTAR{\mvar{i}..\mvar{j}} &\equiv \0\text{~if~}i>0 \\ + && + f\FSTAR{\mvar{i}..\mvar{j}}\FSTAR{\mvar{k}..\mvar{l}} &\equiv f\FSTAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\ + f\FSTAR{0}&\equiv \1 & + f\FSTAR{1}&\equiv f\text{~if~}\varepsilon\nVDash f\\ \end{align*} \noindent @@ -758,20 +822,19 @@ The following rules are all valid with the two arguments swapped. f\AND f &\equiv f& f\ANDALT f &\equiv f & f\OR f &\equiv f& - && + f\FUSION f&\equiv f\FSTAR{2}& 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 & - 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}}\\ + b_1:b_2 &\equiv b_1\ANDALT b_2 +\end{align*} +\begin{align*} +f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}} & +f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\ +f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f&\equiv f\FSTAR{\mvar{i+1}..\mvar{j+1}} & +f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}} \end{align*} - \section{SERE-LTL Binding Operators} The following operators combine a SERE $r$ with a PSL diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index b5c385124..1c147c0e4 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -61,6 +61,11 @@ namespace spot if (min_ == 0) is.accepting_eword = true; break; + case FStar: + is.accepting_eword = false; + if (max_ == unbounded) + is.finite = false; + break; } } @@ -106,6 +111,8 @@ namespace spot { case Star: return "Star"; + case FStar: + return "FStar"; } SPOT_UNREACHABLE(); } @@ -120,20 +127,22 @@ namespace spot case Star: // Syntactic sugaring if (min_ == 1 && max_ == unbounded) - { - out << "[+]"; - return out.str(); - } + return "[+]"; out << "[*"; break; + case FStar: + // Syntactic sugaring + if (min_ == 1 && max_ == unbounded) + return "[:+]"; + out << "[:*"; + break; } if (min_ != 0 || max_ != unbounded) { - // Always print the min_, even when it is equal to - // default_min, this way we avoid ambiguities (like - // when reading a[*..3];b[->..2] which actually - // means a[*0..3];b[->1..2]. + // Always print the min_, even when it is equal to 0, this + // way we avoid ambiguities (like when reading + // a[*..3];b[->..2] which actually means a[*0..3];b[->1..2]. out << min_; if (min_ != max_) { @@ -154,86 +163,110 @@ namespace spot { assert(min <= max); - // Some trivial simplifications. - + const formula* neutral = nullptr; switch (op) { case Star: + neutral = constant::empty_word_instance(); + break; + case FStar: + neutral = constant::true_instance(); + break; + } + + + // common trivial simplifications + + // - [*0][*min..max] = [*0] + // - [*0][:*0..max] = 1 + // - [*0][:*min..max] = 0 if min > 0 + if (child == constant::empty_word_instance()) + switch (op) { - // - [*0][*min..max] = [*0] - if (child == constant::empty_word_instance()) - return child; - - // - 0[*0..max] = [*0] - // - 0[*min..max] = 0 if min > 0 - if (child == constant::false_instance()) - { - if (min == 0) - return constant::empty_word_instance(); - else - return child; - } - - // - Exp[*0] = [*0] - if (max == 0) - { - child->destroy(); - return constant::empty_word_instance(); - } - - // - Exp[*1] = Exp - if (min == 1 && max == 1) - return child; - - // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] - // if i*(min+1)<=j(min)+1. - if (const bunop* s = is_bunop(child)) - { - unsigned i = s->min(); - unsigned j = s->max(); - - // Exp has to be true between i*min and j*min - // then between i*(min+1) and j*(min+1) - // ... - // finally between i*max and j*max - // - // We can merge these intervals into [i*min..j*max] iff the - // first are adjacent or overlap, i.e. iff - // i*(min+1) <= j*min+1. - // (Because i<=j, this entails that the other intervals also - // overlap). - - const formula* exp = s->child(); - if (j == unbounded) - { - min *= i; - max = unbounded; - - // Exp[*min..max] - exp->clone(); - child->destroy(); - child = exp; - } - else - { - if (i * (min + 1) <= (j * min) + 1) - { - min *= i; - if (max != unbounded) - { - if (j == unbounded) - max = unbounded; - else - max *= j; - } - exp->clone(); - child->destroy(); - child = exp; - } - } - } - break; + case Star: + return neutral; + case FStar: + if (min == 0) + return neutral; + else + return constant::false_instance(); } + + // - 0[*0..max] = [*0] + // - 0[*min..max] = 0 if min > 0 + // - b[:*0..max] = 1 + // - b[:*min..max] = 0 if min > 0 + if (child == constant::false_instance() + || (op == FStar && child->is_boolean())) + { + if (min == 0) + { + child->destroy(); + return neutral; + } + return child; + } + + // - Exp[*0] = [*0] + // - Exp[:*0] = 1 + if (max == 0) + { + child->destroy(); + return neutral; + } + + // - Exp[*1] = Exp + // - Exp[:*1] = Exp if Exp does not accept [*0] + if (min == 1 && max == 1) + if (op == Star || !child->accepts_eword()) + return child; + + // - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. + // - Exp[:*i..j][:*k..l] = Exp[:*ik..jl] if i*(k+1)<=jk+1. + if (const bunop* s = is_bunop(child, op)) + { + unsigned i = s->min(); + unsigned j = s->max(); + + // Exp has to be true between i*min and j*min + // then between i*(min+1) and j*(min+1) + // ... + // finally between i*max and j*max + // + // We can merge these intervals into [i*min..j*max] iff the + // first are adjacent or overlap, i.e. iff + // i*(min+1) <= j*min+1. + // (Because i<=j, this entails that the other intervals also + // overlap). + + const formula* exp = s->child(); + if (j == unbounded) + { + min *= i; + max = unbounded; + + // Exp[*min..max] + exp->clone(); + child->destroy(); + child = exp; + } + else + { + if (i * (min + 1) <= (j * min) + 1) + { + min *= i; + if (max != unbounded) + { + if (j == unbounded) + max = unbounded; + else + max *= j; + } + exp->clone(); + child->destroy(); + child = exp; + } + } } const formula* res; diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 30205d500..64bbb56f2 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,7 +38,7 @@ namespace spot class SPOT_API bunop final : public formula { public: - enum type { Star }; + enum type { Star, FStar }; static const unsigned unbounded = -1U; @@ -50,9 +50,16 @@ namespace spot /// - 0[*0..max] = [*0] /// - 0[*min..max] = 0 if min > 0 /// - [*0][*min..max] = [*0] - /// - Exp[*0] = [*0] /// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. + /// - Exp[*0] = [*0] /// - Exp[*1] = Exp + /// - b[:*0..max] = 1 + /// - b[:*min..max] = b if min > 0 + /// - [*0][:*0..max] = 1 + /// - [*0][:*min..max] = 0 if min > 0 + /// - Exp[:*i..j][:*k..l] = Exp[:*ik..jl] if i*(k+1)<=jk+1. + /// - Exp[:*0] = 1 + /// - Exp[:*1] = Exp if Exp does not accept [*0] /// /// These rewriting rules imply that it is not possible to build /// an LTL formula object that is SYNTACTICALLY equal to one of diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 5284704c4..ae63baa5c 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -495,13 +495,19 @@ namespace spot v->swap(tmp); } } - else if (op == Concat) + else if (op == Concat || op == Fusion) { // 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] + // same for FStar: + // 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] + bunop::type bop = op == Concat ? bunop::Star : bunop::FStar; i = v->begin(); while (i != v->end()) { @@ -510,7 +516,7 @@ namespace spot unsigned min; unsigned max; bool changed = false; - if (const bunop* is = is_Star(*i)) + if (const bunop* is = is_bunop(*i, bop)) { f = is->child(); min = is->min(); @@ -528,7 +534,7 @@ namespace spot const formula* f2; unsigned min2; unsigned max2; - if (const bunop* is = is_Star(*i)) + if (const bunop* is = is_bunop(*i, bop)) { f2 = is->child(); if (f2 != f) @@ -558,7 +564,7 @@ namespace spot if (changed) { const formula* newfs = - bunop::instance(bunop::Star, f->clone(), min, max); + bunop::instance(bop, f->clone(), min, max); (*fpos)->destroy(); *fpos = newfs; } diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 89cd540e2..5e9dbff58 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -** Recherche et Développement de l'Epita (LRDE). +** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +** de Recherche et Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Université Pierre et Marie Curie. @@ -176,8 +176,11 @@ using namespace spot::ltl; %token OP_F "sometimes operator" OP_G "always operator" %token OP_X "next operator" OP_NOT "not operator" %token OP_STAR "star operator" OP_BSTAR "bracket star operator" +%token OP_BFSTAR "bracket fusion-star operator" %token OP_PLUS "plus operator" +%token OP_FPLUS "fusion-plus operator" %token OP_STAR_OPEN "opening bracket for star operator" +%token OP_FSTAR_OPEN "opening bracket for fusion-star operator" %token OP_EQUAL_OPEN "opening bracket for equal operator" %token OP_GOTO_OPEN "opening bracket for goto operator" %token OP_SQBKT_CLOSE "closing bracket" @@ -220,7 +223,9 @@ using namespace spot::ltl; %nonassoc OP_X /* High priority regex operator. */ -%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN +%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS + OP_BFSTAR OP_FSTAR_OPEN OP_FPLUS + OP_EQUAL_OPEN OP_GOTO_OPEN /* Not has the most important priority (after Wring's `=0' and `=1', but as those can only attach to atomic proposition, they do not @@ -229,7 +234,7 @@ using namespace spot::ltl; %type subformula booleanatom sere lbtformula boolformula %type bracedsere parenthesedsubformula -%type starargs equalargs sqbracketargs gotoargs +%type starargs fstarargs equalargs sqbracketargs gotoargs %destructor { delete $$; } %destructor { $$->destroy(); } @@ -370,6 +375,21 @@ starargs: kleen_star { error_list.emplace_back(@$, "missing closing bracket for star"); $$.min = $$.max = 0U; } +fstarargs: OP_BFSTAR + { $$.min = 0U; $$.max = bunop::unbounded; } + | OP_FPLUS + { $$.min = 1U; $$.max = bunop::unbounded; } + | OP_FSTAR_OPEN sqbracketargs + { $$ = $2; } + | OP_FSTAR_OPEN error OP_SQBKT_CLOSE + { error_list.emplace_back + (@$, "treating this fusion-star block as [:*]"); + $$.min = 0U; $$.max = bunop::unbounded; } + | OP_FSTAR_OPEN error_opt END_OF_INPUT + { error_list.emplace_back + (@$, "missing closing bracket for fusion-star"); + $$.min = $$.max = 0U; } + equalargs: OP_EQUAL_OPEN sqbracketargs { $$ = $2; } | OP_EQUAL_OPEN error OP_SQBKT_CLOSE @@ -507,15 +527,6 @@ sere: booleanatom { $$ = multop::instance(multop::Fusion, $1, $3); } | sere OP_FUSION error { missing_right_binop($$, $1, @2, "fusion operator"); } - | sere starargs - { - if ($2.max < $2.min) - { - error_list.emplace_back(@2, "reversed range"); - std::swap($2.max, $2.min); - } - $$ = bunop::instance(bunop::Star, $1, $2.min, $2.max); - } | starargs { if ($1.max < $1.min) @@ -526,6 +537,24 @@ sere: booleanatom $$ = bunop::instance(bunop::Star, constant::true_instance(), $1.min, $1.max); } + | sere starargs + { + if ($2.max < $2.min) + { + error_list.emplace_back(@2, "reversed range"); + std::swap($2.max, $2.min); + } + $$ = bunop::instance(bunop::Star, $1, $2.min, $2.max); + } + | sere fstarargs + { + if ($2.max < $2.min) + { + error_list.emplace_back(@2, "reversed range"); + std::swap($2.max, $2.min); + } + $$ = bunop::instance(bunop::FStar, $1, $2.min, $2.max); + } | sere equalargs { if ($2.max < $2.min) diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 0e014c0fa..ac07cd95f 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 2013, 2014, Laboratoire de +** Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, Laboratoire de ** Recherche et Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ** département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -224,6 +224,9 @@ eol2 (\n\r)+|(\r\n)+ "[*]" BEGIN(0); return token::OP_BSTAR; "[+]" BEGIN(0); return token::OP_PLUS; "[*" BEGIN(sqbracket); return token::OP_STAR_OPEN; +"[:*]" BEGIN(0); return token::OP_BFSTAR; +"[:+]" BEGIN(0); return token::OP_FPLUS; +"[:*" BEGIN(sqbracket); return token::OP_FSTAR_OPEN; "[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN; "["{ARROWL} BEGIN(sqbracket); return token::OP_GOTO_OPEN; "]" BEGIN(0); return token::OP_SQBKT_CLOSE; diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index 665e5ab98..4a8834d0a 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche et +# Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -181,6 +181,20 @@ G({1}<>->1), 1 {1[->10\,20];b}, {[*10..20];b} {1[->..];b}, {[*1..];b} {{a&!c}[->0];b}, b + +{(a|c)[:*0..3];d}, {1;d} +{(a|c)[:*1..3];d}, {(a|c);d} +{0[:*0..3];d}, {1;d} +{0[:*1..3];d}, 0 +{1[:*0..3];d}, {1;d} +{1[:*1..3];d}, {1;d} +{[*0][:*0..3];d}, {1;d} +{[*0][:*1..3];d}, 0 +{(a*;b|c)[:*1to3][:*2:4]}, {(a*;b|c)[:*2..12]} +{(a*;b|c)[:*][:+]}, {(a*;b|c)[:*]} +{(a*;b|c)[:*0]}, 1 +{(a*;b|c)[:*1]}, {(a*;b|c)} +{(a;b):(a;b):(a;b)[:*2]:(a;b):b*:b*:(c;d)[:*1]}, {(a;b)[:*5]:b*[:*2]:(c;d)} EOF diff --git a/src/ltltest/latex.test b/src/ltltest/latex.test index aa3188d9a..a3084d2a1 100755 --- a/src/ltltest/latex.test +++ b/src/ltltest/latex.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013 Laboratoire de Recherche et Développement +# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -35,6 +35,7 @@ a U b W c R (d & e) M f {a;b[=2];((c:d*) && f*);e[*2..]}<>-> {((a | [*0])*;b[+]) & (c1[->2])}[]-> h {a;b;c} []=> {d*;e} <>=> !f !{a;b*;c}! -> d +{a*;(b;c)[:*3..4];(c;d)[:+];d}! G(uglyname->Fuglierlongname42) EOF diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test index 59a0ad660..fa9095c85 100755 --- a/src/ltltest/rand.test +++ b/src/ltltest/rand.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -34,6 +34,8 @@ eword 1 boolform 1 star 1 star_b 1 +fstar 1 +fstar_b 1 and 0 andNLM 0 or 1 @@ -53,8 +55,11 @@ EOF diff stdout expected +sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0' +sere="$sere,or=0,concat=0,fstar=0,fstar_b=0" + run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \ - --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \ + --sere-p=$sere \ --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \ --dump-pr > stdout @@ -64,6 +69,8 @@ eword 0 boolform 1 star 0 star_b 0 +fstar 0 +fstar_b 0 and 0 andNLM 0 or 0 @@ -86,7 +93,7 @@ diff stdout expected # Disabling all operators will prevent more formulas to be generated. $randltl -S -n 10000 a b c --tree-size=10..20 \ - --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \ + --sere-p=$sere \ --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out && exit 1 sort out > out2 diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 9b6c06343..8d14dc618 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -308,7 +308,7 @@ namespace spot // SEREs random_sere::random_sere(const atomic_prop_set* ap) - : random_formula(9, ap), rb(ap) + : random_formula(11, ap), rb(ap) { proba_[0].setup("eword", 1, eword_builder); proba_2_ = proba_ + 1; @@ -316,11 +316,13 @@ namespace spot proba_[1].setup("boolform", 1, boolform_builder); proba_[2].setup("star", 2, bunop_unbounded_builder); proba_[3].setup("star_b", 2, bunop_bounded_builder); - proba_[4].setup("and", 3, multop_builder); - proba_[5].setup("andNLM", 3, multop_builder); - proba_[6].setup("or", 3, multop_builder); - proba_[7].setup("concat", 3, multop_builder); - proba_[8].setup("fusion", 3, multop_builder); + proba_[4].setup("fstar", 2, bunop_unbounded_builder); + proba_[5].setup("fstar_b", 2, bunop_bounded_builder); + proba_[6].setup("and", 3, multop_builder); + proba_[7].setup("andNLM", 3, multop_builder); + proba_[8].setup("or", 3, multop_builder); + proba_[9].setup("concat", 3, multop_builder); + proba_[10].setup("fusion", 3, multop_builder); update_sums(); } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 54e987a3b..d9945599b 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -1085,6 +1085,9 @@ namespace spot } result_ = bunop::instance(op, h, min, bo->max()); break; + case bunop::FStar: + result_ = bunop::instance(op, h, min, bo->max()); + break; } } @@ -3274,6 +3277,8 @@ namespace spot r->destroy(); f = 0; break; + case bunop::FStar: + goto common; } break; } diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index 624237a6c..3044c790f 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -70,6 +70,11 @@ namespace spot // Strip the star. result_ = recurse(bo->child()); break; + case bunop::FStar: + // FIXME: Can we deal with FStar in a better way? + result_ = bo->clone(); + break; + } } @@ -171,6 +176,9 @@ namespace spot std::max(bo->min(), 1U), bo->max()); break; + case bunop::FStar: + result_ = bo->clone(); + break; } } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index c5eb56ca1..bea663b7a 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE) +// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE) // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -71,6 +71,8 @@ namespace spot KCloseBunop, KStarBunop, KPlusBunop, + KFStarBunop, + KFPlusBunop, KEqualBunop, KGotoBunop, }; @@ -108,6 +110,8 @@ namespace spot "]", "[*", "[+]", + "[:*", + "[:+]", "[=", "[->", }; @@ -121,7 +125,7 @@ namespace spot " <-> ", // rewritten, although supported " U ", " V ", - " W ", // rewritten, although supported + " W ", // rewritten " M ", // rewritten "<>-> ", // not supported "<>=> ", // not supported @@ -145,6 +149,8 @@ namespace spot "]", // not supported "[*", // not supported "[+]", // not supported + "[:*", // not supported + "[:+]", // not supported "[=", // not supported "[->", // not supported }; @@ -182,6 +188,8 @@ namespace spot "]", // not supported "[*", // not supported "[+]", // not supported + "[:*", // not supported + "[:+]", // not supported "[=", // not supported "[->", // not supported }; @@ -219,6 +227,8 @@ namespace spot "]", "[*", "[+]", + "[:*", + "[:+]", "[=", "[->", }; @@ -256,6 +266,8 @@ namespace spot "}", "\\SereStar{", "\\SerePlus{}", + "\\SereFStar{", + "\\SereFPlus{}", "\\SereEqual{", "\\SereGoto{", }; @@ -297,6 +309,8 @@ namespace spot "}", "^{\\star", "^+", + "^{\\mathsf{:}\\star", + "^{\\mathsf{:}+}", "^{=", "^{\\to", }; @@ -577,17 +591,18 @@ namespace spot visit(const bunop* bo) { const formula* c = bo->child(); - enum { Star, Goto, Equal } sugar = Star; + enum { Star, FStar, Goto } sugar = Star; unsigned default_min = 0; unsigned default_max = bunop::unbounded; + bunop::type op = bo->op(); // Abbreviate "1[*]" as "[*]". - if (c != constant::true_instance()) + if (c != constant::true_instance() || op != bunop::Star) { - bunop::type op = bo->op(); switch (op) { case bunop::Star: + // Is this a Goto? if (const multop* mo = is_Concat(c)) { unsigned s = mo->size(); @@ -599,6 +614,9 @@ namespace spot } } break; + case bunop::FStar: + sugar = FStar; + break; } emit_bunop_child(c); @@ -616,8 +634,13 @@ namespace spot } emit(KStarBunop); break; - case Equal: - emit(KEqualBunop); + case FStar: + if (min == 1 && max == bunop::unbounded) + { + emit(KFPlusBunop); + return; + } + emit(KFStarBunop); break; case Goto: emit(KGotoBunop); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 148b55f1c..cd838df5f 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. @@ -708,20 +708,30 @@ namespace spot unsigned max = bo->max(); assert(max > 0); + bunop::type op = bo->op(); + // we will interpret + // c[*i..j] + // or c[:*i..j] + // as + // c;c[*i-1..j-1] + // or c:c[*i-1..j-1] + // \........../ + // this is f unsigned min2 = (min == 0) ? 0 : (min - 1); unsigned max2 = (max == bunop::unbounded) ? bunop::unbounded : (max - 1); + f = bunop::instance(op, bo->child()->clone(), min2, max2); + + // If we have something to append, we can actually append it + // to f. This is correct even in the case of FStar, as f + // cannot accept [*0]. + if (to_concat_) + f = multop::instance(multop::Concat, f, to_concat_->clone()); - bunop::type op = bo->op(); switch (op) { case bunop::Star: - f = bunop::instance(op, bo->child()->clone(), min2, max2); - - if (to_concat_) - f = multop::instance(multop::Concat, f, to_concat_->clone()); - if (!bo->child()->accepts_eword()) { // f*;g -> f;f*;g | g @@ -777,6 +787,57 @@ namespace spot res_ |= now_to_concat(); } return; + case bunop::FStar: + { + res_ = recurse(bo->child()); + bdd tail_bdd; + bool tail_computed = false; + + minato_isop isop(res_); + bdd cube; + res_ = bddfalse; + if (min == 0) + { + // f[:*0..j];g can be satisfied by X(g). + res_ = next_to_concat(); + } + while ((cube = isop.next()) != bddfalse) + { + bdd label = bdd_exist(cube, dict_.next_set); + bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); + + // The destination is a final state. Make sure we + // can also exit if tail is satisfied. We do not + // even have to check the tail if min == 0. + if (dest->accepts_eword() && min != 0) + { + if (!tail_computed) + { + tail_bdd = recurse(f); + tail_computed = true; + } + res_ |= label & tail_bdd; + } + + // If the destination is not 0 or [*0], it means it + // can have successors. Fusion the tail. + if (dest != constant::false_instance() + && dest != constant::empty_word_instance()) + { + const formula* dest2 = + multop::instance(multop::Fusion, dest, f->clone()); + if (dest2 != constant::false_instance()) + { + int x = dict_.register_next_variable(dest2); + dest2->destroy(); + res_ |= label & bdd_ithvar(x); + } + } + } + f->destroy(); + } + return; } SPOT_UNREACHABLE(); } @@ -961,8 +1022,8 @@ namespace spot // If the destination is not 0 or [*0], it means it // can have successors. Fusion the tail and append // anything to concatenate. - if (dest->kind() != formula::Constant - || dest == ltl::constant::true_instance()) + if (dest != constant::false_instance() + && dest != constant::empty_word_instance()) { const formula* dest2 = multop::instance(multop::Fusion, dest, tail->clone()); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 89fad6a68..fdcbf7435 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -202,6 +202,17 @@ grep 'states: 4$' stdout ../../bin/ltlfilt -f '{a[*];b[*]}' --equivalent-to 'a | b' ../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b' + +# A couple of tests for the [:*i..j] operator +../../bin/ltlfilt -q -f '{{a;b}[:*1..2];c}' \ + --equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))' +../../bin/ltlfilt -q -r -f '{{a;b}[:*1..2];c}' \ + --equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))' +../../bin/ltlfilt -q -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' +../../bin/ltlfilt -q -r -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' +../../bin/ltlfilt -q -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' +../../bin/ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' + # test unknown dot options ../../bin/ltl2tgba --dot=@ a 2>stderr && exit 1 grep 'ltl2tgba: unknown option.*@' stderr