diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 1f76bffd9..31d43fe2e 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -580,22 +580,6 @@ denote arbitrary SERE and $b$ denotes a Boolean formula. & $f\STAR{\mvar{i}:}$ & $f\STAR{\mvar{i} to}$ & $f\STAR{\mvar{i},}$\\ - bounded occurrence & $b\EQUAL{\mvar{i}..\mvar{j}}$ - & $b\EQUAL{\mvar{i}:\mvar{j}}$ - & $b\EQUAL{\mvar{i} to \mvar{j}}$ - & $b\EQUAL{\mvar{i},\mvar{j}}$\\ - unbounded occurrence & $b\EQUAL{\mvar{i}..}$ - & $b\EQUAL{\mvar{i}:}$ - & $b\EQUAL{\mvar{i} to}$ - & $b\EQUAL{\mvar{i},}$\\ - bounded goto & $b\GOTO{\mvar{i}..\mvar{j}}$ - & $b\GOTO{\mvar{i}:\mvar{j}}$ - & $b\GOTO{\mvar{i} to \mvar{j}}$ - & $b\GOTO{\mvar{i},\mvar{j}}$\\ - unbounded goto & $b\GOTO{\mvar{i}..}$ - & $b\GOTO{\mvar{i}:}$ - & $b\GOTO{\mvar{i} to}$ - & $b\GOTO{\mvar{i},}$\\ \end{tabular} \end{center} @@ -642,15 +626,7 @@ $b$ is a Boolean formula. \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 b\EQUAL{\mvar{i}..\mvar{j}} & \iff - \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\ - \sigma\VDash b\EQUAL{\mvar{i}..} & \iff - \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\ - \sigma\VDash b\GOTO{\mvar{i}..\mvar{j}} & \iff - \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\\ - \sigma\VDash b\GOTO{\mvar{i}..} & \iff - \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\\ + \end{cases} \end{align*}} Notes: @@ -667,9 +643,16 @@ operands are Boolean formul\ae. The syntax on the left is equivalent to the syntax on the right. These rewritings are performed from left to right when parsing a -formula, and some are performed from right to left when writing it for -output. +formula, and \emph{some} are performed from right to left when writing +it for output. $b$ must be a Boolean formula. +\begin{align*} + b\GOTO{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}} & + b\EQUAL{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..} \\ + b\GOTO{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..} & + b\EQUAL{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..}\text{~if~}i>0 \\ + && b\EQUAL{0..} &\equiv \mathtt{\{\{}\1\STAR{0..}\mathtt{\}} +\end{align*} \begin{align*} f\STARALT &\equiv f\STAR{0..}\\ f\STAR{} &\equiv f\STAR{0..} & @@ -701,22 +684,10 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae. \begin{align*} \0\STAR{0..\mvar{j}} &\equiv \eword & - \0\EQUAL{0..\mvar{j}} &\equiv \1\STAR{} & - \0\GOTO{0..\mvar{j}} &\equiv \eword \\ - \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 & - \0\EQUAL{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0& - \0\GOTO{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0\\ + \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\ \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword& - \1\EQUAL{0} &\equiv\eword& - \1\GOTO{0} &\equiv\eword\\ - f\STAR{0}&\equiv \eword & - \1\EQUAL{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}& - \1\GOTO{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}\\ - f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}& - b\EQUAL{0..}&\equiv 1\STAR{} & - b\GOTO{0}&\equiv \eword \\ - &\drsh\text{~if~}i(k+1)\le jk+1 & - b\EQUAL{0}&\equiv (\NOT b)\STAR{} \\ + 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 \end{align*} \noindent @@ -1396,16 +1367,6 @@ SERE. b \ANDALT r &\text{if~} i\le 1\le j\\ \0 &\text{else}\\ \end{cases}\\ - b \ANDALT r\EQUAL{\mvar{i}..\mvar{j}} &\equiv - \begin{cases} - b \ANDALT r &\text{if~} i\le 1\le j\\ - \0 &\text{else}\\ - \end{cases}\\ - b \ANDALT r\GOTO{\mvar{i}..\mvar{j}} &\equiv - \begin{cases} - b \ANDALT r &\text{if~} i\le 1\le j\\ - \0 &\text{else}\\ - \end{cases}\\ b \ANDALT \sere{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\ b \ANDALT \sere{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv \begin{cases} diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index b50bab04e..85b9b2e43 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -57,13 +57,6 @@ namespace spot if (min_ == 0) is.accepting_eword = true; break; - case Equal: - case Goto: - is.finite = false; - is.accepting_eword = (min_ == 0); - // Equal and Goto can only apply to Boolean formulae. - assert(child->is_boolean()); - break; } } @@ -140,12 +133,8 @@ namespace spot { switch (op_) { - case Equal: - return "Equal"; case Star: return "Star"; - case Goto: - return "Goto"; } // Unreachable code. assert(0); @@ -157,9 +146,6 @@ namespace spot { std::ostringstream out; - unsigned default_min = 0; - unsigned default_max = unbounded; - switch (op_) { case Star: @@ -171,39 +157,14 @@ namespace spot } out << "[*"; break; - case Equal: - out << "[="; - break; - case Goto: - out << "[->"; - default_min = 1; - default_max = 1; - break; } - // Beware that the default parameters of the Goto operator are - // not the same as Star or Equal: - // - // [->] = [->1..1] - // [->..] = [->1..unbounded] - // [*] = [*0..unbounded] - // [*..] = [*0..unbounded] - // [=] = [=0..unbounded] - // [=..] = [=0..unbounded] - // - // Strictly speaking [=] is not specified by PSL, and anyway we - // automatically rewrite Exp[=0..unbounded] as - // Exp[*0..unbounded], so we should never have to print [=] - // here. - // - // Also - // [*..] = [*0..unbounded] - - if (min_ != default_min || max_ != default_max) + 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 [*..3] near [*->..2]) + // when reading a[*..3];b[->..2] which actually + // means a[*0..3];b[->1..2]. out << min_; if (min_ != max_) { @@ -227,81 +188,6 @@ namespace spot switch (op) { - case Equal: - { - // - Exp[=0..] = [*] - if (min == 0 && max == unbounded) - { - op = Star; - child->destroy(); - child = constant::true_instance(); - break; - } - - // - 0[=0..max] = [*] - // - 0[=min..max] = 0 if min > 0 - if (child == constant::false_instance()) - { - if (min == 0) - { - max = unbounded; - op = Star; - child = constant::true_instance(); - break; - } - else - return child; - } - // - 1[=0] = [*0] - // - 1[=min..max] = 1[*min..max] - if (child == constant::true_instance()) - { - if (max == 0) - return constant::empty_word_instance(); - else - { - op = Star; - break; - } - } - // - Exp[=0] = (!Exp)[*] - if (max == 0) - return bunop::instance(bunop::Star, - unop::instance(unop::Not, child)); - break; - } - case Goto: - { - // - 0[->min..max] = 0 if min>0 - // - 0[->0..max] = [*0] - if (child == constant::false_instance()) - { - if (min == 0) - return constant::empty_word_instance(); - else - return child; - } - // - 1[->0] = [*0] - // - 1[->min..max] = 1[*min..max] - - if (child == constant::true_instance()) - { - if (max == 0) - return constant::empty_word_instance(); - else - { - op = Star; - break; - } - } - // - Exp[->0] = [*0] - if (max == 0) - { - child->destroy(); - return constant::empty_word_instance(); - } - break; - } case Star: { // - [*0][*min..max] = [*0] diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 3069ecd94..730983702 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -37,7 +37,7 @@ namespace spot class bunop : public ref_formula { public: - enum type { Star, Equal, Goto }; + enum type { Star }; static const unsigned unbounded = -1U; @@ -51,17 +51,6 @@ namespace spot /// - [*0][*min..max] = [*0] /// - Exp[*0] = [*0] /// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. - /// - 0[=0..max] = 1[*] - /// - 0[=min..max] = 0 if min > 0 - /// - 1[=0] = [*0] - /// - 1[=min..max] = 1[*min..max] - /// - Exp[=0..] = [*] - /// - Exp[=0] = (!Exp)[*] - /// - 0[->0..max] = [*0] - /// - 0[->min..max] = 0 if min>0 - /// - 1[->0] = [*0] - /// - 1[->min..max] = 1[*min..max] - /// - Exp[->0] = [*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/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 3310f8118..37e20514c 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -8,7 +8,7 @@ // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or +// the Free Software Foundation; either version 3 of the License, or // (at your option) any later version. // // Spot is distributed in the hope that it will be useful, but WITHOUT @@ -276,7 +276,7 @@ namespace spot // SEREs random_sere::random_sere(const atomic_prop_set* ap) - : random_formula(11, ap), rb(ap) + : random_formula(9, ap), rb(ap) { proba_[0].setup("eword", 1, eword_builder); proba_2_ = proba_ + 1; @@ -284,13 +284,11 @@ 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("equal_b", 2, bunop_bool_bounded_builder); - proba_[5].setup("goto_b", 2, bunop_bool_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); + 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); update_sums(); } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 38eaa507b..e77060668 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -5,7 +5,7 @@ // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or +// the Free Software Foundation; either version 3 of the License, or // (at your option) any later version. // // Spot is distributed in the hope that it will be useful, but WITHOUT @@ -2266,13 +2266,16 @@ namespace spot bunop* r = down_cast(*i); // b && r[*i..j] = b & r if i<=1<=j // = 0 otherwise - // likewise for b && r[=i..j] - // and b && r[->i..j] - if (r->min() > 1 || r->max() < 1) - goto returnfalse; - ares->push_back(r->child()->clone()); - r->destroy(); - *i = 0; + switch (r->op()) + { + case bunop::Star: + if (r->min() > 1 || r->max() < 1) + goto returnfalse; + ares->push_back(r->child()->clone()); + r->destroy(); + *i = 0; + break; + } break; } case formula::MultOp: @@ -2540,7 +2543,7 @@ namespace spot fset_t xfset; // XF(...) fset_t xset; // X(...) fmap_t rmset; // (X...)R(...) or (X...)M(...) or - // b & X(b W ...) or b & X(b U ...) + // b & X(b W ...) or b & X(b U ...) unsigned s = res->size(); std::vector tokill(s); diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index d50685bc0..88ab06a33 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -385,12 +385,6 @@ namespace spot } } break; - case bunop::Goto: - sugar = Goto; - break; - case bunop::Equal: - sugar = Equal; - break; } emit_bunop_child(c); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b732d0e58..2c4eb233f 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -548,71 +548,6 @@ namespace spot res_ |= now_to_concat(); } return; - case bunop::Equal: - { - // b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1]) - // b[=0..max] == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1]) - // Note: b[=0] == (!b)[*] is a trivial identity, so it will - // never occur here. - formula* f1 = // !b;b[=min..max] or !b;b[->min..max] - multop::instance(multop::Concat, - unop::instance(unop::Not, - bo->child()->clone()), - bo->clone()); - - formula* f2 = // b;b[=min-1..max-1] or b;b[->min-1..max-1] - multop::instance(multop::Concat, - bo->child()->clone(), - bunop::instance(op, - bo->child()->clone(), - min2, max2)); - f = multop::instance(multop::Or, f1, f2); - res_ = recurse_and_concat(f); - f->destroy(); - if (min == 0) - res_ |= now_to_concat(); - return; - } - case bunop::Goto: - { - // It is important to understand why we do not define Goto - // similarly to equal, i.e.: - // - // b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1]) - // b[->0..max] == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1]) - // Note: b[->0] == [*0] is a trivial identity, so it will - // never occur here. - // - // The above would be wrong when min=0. - // For instance consider {(c&!c)[->0..1]}<>->1 - // This formula is equivalent to {[*0]}<>->1 which is false. - // However with above above rewritings, we get - // {[*0] | !(c&!c);(c&!c)[->0..1] | (c&!c);(c&!c)[->0] }<>->1 - // which is equivalent to { 1;[*0] }<>-> 1 which is true. Oops! - // - // We therefore use the following rules instead: - // b[->min..max] == (!b)[*];b;b[->min-1..max-1] - // b[->0..max] == [*0] | (!b)[*];b;b[->min-1..max-1] - - formula* f1 = // (!b)[*] - bunop::instance(bunop::Star, - unop::instance(unop::Not, - bo->child()->clone()), - 0, bunop::unbounded); - formula* f2 = // b;b[->min-1..max-1] - multop::instance(multop::Concat, - bo->child()->clone(), - bunop::instance(op, - bo->child()->clone(), - min2, max2)); - f = multop::instance(multop::Concat, f1, f2); - res_ = recurse_and_concat(f); - f->destroy(); - if (min == 0) - res_ |= now_to_concat(); - return; - } - } /* Unreachable code. */ assert(0);