From 546559b8c3d05a11a0847b1df823e13dc7210fca Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Jan 2010 14:29:46 +0100 Subject: [PATCH] Introduce rational operators and trivial simplification rules. Trivial simplifications rules (such as "FFa=Fa" or "x&1=x") are performed any time a formule is instanciated. * src/ltlast/constant.hh, src/ltlast/constant.cc (true_instance, true_instance_): Declare the true_instance_ as a static member, and move true_instance() into the .hh so it gets inlined. Have true_instance_ as a class variable will ensure that it is the first formula instantiated. Binop simplifications rely on this to order arguments. (false_instance, false_instance_): Likewise. (empty_word_instance, empty_word_instance_): New method and static member. * src/ltlast/formula.hh (formula::formula): If max_count_ ever loops, skip the first three values so that constants always have smaller hash codes. * src/ltlast/binop.hh, src/ltlast/binop.cc (instance): Add simplifications and document them. * src/ltlast/multop.hh (multop::Concat): New operator. * src/ltlast/multop.cc (op_name): Handle Concat. (instance): Inline Concat arguments without reordering. Handle absorbent and neutral elements for all operators. * src/ltlast/unop.hh (unop::Star): New operator. * src/ltlast/unop.cc (op_name): Handle Star. (instance): Handle Star, and add trivial simplifications for other unary operators. * src/ltlparse/ltlparse.yy (OP_CONCAT, OP_STAR, CONST_EMPTYWORD): Declare these new operators and add rules for them. * src/ltlparse/ltlscan.ll (OP_CONCAT, OP_STAR, CONST_EMPTYWORD): Output these new operators. * src/ltltest/equals.test: New tests. * src/ltltest/parse.test: Remove redundant test. * src/ltltest/tunabbrev.test, src/tgbatest/emptchk.test: Adjust tests. * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc: Complete visitors to handle new operators. * src/ltltest/nenoform.test: More tests. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::visit): Clone formulae before instance() function actually have a chance to destroy them. * src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Adjust switches to assert on new operators. --- src/ltlast/binop.cc | 114 +++++++++++++++++++++++++++++-- src/ltlast/binop.hh | 32 ++++++++- src/ltlast/constant.cc | 28 +++----- src/ltlast/constant.hh | 18 +++-- src/ltlast/formula.hh | 14 ++-- src/ltlast/multop.cc | 37 +++++++--- src/ltlast/multop.hh | 47 ++++++++----- src/ltlast/unop.cc | 80 ++++++++++++++++++++-- src/ltlast/unop.hh | 41 +++++++++-- src/ltlparse/ltlparse.yy | 17 ++++- src/ltlparse/ltlscan.ll | 6 +- src/ltltest/equals.test | 48 ++++++++++++- src/ltltest/nenoform.test | 9 ++- src/ltltest/parse.test | 4 +- src/ltltest/tunabbrev.test | 9 +-- src/ltlvisit/basicreduce.cc | 17 +++-- src/ltlvisit/contain.cc | 2 + src/ltlvisit/lunabbrev.cc | 40 ++++++----- src/ltlvisit/nenoform.cc | 33 +++++++-- src/ltlvisit/reduce.cc | 8 ++- src/ltlvisit/syntimpl.cc | 38 ++++++++--- src/ltlvisit/tostring.cc | 20 ++++++ src/ltlvisit/tunabbrev.cc | 3 +- src/tgba/formula2bdd.cc | 5 ++ src/tgbaalgos/eltl2tgba_lacim.cc | 5 ++ src/tgbaalgos/ltl2taa.cc | 8 +++ src/tgbaalgos/ltl2tgba_fm.cc | 5 ++ src/tgbaalgos/ltl2tgba_lacim.cc | 5 ++ src/tgbatest/emptchk.test | 2 +- 29 files changed, 575 insertions(+), 120 deletions(-) diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 91edc7a5f..915a11db8 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -24,6 +24,8 @@ #include #include #include "binop.hh" +#include "unop.hh" +#include "constant.hh" #include "visitor.hh" #include @@ -127,25 +129,127 @@ namespace spot binop::map binop::instances; - binop* + formula* binop::instance(type op, formula* first, formula* second) { // Sort the operands of commutative operators, so that for // example the formula instance for 'a xor b' is the same as // that for 'b xor a'. + + /// Trivial identities: switch (op) { case Xor: + { + // Xor is commutative: sort operands. + formula_ptr_less_than cmp; + if (cmp(second, first) > 0) + std::swap(first, second); + } + // - (1 ^ Exp) = !Exp + // - (0 ^ Exp) = Exp + if (first == constant::true_instance()) + return unop::instance(unop::Not, second); + if (first == constant::false_instance()) + return second; + // We expect constants to appear first, because they are + // instantiated first. + assert(second != constant::false_instance()); + assert(second != constant::true_instance()); + break; case Equiv: - if (second < first) - std::swap(first, second); + { + // Equiv is commutative: sort operands. + formula_ptr_less_than cmp; + if (cmp(second, first) > 0) + std::swap(first, second); + } + // - (0 <=> Exp) = !Exp + // - (1 <=> Exp) = Exp + if (first == constant::false_instance()) + return unop::instance(unop::Not, second); + if (first == constant::true_instance()) + return second; + // We expect constants to appear first, because they are + // instantiated first. + assert(second != constant::false_instance()); + assert(second != constant::true_instance()); break; case Implies: + /// - (1 => Exp) = Exp + /// - (0 => Exp) = 0 + /// - (Exp => 1) = 1 + /// - (Exp => 0) = !Exp + if (first == constant::true_instance()) + return second; + if (first == constant::false_instance()) + { + second->destroy(); + return first; + } + if (second == constant::true_instance()) + { + first->destroy(); + return second; + } + if (second == constant::false_instance()) + return unop::instance(unop::Not, first); + break; case U: - case R: + /// - (Exp U 1) = 1 + /// - (Exp U 0) = 0 + /// - (0 U Exp) = Exp + if (second == constant::true_instance() + || second == constant::false_instance() + || first == constant::false_instance()) + { + first->destroy(); + return second; + } + break; case W: + /// - (Exp W 1) = 1 + /// - (0 W Exp) = Exp + /// - (1 W Exp) = 1 + if (second == constant::true_instance() + || first == constant::false_instance()) + { + first->destroy(); + return second; + } + if (first == constant::true_instance()) + { + second->destroy(); + return first; + } + break; + case R: + /// - (Exp R 1) = 1 + /// - (Exp R 0) = 0 + /// - (1 R Exp) = Exp + if (second == constant::true_instance() + || second == constant::false_instance() + || first == constant::true_instance()) + { + first->destroy(); + return second; + } + break; case M: - // Non commutative operators. + /// - (Exp M 0) = 0 + /// - (1 M Exp) = Exp + /// - (0 M Exp) = 0 + if (second == constant::false_instance() + || first == constant::true_instance()) + { + first->destroy(); + return second; + } + if (first == constant::false_instance()) + { + second->destroy(); + return first; + } break; } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 9650fed08..1731b1d67 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -56,9 +56,37 @@ namespace spot M //< strong release (dual of weak until) }; - /// Build an unary operator with operation \a op and + /// \brief Build a unary operator with operation \a op and /// children \a first and \a second. - static binop* instance(type op, formula* first, formula* second); + /// + /// Some reordering will be performed on arguments of commutative + /// operators (Xor and Equiv) to ensure that for instance (a <=> b) + /// is the same formula as (b <=> a). + /// + /// Furthermore, the following trivial simplifications are + /// performed (the left formula is rewritten as the right + /// formula): + /// - (1 => Exp) = Exp + /// - (0 => Exp) = 0 + /// - (Exp => 1) = 1 + /// - (Exp => 0) = !Exp + /// - (1 ^ Exp) = !Exp + /// - (0 ^ Exp) = Exp + /// - (0 <=> Exp) = !Exp + /// - (1 <=> Exp) = Exp + /// - (Exp U 1) = 1 + /// - (Exp U 0) = 0 + /// - (0 U Exp) = Exp + /// - (Exp W 1) = 1 + /// - (0 W Exp) = Exp + /// - (1 W Exp) = 1 + /// - (Exp R 1) = 1 + /// - (Exp R 0) = 0 + /// - (1 R Exp) = Exp + /// - (Exp M 0) = 0 + /// - (1 M Exp) = Exp + /// - (0 M Exp) = 0 + static formula* instance(type op, formula* first, formula* second); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 859b8bb27..c3d13ab53 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,8 +1,8 @@ -// 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 et Marie Curie. +// 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -29,6 +29,10 @@ namespace spot { namespace ltl { + constant constant::true_instance_(constant::True); + constant constant::false_instance_(constant::False); + constant constant::empty_word_instance_(constant::EmptyWord); + constant::constant(type val) : val_(val) { @@ -47,6 +51,8 @@ namespace spot return "constant(1)"; case False: return "constant(0)"; + case EmptyWord: + return "constant(e)"; } // Unreachable code. assert(0); @@ -80,24 +86,12 @@ namespace spot return "1"; case False: return "0"; + case EmptyWord: + return "#e"; } // Unreachable code. assert(0); return 0; } - - constant* - constant::false_instance() - { - static constant f(constant::False); - return &f; - } - - constant* - constant::true_instance() - { - static constant t(constant::True); - return &t; - } } } diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index b60ad8ca2..2d3a8fe87 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -1,8 +1,6 @@ -// 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 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -38,7 +36,7 @@ namespace spot class constant : public formula { public: - enum type { False, True }; + enum type { False, True, EmptyWord }; virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -50,9 +48,11 @@ namespace spot virtual std::string dump() const; /// Get the sole instance of spot::ltl::constant::constant(True). - static constant* true_instance(); + static constant* true_instance() { return &true_instance_; } /// Get the sole instance of spot::ltl::constant::constant(False). - static constant* false_instance(); + static constant* false_instance() { return &false_instance_; } + /// Get the sole instance of spot::ltl::constant::constant(EmptyWord). + static constant* empty_word_instance() { return &empty_word_instance_; } protected: constant(type val); @@ -60,6 +60,12 @@ namespace spot private: type val_; + + static constant true_instance_; + static constant false_instance_; + static constant empty_word_instance_; + // If you add new constants here, be sure to update the + // formula::formula() constructor. }; } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index aa8d0c4e1..ece1135ca 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,8 +1,6 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 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), -// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -73,7 +71,15 @@ namespace spot class formula { public: - formula() : count_(++max_count) {} + formula() : count_(max_count++) + { + // If the counter of formulae ever loops, we want to skip the + // first three values, because they are permanently associated + // to constants, and its convenient to have constants smaller + // than all other formulae. + if (max_count == 0) + max_count = 3; + } /// Entry point for vspot::ltl::visitor instances. virtual void accept(visitor& v) = 0; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 85ce20f7c..c659990a0 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,8 +1,8 @@ -// 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), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -110,6 +110,8 @@ namespace spot return "And"; case Or: return "Or"; + case Concat: + return "Concat"; } // Unreachable code. assert(0); @@ -146,13 +148,24 @@ namespace spot } else { + // All operator except "Concat" not commutative, so + // we just keep a list of the inlined arguments that + // should later be added to the vector. + // For concat we have to keep track of the order of + // all the arguments. + if (op == Concat) + inlined.push_back(*i); ++i; } } - v->insert(v->end(), inlined.begin(), inlined.end()); + if (op == Concat) + *v = inlined; + else + v->insert(v->end(), inlined.begin(), inlined.end()); } - std::sort(v->begin(), v->end(), formula_ptr_less_than()); + if (op != Concat) + std::sort(v->begin(), v->end(), formula_ptr_less_than()); formula* neutral; formula* abs; @@ -166,15 +179,19 @@ namespace spot neutral = constant::false_instance(); abs = constant::true_instance(); break; + case Concat: + neutral = constant::empty_word_instance(); + abs = constant::false_instance(); + break; default: neutral = 0; abs = 0; break; } - // Remove duplicates. We can't use std::unique(), because we - // must destroy() any formula we drop. Also ignore neutral - // elements and handle absorbent elements. + // Remove duplicates (except for Concat). We can't use + // std::unique(), because we must destroy() any formula we drop. + // Also ignore neutral elements and handle absorbent elements. { formula* last = 0; vec::iterator i = v->begin(); @@ -194,7 +211,9 @@ namespace spot } else { - last = *i++; + if (op != Concat) // Don't remove duplicates for Concat. + last = *i; + ++i; } } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 1b979e27b..3b6919d2d 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,8 +1,8 @@ -// 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 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -38,12 +38,10 @@ namespace spot /// \brief Multi-operand operators. /// \ingroup ltl_ast - /// - /// These operators are considered commutative and associative. class multop : public ref_formula { public: - enum type { Or, And }; + enum type { Or, And, Concat }; /// List of formulae. typedef std::vector vec; @@ -51,29 +49,46 @@ namespace spot /// \brief Build a spot::ltl::multop with two children. /// /// If one of the children itself is a spot::ltl::multop - /// with the same type, it will be merged. I.e., children - /// if that child will be added, and that child itself will + /// with the same type, it will be inlined. I.e., children + /// of that child will be added, and that child itself will /// be destroyed. This allows incremental building of /// n-ary ltl::multop. /// /// This functions can perform slight optimizations and - /// may not return an ltl::multop objects. For instance - /// if \c first and \c second are equal, that formula is - /// returned as-is. + /// may not return an ltl::multop object. See the other + /// instance function for the list of rewritings. static formula* instance(type op, formula* first, formula* second); /// \brief Build a spot::ltl::multop with many children. /// /// Same as the other instance() function, but take a vector of - /// formula in argument. This vector is acquired by the + /// formulae as argument. This vector is acquired by the /// spot::ltl::multop class, the caller should allocate it with /// \c new, but not use it (especially not destroy it) after it /// has been passed to spot::ltl::multop. /// - /// This functions can perform slight optimizations and - /// may not return an ltl::multop objects. For instance - /// if the vector contain only one unique element, this - /// this formula will be returned as-is. + /// All operators (Or, And, Concat) are associative, and are + /// automatically inlined. Or and And are commutative, so their + /// argument are also sorted, to ensure that "a & b" is equal to + /// "b & a". For Or and And, duplicate arguments are also + /// removed. + /// + /// Furthermore this function can perform slight optimizations + /// and may not return an ltl::multop object. For instance if + /// the vector contains only one unique element, this this + /// formula will be returned as-is. Neutral and absorbent element + /// are also taken care of. The following rewriting are performed + /// (the left patterns are rewritten as shown on the right): + /// + /// - Concat(Exps1...,#e,Exps2...) = Concat(Exps1...,Exps2...) + /// - Concat(Exps1...,0,Exps2...) = 0 + /// - Concat(Exp) = Exp + /// - And(Exps1...,1,Exps2...) = And(Exps1...,Exps2...) + /// - And(Exps1...,0,Exps2...) = 0 + /// - And(Exp) = Exp + /// - Or(Exps1...,1,Exps2...) = 1 + /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...) + /// - Or(Exp) = Exp static formula* instance(type op, vec* v); virtual void accept(visitor& v); diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index efca0e876..cd30b5609 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,8 +1,8 @@ -// 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 et Marie Curie. +// 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -25,6 +25,7 @@ #include "visitor.hh" #include #include +#include "constant.hh" namespace spot { @@ -98,6 +99,8 @@ namespace spot return "G"; case Finish: return "Finish"; + case Star: + return "Star"; } // Unreachable code. assert(0); @@ -106,9 +109,78 @@ namespace spot unop::map unop::instances; - unop* + formula* unop::instance(type op, formula* child) { + + // Some trivial simplifications. + switch (op) + { + // We have (0*) == (#e) + // (#e*) == (#e) + case Star: + if (child == constant::false_instance() + || child == constant::empty_word_instance()) + return constant::empty_word_instance(); + + // -- fall thru -- + + case F: + case G: + { + // F, G, * are idempotent. + unop* u = dynamic_cast(child); + if (u && u->op() == op) + return u; + + if (op == Star) + break; + + // F(0) = G(0) = 0 + // F(1) = G(1) = 1 + if (child == constant::false_instance() + || child == constant::true_instance()) + return child; + // F(#e) = G(#e) = 1 + if (child == constant::empty_word_instance()) + return constant::true_instance(); + } + + + case Not: + { + // !1 = 0 + if (child == constant::true_instance()) + return constant::false_instance(); + // !0 = 1 + if (child == constant::false_instance()) + return constant::true_instance(); + // Not is an involution. + unop* u = dynamic_cast(child); + if (u && u->op() == op) + { + formula* c = u->child()->clone(); + u->destroy(); + return c; + } + break; + } + + case X: + // X(1) = 1, X(0) = 0 + if (child == constant::true_instance() + || child == constant::false_instance()) + return child; + // X(#e) = 1 + if (child == constant::empty_word_instance()) + return constant::true_instance(); + break; + + case Finish: + // No simplifications for Finish. + break; + } + pair p(op, child); map::iterator i = instances.find(p); if (i != instances.end()) diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index cfd429266..5217fd108 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,8 +1,8 @@ -// 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 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -40,11 +40,40 @@ namespace spot class unop : public ref_formula { public: - enum type { Not, X, F, G, Finish }; // Finish is used in ELTL formulae. + enum type { + // LTL + Not, X, F, G, + // ELTL + Finish, + // Kleene Star + Star, + }; - /// Build an unary operator with operation \a op and + /// \brief Build an unary operator with operation \a op and /// child \a child. - static unop* instance(type op, formula* child); + /// + /// The following trivial simplifications are performed + /// automatically (the left expression is rewritten as the right + /// expression): + /// - 0* = #e + /// - #e* = #e + /// - Exp** = Exp* + /// - FF(Exp) = F(Exp) + /// - GG(Exp) = G(Exp) + /// - F(0) = 0 + /// - G(0) = 0 + /// - F(1) = 1 + /// - G(1) = 1 + /// - F(#e) = 1 + /// - G(#e) = 1 + /// - !1 = 0 + /// - !0 = 1 + /// - !!Exp = Exp + /// + /// This rewriting implies that it is not possible to build an + /// LTL formula object that is SYNTACTICALLY equal to one of + /// these left expressions. + static formula* instance(type op, formula* child); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 820d55dd0..4c1dca2c2 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -83,12 +83,16 @@ using namespace spot::ltl; %token OP_F "sometimes operator" OP_G "always operator" %token OP_X "next operator" OP_NOT "not operator" %token ATOMIC_PROP "atomic proposition" +%token OP_STAR "star operator" OP_CONCAT "concat operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" -%token END_OF_INPUT "end of formula" +%token END_OF_INPUT "end of formula" CONST_EMPTYWORD "empty word" %token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" /* Priorities. */ +/* Low priority regex operator. */ +%left OP_CONCAT + /* Logical operators. */ %left OP_IMPLIES OP_EQUIV %left OP_OR @@ -100,6 +104,9 @@ using namespace spot::ltl; %nonassoc OP_F OP_G %nonassoc OP_X +/* High priority regex operator. */ +%nonassoc OP_STAR + /* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT @@ -194,6 +201,8 @@ subformula: ATOMIC_PROP { $$ = constant::true_instance(); } | CONST_FALSE { $$ = constant::false_instance(); } + | CONST_EMPTYWORD + { $$ = constant::empty_word_instance(); } | PAR_OPEN subformula PAR_CLOSE { $$ = $2; } | PAR_OPEN error PAR_CLOSE @@ -220,6 +229,10 @@ subformula: ATOMIC_PROP { $$ = multop::instance(multop::Or, $1, $3); } | subformula OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } + | subformula OP_CONCAT subformula + { $$ = multop::instance(multop::Concat, $1, $3); } + | subformula OP_CONCAT error + { missing_right_binop($$, $1, @2, "concat operator"); } | subformula OP_XOR subformula { $$ = binop::instance(binop::Xor, $1, $3); } | subformula OP_XOR error @@ -264,6 +277,8 @@ subformula: ATOMIC_PROP { $$ = unop::instance(unop::Not, $2); } | OP_NOT error { missing_right_op($$, @1, "not operator"); } + | subformula OP_STAR + { $$ = unop::instance(unop::Star, $1); } ; %% diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index a93bef7e4..5732c686e 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,7 +1,7 @@ /* Copyright (C) 2010, 2011, 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 +** département Syst�mes R�partis Coop�ratifs (SRC), Université Pierre ** et Marie Curie. ** ** This file is part of Spot, a model checking library. @@ -75,6 +75,8 @@ flex_set_buffer(const char* buf) /* ~ comes from Goal, ! from everybody else */ "!"|"~" BEGIN(0); return token::OP_NOT; +"#e" BEGIN(0); return token::CONST_EMPTYWORD; + /* & and | come from Spin. && and || from LTL2BA. /\, \/, and xor are from LBTT. --> and <--> come from Goal. */ @@ -83,6 +85,8 @@ flex_set_buffer(const char* buf) "^"|"xor" BEGIN(0); return token::OP_XOR; "=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES; "<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV; +"*" BEGIN(0); return token::OP_STAR; +";" BEGIN(0); return token::OP_CONCAT; /* <>, [], and () are used in Spin. */ "F"|"<>" BEGIN(0); return token::OP_F; diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index ad120baa6..15221b653 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2010, 2011 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 @@ -68,3 +68,49 @@ run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a' # Corner cases parsing run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))' + +# Trivial simplifications +run 0 ../equals '0*' '#e' +run 0 ../equals '#e*' '#e' +run 0 ../equals 'Exp**' 'Exp*' +run 0 ../equals 'FF(Exp)' 'F(Exp)' +run 0 ../equals 'GG(Exp)' 'G(Exp)' +run 0 ../equals 'F(0)' '0' +run 0 ../equals 'G(0)' '0' +run 0 ../equals 'F(1)' '1' +run 0 ../equals 'G(1)' '1' +run 0 ../equals 'F(#e)' '1' +run 0 ../equals 'G(#e)' '1' +run 0 ../equals '!1' '0' +run 0 ../equals '!0' '1' +run 0 ../equals '!!Exp' 'Exp' + +run 0 ../equals '(1 => Exp)' 'Exp' +run 0 ../equals '(0 => Exp)' '0' +run 0 ../equals '(Exp => 1)' '1' +run 0 ../equals '(Exp => 0)' '!Exp' +run 0 ../equals '(1 ^ Exp)' '!Exp' +run 0 ../equals '(0 ^ Exp)' 'Exp' +run 0 ../equals '(0 <=> Exp)' '!Exp' +run 0 ../equals '(1 <=> Exp)' 'Exp' +run 0 ../equals '(Exp U 1)' '1' +run 0 ../equals '(Exp U 0)' '0' +run 0 ../equals '(Exp R 1)' '1' +run 0 ../equals '(Exp R 0)' '0' +run 0 ../equals '(1 R Exp)' 'Exp' + +run 0 ../equals FFx Fx +run 0 ../equals FFFFFx Fx +run 0 ../equals GGx Gx +run 0 ../equals GGGGGx Gx +run 0 ../equals '!!x' x +run 0 ../equals '!!!!!x' '!x' +run 0 ../equals '#e;x' x +run 0 ../equals 'x;#e' x +run 0 ../equals '#e;x;#e;#e' x +run 0 ../equals '#e;x;#e;x;#e' 'x;x' +run 0 ../equals 'x;x;x;#e;x;x' 'x;x;x;x;x' +run 0 ../equals 'x;0;x;x;x' '0' +run 0 ../equals '0*' '#e' +run 0 ../equals '#e*' '#e' +run 0 ../equals 'x;x;FF(0)' '0' diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test index bb6f02cb7..f46682de8 100755 --- a/src/ltltest/nenoform.test +++ b/src/ltltest/nenoform.test @@ -1,8 +1,8 @@ #! /bin/sh -# 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 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -66,3 +66,8 @@ run 0 ../nenoform '!(a | b | c | d)' '!a & !b & !c & !d' run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \ '!a R (b R ((!a | !b | !c) U !d))' run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b' + +# Rational operators +run 0 ../nenoform '!(X((!Xa)*))' 'X!((X!a)*)' +run 0 ../nenoform 'X((Xa)*)' 'X((Xa)*)' +run 0 ../nenoform '!F!X!(GF(a);!FG(a);x)' 'GX!(GFa;GF!a;x)' diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test index 1c0a59c19..d8ec2aaf6 100755 --- a/src/ltltest/parse.test +++ b/src/ltltest/parse.test @@ -2,7 +2,7 @@ # Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement # 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 +# d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -42,8 +42,6 @@ for f in \ 'a && .b.' \ 'a + b' \ 'a3214 | b' \ - 'a & b' \ - 'a && b' \ 'a /\ b' \ 'a || b' \ 'a \/ b' \ diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test index 8148f239d..60a7b3dff 100755 --- a/src/ltltest/tunabbrev.test +++ b/src/ltltest/tunabbrev.test @@ -1,8 +1,8 @@ #! /bin/sh -# 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 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -55,5 +55,6 @@ run 0 ../tunabbrev '(a ^ b) | (b ^ c)' \ run 0 ../tunabbrev 'G a ' 'false R a' run 0 ../tunabbrev 'GF a => F G(b)' \ '!(false R (true U a)) | (true U (false V b))' -run 0 ../tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))' -run 0 ../tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))' +run 0 ../tunabbrev 'GGGGa' 'false V a' +run 0 ../tunabbrev 'FFFfalse' '0' +run 0 ../tunabbrev 'FFFf' 'true U f' diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index adc1126b5..e31dd83bc 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -1,8 +1,8 @@ // Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2007 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), +// Universit� Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -241,6 +241,10 @@ namespace spot case unop::Finish: result_ = unop::instance(unop::Finish, result_); return; + + case unop::Star: + result_ = unop::instance(unop::Star, result_); + return; } /* Unreachable code. */ assert(0); @@ -477,7 +481,7 @@ namespace spot || b->op() == binop::M) && b->first() == a) { - binop* r = + formula* r = binop::instance(binop::M, a->clone(), b->second()->clone()); @@ -490,7 +494,7 @@ namespace spot || b->op() == binop::U) && b->second() == a) { - binop* r = + formula* r = binop::instance(binop::U, b->first()->clone(), a->clone()); @@ -656,7 +660,7 @@ namespace spot || b->op() == binop::W) && b->first() == a) { - binop* r = + formula* r = binop::instance(binop::W, a->clone(), b->second()->clone()); @@ -779,6 +783,9 @@ namespace spot } break; + case multop::Concat: + std::copy(res->begin(), res->end(), tmpOther->end()); + break; } res->clear(); diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index cc727154e..0a38faa26 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -355,6 +355,8 @@ namespace spot } } break; + case multop::Concat: + break; } if (changed) { diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index f40262971..f5d588772 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,7 +1,7 @@ // Copyright (C) 2009, 2010 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 +// d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -49,14 +49,15 @@ namespace spot { /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: - result_ = multop::instance(multop::Or, - multop::instance(multop::And, f1->clone(), - unop::instance(unop::Not, - f2)), - multop::instance(multop::And, f2->clone(), - unop::instance(unop::Not, - f1))); - return; + { + formula* a = multop::instance(multop::And, f1->clone(), + unop::instance(unop::Not, + f2->clone())); + formula* b = multop::instance(multop::And, f2, + unop::instance(unop::Not, f1)); + result_ = multop::instance(multop::Or, a, b); + return; + } /* f1 => f2 == !f1 | f2 */ case binop::Implies: result_ = multop::instance(multop::Or, @@ -64,15 +65,18 @@ namespace spot return; /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ case binop::Equiv: - result_ = multop::instance(multop::Or, - multop::instance(multop::And, - f1->clone(), f2->clone()), - multop::instance(multop::And, - unop::instance(unop::Not, - f1), - unop::instance(unop::Not, - f2))); - return; + { + formula* f1c = f1->clone(); + formula* f2c = f2->clone(); + + result_ = + multop::instance(multop::Or, + multop::instance(multop::And, f1c, f2c), + multop::instance(multop::And, + unop::instance(unop::Not, f1), + unop::instance(unop::Not, f2))); + return; + } /* f1 U f2 == f1 U f2 */ /* f1 R f2 == f1 R f2 */ /* f1 W f2 == f1 W f2 */ diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 286d8d011..e455dcfc6 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -76,6 +76,10 @@ namespace spot case constant::False: result_ = constant::true_instance(); return; + case constant::EmptyWord: + result_ = unop::instance(unop::Not, + constant::empty_word_instance()); + return; } /* Unreachable code. */ assert(0); @@ -104,12 +108,18 @@ namespace spot result_ = unop::instance(negated_ ? unop::F : unop::G, recurse(f)); return; - case unop::Finish: + /* Finish(x) is not simplified */ result_ = unop::instance(unop::Finish, recurse_(f, false)); if (negated_) result_ = unop::instance(unop::Not, result_); return; + case unop::Star: + /* !(a*) is not simplified */ + result_ = unop::instance(unop::Star, recurse_(f, false)); + if (negated_) + result_ = unop::instance(unop::Not, result_); + return; } /* Unreachable code. */ assert(0); @@ -184,9 +194,9 @@ namespace spot void visit(multop* mo) { + multop::type op = mo->op(); /* !(a & b & c) == !a | !b | !c */ /* !(a | b | c) == !a & !b & !c */ - multop::type op = mo->op(); if (negated_) switch (op) { @@ -196,12 +206,25 @@ namespace spot case multop::Or: op = multop::And; break; + case multop::Concat: + break; } multop::vec* res = new multop::vec; unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(op, res); + if (op != multop::Concat) + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(op, res); + } + else + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse_(mo->nth(i), false)); + result_ = multop::instance(op, res); + if (negated_) + result_ = unop::instance(unop::Not, result_); + } } formula* diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index d506e7e60..36bad8e36 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -256,6 +256,11 @@ namespace spot case unop::Finish: result_ = unop::instance(unop::Finish, result_); return; + + case unop::Star: + result_ = unop::instance(unop::Star, result_); + return; + } /* Unreachable code. */ assert(0); @@ -470,7 +475,8 @@ namespace spot for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); - if (opt_ & Reduce_Syntactic_Implications) + if ((opt_ & Reduce_Syntactic_Implications) + && (mo->op() != multop::Concat)) { bool removed = true; diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 7c2a51b78..2013af89d 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -74,6 +74,8 @@ namespace spot case constant::False: result_ = false; return; + case constant::EmptyWord: + result_ = true; } } @@ -105,6 +107,8 @@ namespace spot return; case unop::Finish: return; + case unop::Star: + return; } /* Unreachable code. */ assert(0); @@ -195,6 +199,8 @@ namespace spot if (syntactic_implication(f, mo->nth(i))) result_ = true; break; + case multop::Concat: + break; } } @@ -230,6 +236,15 @@ namespace spot return false; } + bool + special_case_check(const formula* f2) + { + const binop* f2b = dynamic_cast(f2); + if (!f2b) + return false; + return special_case(f2b); + } + int result() const { @@ -257,6 +272,9 @@ namespace spot case constant::False: result_ = true; return; + case constant::EmptyWord: + result_ = true; + return; } /* Unreachable code. */ assert(0); @@ -283,10 +301,10 @@ namespace spot case unop::F: { /* F(a) = true U a */ - const binop* tmp = binop::instance(binop::U, - constant::true_instance(), - f1->clone()); - if (special_case(tmp)) + const formula* tmp = binop::instance(binop::U, + constant::true_instance(), + f1->clone()); + if (special_case_check(tmp)) { result_ = true; tmp->destroy(); @@ -300,10 +318,10 @@ namespace spot case unop::G: { /* G(a) = false R a */ - const binop* tmp = binop::instance(binop::R, - constant::false_instance(), - f1->clone()); - if (special_case(tmp)) + const formula* tmp = binop::instance(binop::R, + constant::false_instance(), + f1->clone()); + if (special_case_check(tmp)) { result_ = true; tmp->destroy(); @@ -316,6 +334,8 @@ namespace spot } case unop::Finish: return; + case unop::Star: + return; } /* Unreachable code. */ assert(0); @@ -431,6 +451,8 @@ namespace spot return; result_ = true; break; + case multop::Concat: + break; } } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index cbbe59252..cedb8b61b 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -174,6 +174,10 @@ namespace spot os_ << "finish"; need_parent = true; break; + case unop::Star: + // Do not output anything yet, star is a postfix operator. + need_parent = false; + break; } top_level_ = false; @@ -185,6 +189,9 @@ namespace spot if (full_parent_ && !top_level) os_ << ")"; + + if (uo->op() == unop::Star) + os_ << "*"; } void @@ -227,6 +234,9 @@ namespace spot case multop::And: ch = " & "; break; + case multop::Concat: + ch = ";"; + break; } for (unsigned n = 1; n < max; ++n) @@ -351,6 +361,11 @@ namespace spot os_ << "finish"; need_parent = true; break; + case unop::Star: + // Do not output anything yet, star is a postfix operator. + // FIXME: is there a better way to output "Star" for Spin? + need_parent = false; + break; } top_level_ = false; @@ -359,6 +374,8 @@ namespace spot uo->child()->accept(*this); if (need_parent) os_ << ")"; + if (uo->op() == unop::Star) + os_ << "*"; if (full_parent_ && !top_level) os_ << ")"; } @@ -403,6 +420,9 @@ namespace spot case multop::And: ch = " && "; break; + case multop::Concat: + ch = ";"; + break; } for (unsigned n = 1; n < max; ++n) diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index f778ccdcd..6f8485380 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -42,6 +42,7 @@ namespace spot case unop::Finish: case unop::X: case unop::Not: + case unop::Star: this->super::visit(uo); return; case unop::F: diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 6dfc7467d..0607a6a1b 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -63,6 +63,8 @@ namespace spot case constant::False: res_ = bddfalse; return; + case constant::EmptyWord: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); @@ -77,6 +79,7 @@ namespace spot case unop::F: case unop::G: case unop::X: + case unop::Star: assert(!"unsupported operator"); case unop::Not: { @@ -135,6 +138,8 @@ namespace spot op = bddop_or; res_ = bddfalse; break; + case multop::Concat: + assert(!"unsupported operator"); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 429be6b4b..78b67c7b7 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -71,6 +71,8 @@ namespace spot case constant::False: res_ = bddfalse; return; + case constant::EmptyWord: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); @@ -99,6 +101,7 @@ namespace spot case unop::X: case unop::F: case unop::G: + case unop::Star: assert(!"unsupported operator"); } /* Unreachable code. */ @@ -152,6 +155,8 @@ namespace spot op = bddop_or; res_ = bddfalse; break; + case multop::Concat: + assert(!"unsupported operator"); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 89767cd95..31795fe95 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -102,6 +102,9 @@ namespace spot } case constant::False: return; + case constant::EmptyWord: + assert(!"unsupported operator"); + return; } /* Unreachable code. */ assert(0); @@ -138,7 +141,9 @@ namespace spot succ_ = v.succ_; return; case unop::Finish: + case unop::Star: assert(!"unsupported operator"); + return; } /* Unreachable code. */ assert(0); @@ -313,6 +318,9 @@ namespace spot succ_.push_back(*i); } return; + case multop::Concat: + assert(!"unsupported operator"); + return; } /* Unreachable code. */ assert(0); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 56e66a1b2..ea14853a4 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -307,6 +307,8 @@ namespace spot case constant::False: res_ = bddfalse; return; + case constant::EmptyWord: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); @@ -361,6 +363,7 @@ namespace spot return; } case unop::Finish: + case unop::Star: assert(!"unsupported operator"); } /* Unreachable code. */ @@ -440,6 +443,8 @@ namespace spot op = bddop_or; res_ = bddfalse; break; + case multop::Concat: + assert(!"unsupported operator"); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index c3bce3782..1fdfd23a6 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -76,6 +76,8 @@ namespace spot case constant::False: res_ = bddfalse; return; + case constant::EmptyWord: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); @@ -148,6 +150,7 @@ namespace spot return; } case unop::Finish: + case unop::Star: assert(!"unsupported operator"); } /* Unreachable code. */ @@ -248,6 +251,8 @@ namespace spot op = bddop_or; res_ = bddfalse; break; + case multop::Concat: + assert(!"unsupported operator"); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 7630fa528..2f7ea96bd 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -96,6 +96,6 @@ expect_ce 'Fa & Xb & GFc & Gd' 1 expect_ce 'Fa & Xa & GFc & Gc' 2 expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1 expect_ce '!((FF a) <=> (F x))' 3 -expect_no '!((FF a) <=> (F a))' 4 +expect_no '!((FF a) <=> (F a))' 3 expect_no 'Xa && (!a U b) && !b && X!b' 4 expect_no '(a U !b) && Gb' 3