diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 8763e446c..e1116a09f 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 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), @@ -34,6 +34,17 @@ namespace spot atomic_prop::atomic_prop(const std::string& name, environment& env) : name_(name), env_(&env) { + is.boolean = true; + is.sugar_free_boolean = true; + is.in_nenoform = true; + is.X_free = true; + is.sugar_free_ltl = true; + is.ltl_formula = true; + is.eltl_formula = true; + is.psl_formula = true; + is.eventual = false; + is.universal = false; + is.not_marked = true; } atomic_prop::~atomic_prop() diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 34093c944..4b616c441 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Developpement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -30,6 +30,21 @@ namespace spot automatop::automatop(const nfa::ptr nfa, vec* v, bool negated) : nfa_(nfa), children_(v), negated_(negated) { + is.boolean = false; + is.sugar_free_boolean = true; + is.in_nenoform = true; + is.X_free = true; + is.sugar_free_ltl = true; + is.ltl_formula = false; + is.eltl_formula = true; + is.psl_formula = false; + is.eventual = false; + is.universal = false; + is.not_marked = true; + + unsigned s = v->size(); + for (unsigned i = 0; i < s; ++i) + props &= (*v)[i]->get_props(); } automatop::~automatop() diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index b2c8391d8..1735ffa55 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -36,6 +36,65 @@ namespace spot binop::binop(type op, formula* first, formula* second) : op_(op), first_(first), second_(second) { + // Beware: (f U g) is purely eventual if both operands + // are purely eventual, unlike in the proceedings of + // Concur'00. (The revision of the paper available at + // http://www.bell-labs.com/project/TMP/ is fixed.) See + // also http://arxiv.org/abs/1011.4214 for a discussion + // about this problem. (Which we fixed in 2005 thanks + // to LBTT.) + + // This means that we can use the following line to handle + // all cases of (f U g), (f R g), (f W g), (f M g) for + // universality and eventuality. + props = first->get_props() & second->get_props(); + + switch (op) + { + case Xor: + case Implies: + case Equiv: + is.sugar_free_boolean = false; + is.in_nenoform = false; + break; + case EConcatMarked: + is.not_marked = false; + // fall through + case EConcat: + case UConcat: + is.ltl_formula = false; + is.boolean = false; + is.eltl_formula = false; + break; + case U: + // 1 U a = Fa + if (first == constant::true_instance()) + is.eventual = 1; + is.boolean = false; + is.eltl_formula = false; + break; + case W: + // a W 0 = Ga + if (second == constant::false_instance()) + is.universal = 1; + is.boolean = false; + is.eltl_formula = false; + break; + case R: + // 0 R a = Ga + if (first == constant::false_instance()) + is.universal = 1; + is.boolean = false; + is.eltl_formula = false; + break; + case M: + // a M 1 = Fa + if (second == constant::true_instance()) + is.eventual = 1; + is.boolean = false; + is.eltl_formula = false; + break; + } } binop::~binop() diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 19539c97f..733c8c487 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -25,7 +25,6 @@ #include #include "constant.hh" #include "unop.hh" -#include "ltlvisit/kind.hh" namespace spot { @@ -34,6 +33,20 @@ namespace spot bunop::bunop(type op, formula* child, unsigned min, unsigned max) : op_(op), child_(child), min_(min), max_(max) { + props = child->get_props(); + + switch (op_) + { + case Equal: + case Star: + case Goto: + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.eventual = false; + is.universal = false; + break; + } } bunop::~bunop() diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 96025c3bf..df15547e5 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -36,6 +36,36 @@ namespace spot constant::constant(type val) : val_(val) { + switch (val) + { + case constant::True: + case constant::False: + is.boolean = true; + is.sugar_free_boolean = true; + is.in_nenoform = true; + is.X_free = true; + is.sugar_free_ltl = true; + is.ltl_formula = true; + is.eltl_formula = true; + is.psl_formula = true; + is.eventual = true; + is.universal = true; + is.not_marked = true; + break; + case constant::EmptyWord: + is.boolean = false; + is.sugar_free_boolean = false; + is.in_nenoform = true; + is.X_free = true; + is.sugar_free_ltl = true; + is.ltl_formula = false; + is.eltl_formula = false; + is.psl_formula = true; + is.eventual = false; + is.universal = false; + is.not_marked = true; + break; + } } constant::~constant() diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 123ebcd2d..4033a1d9c 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -23,6 +23,7 @@ #include "formula.hh" #include "misc/hash.hh" +#include namespace spot { @@ -60,5 +61,32 @@ namespace spot // Not reference counted by default. return false; } + + std::ostream& + print_formula_props(std::ostream& out, const formula* f, bool abbr) + { + const char* comma = abbr ? "" : ", "; + const char* sep = ""; + +#define proprint(m, a, l) \ + if (f->m()) \ + { \ + out << sep; out << (abbr ? a : l); \ + sep = comma; \ + } + + proprint(is_boolean, "B", "Boolean formula"); + proprint(is_sugar_free_boolean, "&", "without Boolean sugar"); + proprint(is_in_nenoform, "!", "in negative normal form"); + proprint(is_X_free, "x", "without X operator"); + proprint(is_sugar_free_ltl, "f", "without LTL sugar"); + proprint(is_ltl_formula, "L", "LTL formula"); + proprint(is_eltl_formula, "E", "ELTL formula"); + proprint(is_psl_formula, "P", "PSL formula"); + proprint(is_eventual, "e", "pure eventuality"); + proprint(is_universal, "u", "purely universal"); + proprint(is_marked, "+", "marked"); + return out; + } } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index ece1135ca..f221239e8 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -100,6 +100,123 @@ namespace spot /// Return a canonic representation of the formula virtual std::string dump() const = 0; + //////////////// + // Properties // + //////////////// + + /// Whether the formula use only boolean operators. + bool is_boolean() const + { + return is.boolean; + } + + /// Whether the formula use only AND, OR, and NOT operators. + bool is_sugar_free_boolean() const + { + return is.sugar_free_boolean; + } + + /// \brief Whether the formula is in negative normal form. + /// + /// A formula is in negative normal form if the not operators + /// occur only in front of atomic propositions. + bool is_in_nenoform() const + { + return is.in_nenoform; + } + + /// Whether the formula avoid the X operator. + bool is_X_free() const + { + return is.X_free; + } + + /// Whether the formula avoid the F and G operators. + bool is_sugar_free_ltl() const + { + return is.sugar_free_ltl; + } + + /// Whether the formula use only LTL operators. + bool is_ltl_formula() const + { + return is.ltl_formula; + } + + /// Whether the formula use only ELTL operators. + bool is_eltl_formula() const + { + return is.eltl_formula; + } + + /// Whether the formula use only PSL operators. + bool is_psl_formula() const + { + return is.psl_formula; + } + + /// \brief Whether the formula is purely eventual. + /// + /// Pure eventuality formulae are defined in + /// \verbatim + /// @InProceedings{ etessami.00.concur, + /// author = {Kousha Etessami and Gerard J. Holzmann}, + /// title = {Optimizing {B\"u}chi Automata}, + /// booktitle = {Proceedings of the 11th International Conference on + /// Concurrency Theory (Concur'2000)}, + /// pages = {153--167}, + /// year = {2000}, + /// editor = {C. Palamidessi}, + /// volume = {1877}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + /// + /// A word that satisfies a pure eventuality can be prefixed by + /// anything and still satisfies the formula. + bool is_eventual() const + { + return is.eventual; + } + + /// \brief Whether a formula is purely universal. + /// + /// Purely universal formulae are defined in + /// \verbatim + /// @InProceedings{ etessami.00.concur, + /// author = {Kousha Etessami and Gerard J. Holzmann}, + /// title = {Optimizing {B\"u}chi Automata}, + /// booktitle = {Proceedings of the 11th International Conference on + /// Concurrency Theory (Concur'2000)}, + /// pages = {153--167}, + /// year = {2000}, + /// editor = {C. Palamidessi}, + /// volume = {1877}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + /// + /// Any (non-empty) suffix of a word that satisfies a purely + /// universal formula also satisfies the formula. + bool is_universal() const + { + return is.universal; + } + + /// Whether the formula has an occurrence of EConcatMarked. + bool is_marked() const + { + return !is.not_marked; + } + + /// The properties as a field of bits. For internal use. + unsigned get_props() const + { + return props; + } + /// Return a hash key for the formula. size_t hash() const @@ -118,6 +235,40 @@ namespace spot /// \brief The hash key of this formula. size_t count_; + struct ltl_prop + { + // All properties here should be expressed in such a a way + // that property(f && g) is just property(f)&property(g). + // This allows us to compute all properties of a compound + // formula in one operation. + // + // For instance we do not use a property that says "has + // temporal operator", because it would require an OR between + // the two arguments. Instead we have a property that + // says "no temporal operator", and that one is computed + // with an AND between the arguments. + // + // Also choose a name that makes sense when prefixed with + // "the formula is". + bool boolean:1; // No temporal operators. + bool sugar_free_boolean:1; // Only AND, OR, and NOT operators. + bool in_nenoform:1; // Negative Normal Form + bool X_free:1; // No X operators. + bool sugar_free_ltl:1; // No F and G operators. + bool ltl_formula:1; // Only LTL operators. + bool eltl_formula:1; // Only ELTL operators. + bool psl_formula:1; // Only PSL operators. + bool eventual:1; // Purely eventual formula. + bool universal:1; // Purely universal formula. + bool not_marked:1; // No occurrence of EConcatMarked + }; + union + { + // Use an unsigned for fast computation of all properties. + unsigned props; + ltl_prop is; + }; + private: /// \brief Number of formulae created so far. static size_t max_count; @@ -189,6 +340,10 @@ namespace spot } }; + /// Print the properties of formula \a f on stream \a out. + std::ostream& print_formula_props(std::ostream& out, + const formula* f, + bool abbreviated = false); } } diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index ed0d19d83..84bedeba4 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -37,6 +37,32 @@ namespace spot multop::multop(type op, vec* v) : op_(op), children_(v) { + unsigned s = v->size(); + assert(s > 1); + + props = (*v)[0]->get_props(); + for (unsigned i = 1; i < s; ++i) + props &= (*v)[i]->get_props(); + + switch (op) + { + case Concat: + case Fusion: + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.eventual = false; + is.universal = false; + break; + case AndNLM: + // The non-matching-length-And (&) can only appear in the + // rational parts of PSL formula. We don't remove the + // Boolean flag, because applied to atomic propositions a&b + // has the same effect as a&&b. + case And: + case Or: + break; + } } multop::~multop() diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index d8ac2977c..b19880000 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -26,6 +26,7 @@ #include #include #include "constant.hh" +#include "atomic_prop.hh" namespace spot { @@ -34,6 +35,41 @@ namespace spot unop::unop(type op, formula* child) : op_(op), child_(child) { + props = child->get_props(); + switch (op) + { + case Not: + is.in_nenoform = !!dynamic_cast(child); + break; + case X: + is.boolean = false; + is.X_free = false; + is.eltl_formula = false; + break; + case F: + is.boolean = false; + is.eltl_formula = false; + is.sugar_free_ltl = false; + is.eventual = true; + break; + case G: + is.boolean = false; + is.eltl_formula = false; + is.sugar_free_ltl = false; + is.universal = true; + break; + case Finish: + is.boolean = false; + is.ltl_formula = false; + is.psl_formula = false; + break; + case Closure: + case NegClosure: + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + break; + } } unop::~unop() diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 45b169f28..4a18dc350 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -35,7 +35,6 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/kind.hh" struct minmax_t { unsigned min, max; }; } @@ -367,7 +366,7 @@ rationalexp: booleanatom $1.min, $1.max); } | rationalexp equalargs { - if ((kind_of($1) & Boolean_Kind) == Boolean_Kind) + if ($1->is_boolean()) { $$ = bunop::instance(bunop::Equal, $1, $2.min, $2.max); } @@ -384,7 +383,7 @@ rationalexp: booleanatom } | rationalexp gotoargs { - if ((kind_of($1) & Boolean_Kind) == Boolean_Kind) + if ($1->is_boolean()) { $$ = bunop::instance(bunop::Goto, $1, $2.min, $2.max); } diff --git a/src/ltltest/kind.cc b/src/ltltest/kind.cc index 04b8c5ca2..434765624 100644 --- a/src/ltltest/kind.cc +++ b/src/ltltest/kind.cc @@ -22,7 +22,6 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/kind.hh" #include "ltlast/allnodes.hh" void @@ -44,9 +43,8 @@ main(int argc, char **argv) if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; - unsigned k = spot::ltl::kind_of(f1); - spot::ltl::print_kind(std::cout, k, true) << " = "; - spot::ltl::print_kind(std::cout, k, false) << std::endl; + spot::ltl::print_formula_props(std::cout, f1, true) << " = "; + spot::ltl::print_formula_props(std::cout, f1, false) << std::endl; f1->destroy(); assert(spot::ltl::atomic_prop::instance_count() == 0); diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 4befe04b9..442625be1 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -37,12 +37,18 @@ check 'a' 'B&!xfLEP' check 'a<->b' 'BxfLEP' check '!a' 'B&!xfLEP' check '!(a|b)' 'B&xfLEP' +check 'F(a)' '&!xLPe' +check 'G(a)' '&!xLPu' check 'a U b' '&!xfLP' check 'a U Fb' '&!xLP' check 'Ga U b' '&!xLP' +check '1 U a' '&!xfLPe' check 'a W b' '&!xfLP' +check 'a W 0' '&!xfLPu' check 'a M b' '&!xfLP' +check 'a M 1' '&!xfLPe' check 'a R b' '&!xfLP' +check '0 R b' '&!xfLPu' check '{a}|->!Xb' '&fP' check '{a}|->X!b' '&!fP' check '{a}|->!Gb' '&xP' diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 813894805..186d1d286 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -35,7 +35,6 @@ ltlvisit_HEADERS = \ destroy.hh \ dotty.hh \ dump.hh \ - kind.hh \ length.hh \ lunabbrev.hh \ mark.hh \ @@ -58,7 +57,6 @@ libltlvisit_la_SOURCES = \ destroy.cc \ dotty.cc \ dump.cc \ - kind.cc \ length.cc \ lunabbrev.cc \ mark.cc \ diff --git a/src/ltlvisit/kind.cc b/src/ltlvisit/kind.cc deleted file mode 100644 index cd2fe378c..000000000 --- a/src/ltlvisit/kind.cc +++ /dev/null @@ -1,229 +0,0 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// 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 -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "kind.hh" -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" -#include - -namespace spot -{ - namespace ltl - { - namespace - { - - class kind_visitor : public visitor - { - unsigned result_; - public: - kind_visitor() - : result_(All_Kind) - { - } - ~kind_visitor() - { - } - - unsigned - result() - { - return result_; - } - - void - visit(atomic_prop*) - { - } - - void - visit(constant* c) - { - if (c == constant::empty_word_instance()) - result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); - } - - void - visit(bunop* bo) - { - result_ = recurse(bo->child()); - result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); - } - - void - visit(unop* uo) - { - result_ = recurse(uo->child()); - - switch (uo->op()) - { - case unop::NegClosure: - case unop::Closure: - result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); - return; - case unop::Finish: - result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind); - return; - case unop::Not: - if (!dynamic_cast(uo->child())) - result_ &= ~NeNoForm_Kind; - return; - case unop::X: - result_ &= ~(Boolean_Kind | No_X_Kind | ELTL_Kind); - return; - case unop::F: - case unop::G: - result_ &= ~(Boolean_Kind | SugarFree_LTL_Kind | ELTL_Kind); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(automatop* ao) - { - unsigned aos = ao->size(); - for (unsigned i = 0; i < aos && !result_; ++i) - result_ &= recurse(ao->nth(i)); - - result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind); - } - - void - visit(multop* mo) - { - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos && !result_; ++i) - result_ &= recurse(mo->nth(i)); - - switch (mo->op()) - { - case multop::Or: - case multop::And: - return; - case multop::AndNLM: - // The non-matching-length-And (&) can only appear - // in the rational parts of PSL formula. We - // don't remove the Boolean_Kind flags, because - // applied to atomic propositions a&b has the same - // effect as a&&b. - result_ &= ~(LTL_Kind | ELTL_Kind); - return; - case multop::Concat: - case multop::Fusion: - result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); - return; - } - } - - void - visit(binop* bo) - { - result_ = recurse(bo->first()) & recurse(bo->second()); - - switch (bo->op()) - { - case binop::EConcatMarked: - case binop::UConcat: - case binop::EConcat: - result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); - return; - case binop::Xor: - case binop::Implies: - case binop::Equiv: - result_ &= ~(NeNoForm_Kind | SugarFree_Boolean_Kind); - return; - case binop::U: - case binop::W: - case binop::M: - case binop::R: - result_ &= ~(Boolean_Kind | ELTL_Kind); - return; - } - /* Unreachable code. */ - assert(0); - } - - unsigned - recurse(const formula* f) - { - return kind_of(f); - } - }; - } - - unsigned - kind_of(const formula* f) - { - kind_visitor v; - const_cast(f)->accept(v); - return v.result(); - } - - - - std::ostream& - print_kind(std::ostream& o, unsigned k, bool abbreviated) - { - struct data { char abbrev; const char* name; }; - static const data kind_name[] = - { - {'B', "Boolean formula"}, // 1 - {'&', "no sugar Boolean operator"}, // 2 - {'!', "in negative normal form"}, // 4 - {'x', "no X LTL operator"}, // 8 - {'f', "no sugar LTL operator"}, // 16 - {'L', "LTL formula"}, // 32 - {'E', "ELTL formula"}, // 64 - {'P', "PSL formula"}, // 128 - }; - const char* comma = ""; - unsigned size = (sizeof kind_name)/(sizeof *kind_name); - for (unsigned i = 0; i < size; ++i) - { - if ((k & 1)) - { - if (abbreviated) - { - o << kind_name[i].abbrev; - } - else - { - o << comma << kind_name[i].name; - comma = ", "; - } - } - k >>= 1; - } - return o; - } - - - std::ostream& - print_kind(std::ostream& o, const formula* f, bool abbreviated) - { - print_kind(o, kind_of(f), abbreviated); - return o; - } - - - } -} diff --git a/src/ltlvisit/kind.hh b/src/ltlvisit/kind.hh deleted file mode 100644 index d984ffa70..000000000 --- a/src/ltlvisit/kind.hh +++ /dev/null @@ -1,69 +0,0 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// 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 -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#ifndef SPOT_LTLVISIT_KIND_HH -# define SPOT_LTLVISIT_KIND_HH - -#include "ltlast/predecl.hh" -#include - -namespace spot -{ - namespace ltl - { - /// Different kinds or proporties of formulae. - // If you change this list, you have to adjust - // the kind_name array in print_kind() (kind.cc) - enum kind - { - Boolean_Kind = 1, - SugarFree_Boolean_Kind = 2, - NeNoForm_Kind = 4, - No_X_Kind = 8, - SugarFree_LTL_Kind = 16, - LTL_Kind = 32, - ELTL_Kind = 64, - PSL_Kind = 128, - All_Kind = -1U, - }; - - - /// \brief Compute properties of a formula. - /// \ingroup ltl_visitor - /// - /// Return a sum of ltl::kind values depending on the operators - /// used by a formula. - /// - /// \param f The formula to analyze. - unsigned kind_of(const formula* f); - - /// \brief Print a ltl::kind (computed by kind_of()). - /// \ingroup ltl_visitor - std::ostream& print_kind(std::ostream& o, unsigned k, - bool abbreviated = false); - - /// \brief Print the properties of a formula. - /// \ingroup ltl_visitor - std::ostream& print_kind(std::ostream& o, const formula* f, - bool abbreviated = false); - } -} - -#endif // SPOT_LTLVISIT_KIND_HH diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 66cb9fa85..9821705f2 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -38,168 +38,6 @@ namespace spot { namespace { - typedef union - { - unsigned v; - struct is_struct - { - bool eventual:1; - bool universal:1; - } is; - } eu_info; - - static unsigned recurse_eu(const formula* f); - - class eventual_universal_visitor: public const_visitor - { - public: - - eventual_universal_visitor() - { - } - - virtual - ~eventual_universal_visitor() - { - } - - bool - is_eventual() const - { - return ret_.is.eventual; - } - - bool - is_universal() const - { - return ret_.is.universal; - } - - unsigned - eu() const - { - return ret_.v; - } - - void - visit(const atomic_prop*) - { - ret_.v = 0; - } - - void - visit(const constant*) - { - ret_.v = 0; - } - - void - visit(const bunop*) - { - ret_.v = 0; - } - - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - if (uo->op() == unop::F) - { - ret_.v = recurse_eu(f1); - ret_.is.eventual = true; - return; - } - if (uo->op() == unop::G) - { - ret_.v = recurse_eu(f1); - ret_.is.universal = true; - return; - } - ret_.v = 0; - return; - } - - void - visit(const binop* bo) - { - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - - // Beware: (f U g) is purely eventual if both operands - // are purely eventual, unlike in the proceedings of - // Concur'00. (The revision of the paper available at - // http://www.bell-labs.com/project/TMP/ is fixed.) See - // also http://arxiv.org/abs/1011.4214 for a discussion - // about this problem. (Which we fixed in 2005 thanks - // to LBTT.) - - // This means that we can use the following case to handle - // all cases of (f U g), (f R g), (f W g), (f M g) for - // universality and eventuality. - ret_.v = recurse_eu(f1) & recurse_eu(f2); - - // we are left with the case where U, R, W, or M are actually - // used to represent F or G. - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - return; - case binop::U: - if (f1 == constant::true_instance()) - ret_.is.eventual = true; - return; - case binop::W: - if (f2 == constant::true_instance()) - ret_.is.eventual = true; - return; - case binop::R: - if (f1 == constant::false_instance()) - ret_.is.universal = true; - return; - case binop::M: - if (f2 == constant::false_instance()) - ret_.is.universal = true; - return; - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const automatop*) - { - assert(0); - } - - void - visit(const multop* mo) - { - unsigned mos = mo->size(); - assert(mos != 0); - ret_.v = recurse_eu(mo->nth(0)); - for (unsigned i = 1; i < mos && ret_.v != 0; ++i) - ret_.v &= recurse_eu(mo->nth(i)); - } - - private: - eu_info ret_; - }; - - static unsigned - recurse_eu(const formula* f) - { - eventual_universal_visitor v; - const_cast(f)->accept(v); - return v.eu(); - } - - ///////////////////////////////////////////////////////////////////////// class reduce_visitor: public visitor @@ -251,14 +89,14 @@ namespace spot case unop::F: /* If f is a pure eventuality formula then F(f)=f. */ if (!(opt_ & Reduce_Eventuality_And_Universality) - || !is_eventual(result_)) + || !result_->is_eventual()) result_ = unop::instance(unop::F, result_); return; case unop::G: /* If f is a pure universality formula then G(f)=f. */ if (!(opt_ & Reduce_Eventuality_And_Universality) - || !is_universal(result_)) + || !result_->is_universal()) result_ = unop::instance(unop::G, result_); return; @@ -280,14 +118,13 @@ namespace spot binop::type op = bo->op(); formula* f2 = recurse(bo->second()); - eu_info f2i = { recurse_eu(f2) }; if (opt_ & Reduce_Eventuality_And_Universality) { /* If b is a pure eventuality formula then a U b = b. If b is a pure universality formula a R b = b. */ - if ((f2i.is.eventual && (op == binop::U)) - || (f2i.is.universal && (op == binop::R))) + if ((f2->is_eventual() && (op == binop::U)) + || (f2->is_universal() && (op == binop::R))) { result_ = f2; return; @@ -295,17 +132,16 @@ namespace spot } formula* f1 = recurse(bo->first()); - eu_info f1i = { recurse_eu(f1) }; if (opt_ & Reduce_Eventuality_And_Universality) { /* If a is a pure eventuality formula then a M b = a & b. If a is a pure universality formula a W b = a|b. */ - if (f1i.is.eventual && (op == binop::M)) + if (f1->is_eventual() && (op == binop::M)) { result_ = multop::instance(multop::And, f1, f2); return; } - if (f1i.is.universal && (op == binop::W)) + if (f1->is_universal() && (op == binop::W)) { result_ = multop::instance(multop::Or, f1, f2); return; @@ -639,17 +475,13 @@ namespace spot bool is_eventual(const formula* f) { - eventual_universal_visitor v; - const_cast(f)->accept(v); - return v.is_eventual(); + return f->is_eventual(); } bool is_universal(const formula* f) { - eventual_universal_visitor v; - const_cast(f)->accept(v); - return v.is_universal(); + return f->is_universal(); } } } diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index 3c6fcf850..33326770b 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -82,7 +82,13 @@ namespace spot /// /// A word that satisfies a pure eventuality can be prefixed by /// anything and still satisfies the formula. + /// + /// \deprecated Use f->is_eventual() instead. +#if __GNUC__ + bool is_eventual(const formula* f) __attribute__ ((deprecated)); +#else bool is_eventual(const formula* f); +#endif /// \brief Check whether a formula is purely universal. /// \ingroup ltl_misc @@ -105,7 +111,13 @@ namespace spot /// /// Any (non-empty) suffix of a word that satisfies if purely /// universal formula also satisfies the formula. + /// + /// \deprecated Use f->is_universal() instead. +#if __GNUC__ + bool is_universal(const formula* f) __attribute__ ((deprecated)); +#else bool is_universal(const formula* f); +#endif } }