diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index e1116a09f..1f7c17a89 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -45,6 +45,7 @@ namespace spot is.eventual = false; is.universal = false; is.not_marked = true; + is.accepting_eword = false; } atomic_prop::~atomic_prop() diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 4b616c441..69c674a84 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -41,6 +41,7 @@ namespace spot is.eventual = false; is.universal = false; is.not_marked = true; + is.accepting_eword = false; unsigned s = v->size(); for (unsigned i = 0; i < s; ++i) diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 1735ffa55..cf0363525 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -56,6 +56,7 @@ namespace spot case Equiv: is.sugar_free_boolean = false; is.in_nenoform = false; + is.accepting_eword = false; break; case EConcatMarked: is.not_marked = false; @@ -65,6 +66,7 @@ namespace spot is.ltl_formula = false; is.boolean = false; is.eltl_formula = false; + is.accepting_eword = false; break; case U: // 1 U a = Fa @@ -72,6 +74,7 @@ namespace spot is.eventual = 1; is.boolean = false; is.eltl_formula = false; + is.accepting_eword = false; break; case W: // a W 0 = Ga @@ -79,6 +82,7 @@ namespace spot is.universal = 1; is.boolean = false; is.eltl_formula = false; + is.accepting_eword = false; break; case R: // 0 R a = Ga @@ -86,6 +90,7 @@ namespace spot is.universal = 1; is.boolean = false; is.eltl_formula = false; + is.accepting_eword = false; break; case M: // a M 1 = Fa @@ -93,6 +98,7 @@ namespace spot is.eventual = 1; is.boolean = false; is.eltl_formula = false; + is.accepting_eword = false; break; } } diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 733c8c487..c9bb31af7 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -35,16 +35,21 @@ namespace spot { props = child->get_props(); + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.eventual = false; + is.universal = false; + switch (op_) { - case Equal: case Star: + if (min_ == 0) + is.accepting_eword = true; + break; + case Equal: case Goto: - is.boolean = false; - is.ltl_formula = false; - is.eltl_formula = false; - is.eventual = false; - is.universal = false; + is.accepting_eword = (min_ == 0); break; } } diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index df15547e5..2fb9dc834 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -51,6 +51,7 @@ namespace spot is.eventual = true; is.universal = true; is.not_marked = true; + is.accepting_eword = false; break; case constant::EmptyWord: is.boolean = false; @@ -64,6 +65,7 @@ namespace spot is.eventual = false; is.universal = false; is.not_marked = true; + is.accepting_eword = true; break; } } diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 4033a1d9c..92a36fa1d 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -86,6 +86,7 @@ namespace spot proprint(is_eventual, "e", "pure eventuality"); proprint(is_universal, "u", "purely universal"); proprint(is_marked, "+", "marked"); + proprint(accepts_eword, "0", "accepts the empty word"); return out; } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index f221239e8..5a323f030 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -211,6 +211,12 @@ namespace spot return !is.not_marked; } + /// Whether the formula accepts [*0]. + bool accepts_eword() const + { + return is.accepting_eword; + } + /// The properties as a field of bits. For internal use. unsigned get_props() const { @@ -252,7 +258,7 @@ namespace spot // "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 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. @@ -260,7 +266,8 @@ namespace spot 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 + bool not_marked:1; // No occurrence of EConcatMarked. + bool accepting_eword:1; // Accepts the empty word. }; union { diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 84bedeba4..dc5c32ab5 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -28,7 +28,6 @@ #include "multop.hh" #include "constant.hh" #include "visitor.hh" -#include "ltlvisit/consterm.hh" namespace spot { @@ -40,10 +39,6 @@ namespace spot 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: @@ -53,15 +48,29 @@ namespace spot is.eltl_formula = false; is.eventual = false; is.universal = false; - break; + // fall through 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: + props = (*v)[0]->get_props(); + for (unsigned i = 1; i < s; ++i) + props &= (*v)[i]->get_props(); break; + case Or: + { + bool ew = (*v)[0]->accepts_eword(); + props = (*v)[0]->get_props(); + for (unsigned i = 1; i < s; ++i) + { + ew |= (*v)[i]->accepts_eword(); + props &= (*v)[i]->get_props(); + } + is.accepting_eword = ew; + break; + } } } @@ -280,21 +289,20 @@ namespace spot ++i; } } - // We have a* & [*0] & 0 = 0 // already checked above - // but a* & [*0] & c* = [*0] - // So if [*0] has been seen, check if all term recognize the + // We have a* & [*0] & c = 0 + // and a* & [*0] & c* = [*0] + // So if [*0] has been seen, check if alls term recognize the // empty word. if (weak_abs_seen) { - bool acc_empty = true; + bool acc_eword = true; for (i = v->begin(); i != v->end(); ++i) { - if (acc_empty) - acc_empty = constant_term_as_bool(*i); + acc_eword &= (*i)->accepts_eword(); (*i)->destroy(); } delete v; - if (acc_empty) + if (acc_eword) return weak_abs; else return constant::false_instance(); diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index b19880000..b7129e6b8 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -40,34 +40,40 @@ namespace spot { case Not: is.in_nenoform = !!dynamic_cast(child); + is.accepting_eword = false; break; case X: is.boolean = false; is.X_free = false; is.eltl_formula = false; + is.accepting_eword = false; break; case F: is.boolean = false; is.eltl_formula = false; is.sugar_free_ltl = false; is.eventual = true; + is.accepting_eword = false; break; case G: is.boolean = false; is.eltl_formula = false; is.sugar_free_ltl = false; is.universal = true; + is.accepting_eword = false; break; case Finish: is.boolean = false; is.ltl_formula = false; is.psl_formula = false; + is.accepting_eword = false; break; case Closure: case NegClosure: is.boolean = false; is.ltl_formula = false; is.eltl_formula = false; + is.accepting_eword = false; break; } } diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc index 94531c5c6..ae8f3e3f5 100644 --- a/src/ltltest/consterm.cc +++ b/src/ltltest/consterm.cc @@ -22,7 +22,6 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/consterm.hh" #include "ltlast/allnodes.hh" void @@ -44,7 +43,7 @@ main(int argc, char **argv) if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; - bool b = spot::ltl::constant_term_as_bool(f1); + bool b = f1->accepts_eword(); std::cout << b << std::endl; @@ -52,6 +51,7 @@ main(int argc, char **argv) assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::bunop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); return b; } diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 186d1d286..bd7a600a2 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -29,7 +29,6 @@ ltlvisitdir = $(pkgincludedir)/ltlvisit ltlvisit_HEADERS = \ apcollect.hh \ basicreduce.hh \ - consterm.hh \ contain.hh \ clone.hh \ destroy.hh \ @@ -51,7 +50,6 @@ noinst_LTLIBRARIES = libltlvisit.la libltlvisit_la_SOURCES = \ apcollect.cc \ basicreduce.cc \ - consterm.cc \ contain.cc \ clone.cc \ destroy.cc \ diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc deleted file mode 100644 index 5bf3f8f72..000000000 --- a/src/ltlvisit/consterm.cc +++ /dev/null @@ -1,175 +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 "ltlvisit/consterm.hh" -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" - -namespace spot -{ - namespace ltl - { - namespace - { - class consterm_visitor: public const_visitor - { - public: - consterm_visitor() {} - virtual ~consterm_visitor() {} - - bool result() const { return result_; } - - void - visit(const atomic_prop*) - { - result_ = false; - } - - void - visit(const constant* c) - { - result_ = (c == constant::empty_word_instance()); - } - - void - visit(const binop* bo) - { - switch (bo->op()) - { - case binop::Xor: - case binop::Implies: - case binop::Equiv: - assert(!"const_term not yet defined on Xor, Implies and Equiv"); - break; - case binop::U: - case binop::W: - case binop::M: - case binop::R: - case binop::EConcat: - case binop::UConcat: - case binop::EConcatMarked: - assert(!"unsupported operator"); - break; - } - } - - void - visit(const bunop* bo) - { - switch (bo->op()) - { - case bunop::Star: - if (bo->min() == 0) - result_ = true; - else - bo->child()->accept(*this); - break; - case bunop::Equal: - case bunop::Goto: - result_ = bo->min() == 0; - break; - } - } - - void - visit(const unop* uo) - { - switch (uo->op()) - { - case unop::Not: - result_ = false; - break; - case unop::X: - case unop::F: - case unop::G: - case unop::Finish: - case unop::Closure: - case unop::NegClosure: - assert(!"unsupported operator"); - break; - } - } - - void - visit(const automatop*) - { - assert(!"automatop not supported for constant term"); - } - - void - visit(const multop* mo) - { - // The fusion operator cannot be used to recognize the empty word. - if (mo->op() == multop::Fusion) - { - result_ = false; - return; - } - - unsigned max = mo->size(); - // This sets the initial value of result_. - mo->nth(0)->accept(*this); - - for (unsigned n = 1; n < max; ++n) - { - bool r = constant_term_as_bool(mo->nth(n)); - - switch (mo->op()) - { - case multop::Or: - result_ |= r; - if (result_) - return; - break; - case multop::And: - case multop::AndNLM: - case multop::Concat: - result_ &= r; - if (!result_) - return; - break; - case multop::Fusion: - /* Unreachable code */ - assert(0); - break; - } - } - } - - private: - bool result_; - }; - - } - - bool constant_term_as_bool(const formula* f) - { - consterm_visitor v; - f->accept(v); - return v.result(); - } - - formula* constant_term(const formula* f) - { - return constant_term_as_bool(f) ? - constant::empty_word_instance() : constant::false_instance(); - } - } -} diff --git a/src/ltlvisit/consterm.hh b/src/ltlvisit/consterm.hh deleted file mode 100644 index e40f42df5..000000000 --- a/src/ltlvisit/consterm.hh +++ /dev/null @@ -1,54 +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_CONSTERM_HH -# define SPOT_LTLVISIT_CONSTERM_HH - -#include "ltlast/formula.hh" - -namespace spot -{ - namespace ltl - { - /// \brief Compute the constant term of a formula. - /// \ingroup ltl_misc - /// - /// The constant term of a formula is the empty word if the empty - /// word is a model of the formula, it is false otherwise. - /// - /// \see constant_term_as_bool - formula* constant_term(const formula* f); - - /// \brief Compute the constant term of a formula. - /// \ingroup ltl_misc - /// - /// The constant term of a formula is the empty word if the empty - /// word is a model of the formula, it is false otherwise. - /// - /// This variant of the function return true instead of - /// constant::empty_word_instance() and false instead of - /// constant::false_instance(). - /// - /// \see constant_term - bool constant_term_as_bool(const formula* f); - } -} - -#endif // SPOT_LTLVISIT_LENGTH_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 10ae772d4..85c3107c7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -38,7 +38,6 @@ #include #include "ltl2tgba_fm.hh" #include "ltlvisit/contain.hh" -#include "ltlvisit/consterm.hh" #include "tgba/bddprint.hh" namespace spot @@ -506,7 +505,7 @@ namespace spot for (unsigned n = 0; n < s; ++n) { const formula* f = node->nth(n); - if (constant_term_as_bool(f)) + if (f->accepts_eword()) final->push_back(f->clone()); else non_final->push_back(f->clone()); @@ -593,12 +592,12 @@ namespace spot dest2->destroy(); res_ |= label & bdd_ithvar(x); } - if (constant_term_as_bool(node)) + if (node->accepts_eword()) res_ |= label & next_to_concat(); } } } - if (constant_term_as_bool(node)) + if (node->accepts_eword()) res_ |= now_to_concat(); break; @@ -652,7 +651,7 @@ namespace spot bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); formula* dest = dict_.conj_bdd_to_formula(dest_bdd); - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) { // The destination is a final state. Make sure we // can also exit if tail is satisfied. @@ -838,7 +837,7 @@ namespace spot case unop::Closure: { rat_seen_ = true; - if (constant_term_as_bool(node->child())) + if (node->child()->accepts_eword()) { res_ = bddtrue; return; @@ -864,7 +863,7 @@ namespace spot dict_.var_set)); const formula* dest2; - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) { dest->destroy(); res_ |= label; @@ -891,7 +890,7 @@ namespace spot formula* dest = dict_.conj_bdd_to_formula(dest_bdd); const formula* dest2; - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) { dest->destroy(); res_ |= label; @@ -915,7 +914,7 @@ namespace spot rat_seen_ = true; has_marked_ = true; - if (constant_term_as_bool(node->child())) + if (node->child()->accepts_eword()) { res_ = bddfalse; return; @@ -945,7 +944,7 @@ namespace spot dict_.var_set)); // !{ Exp } is false if Exp accepts the empty word. - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) { dest->destroy(); continue; @@ -1084,7 +1083,7 @@ namespace spot dest2->destroy(); res_ |= label & bdd_ithvar(x); } - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) res_ |= label & f2; } } @@ -1112,7 +1111,7 @@ namespace spot dest2->destroy(); res_ |= label & bdd_ithvar(x); } - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) res_ |= label & f2; } } @@ -1154,7 +1153,7 @@ namespace spot bdd udest = bdd_ithvar(dict_.register_next_variable(dest2)); - if (constant_term_as_bool(dest)) + if (dest->accepts_eword()) udest &= f2; dest2->destroy();