// Copyright (C) 2003 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. // // 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 "ltlast/visitor.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "tgba/tgbabddconcretefactory.hh" #include #include "ltl2tgba_lacim.hh" namespace spot { using namespace ltl; /// \brief Recursively translate a formula into a BDD. /// /// The algorithm used here is adapted from Jean-Michel Couvreur's /// Probataf tool. class ltl_trad_visitor: public const_visitor { public: ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) : fact_(fact), root_(root) { } virtual ~ltl_trad_visitor() { } bdd result() { return res_; } void visit(const atomic_prop* node) { res_ = bdd_ithvar(fact_.create_atomic_prop(node)); } void visit(const constant* node) { switch (node->val()) { case constant::True: res_ = bddtrue; return; case constant::False: res_ = bddfalse; return; } /* Unreachable code. */ assert(0); } void visit(const unop* node) { switch (node->op()) { case unop::F: { /* Fx <=> x | XFx In other words: now <=> x | next */ int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); bdd x = recurse(node->child()); fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); /* `x | next', doesn't actually encode the fact that x should be fulfilled eventually. We ensure this by creating a new generalized Büchi acceptance set, Acc[x], and leave out of this set any transition going off NOW without checking X. Such acceptance conditions are checked for during the emptiness check. */ fact_.declare_acceptance_condition(x | !now, node->child()); res_ = now; return; } case unop::G: { bdd child = recurse(node->child()); // If G occurs at the top of the formula we don't // need Now/Next variables. We just constrain // the relation so that the child always happens. // This saves 2 BDD variables. if (root_) { fact_.constrain_relation(child); res_ = child; return; } // Gx <=> x && XGx int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, child & next, bddop_biimp)); res_ = now; return; } case unop::Not: { res_ = bdd_not(recurse(node->child())); return; } case unop::X: { int v = fact_.create_state(node->child()); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, recurse(node->child()), bddop_biimp)); res_ = next; return; } } /* Unreachable code. */ assert(0); } void visit(const binop* node) { bdd f1 = recurse(node->first()); bdd f2 = recurse(node->second()); switch (node->op()) { case binop::Xor: res_ = bdd_apply(f1, f2, bddop_xor); return; case binop::Implies: res_ = bdd_apply(f1, f2, bddop_imp); return; case binop::Equiv: res_ = bdd_apply(f1, f2, bddop_biimp); return; case binop::U: { /* f1 U f2 <=> f2 | (f1 & X(f1 U f2)) In other words: now <=> f2 | (f1 & next) */ int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), bddop_biimp)); /* The rightmost conjunction, f1 & next, doesn't actually encode the fact that f2 should be fulfilled eventually. We declare an acceptance condition for this purpose (see the comment in the unop::F case). */ fact_.declare_acceptance_condition(f2 | !now, node->second()); res_ = now; return; } case binop::R: { /* f1 R f2 <=> f2 & (f1 | X(f1 U f2)) In other words: now <=> f2 & (f1 | next) */ int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp)); res_ = now; return; } } /* Unreachable code. */ assert(0); } void visit(const multop* node) { int op = -1; bool root = false; switch (node->op()) { case multop::And: op = bddop_and; res_ = bddtrue; // When the root formula is a conjunction it's ok to // consider all children as root formulae. This allows the // root-G trick to save many more variable. (See the // translation of G.) root = root_; break; case multop::Or: op = bddop_or; res_ = bddfalse; break; } assert(op != -1); unsigned s = node->size(); for (unsigned n = 0; n < s; ++n) { res_ = bdd_apply(res_, recurse(node->nth(n), root), op); } } bdd recurse(const formula* f, bool root = false) { ltl_trad_visitor v(fact_, root); f->accept(v); return v.result(); } private: bdd res_; tgba_bdd_concrete_factory& fact_; bool root_; }; tgba_bdd_concrete* ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict) { // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic // abbreviations such as <=>, =>, or XOR, since they // would involve negations at the BDD level. const ltl::formula* f1 = ltl::unabbreviate_logic(f); const ltl::formula* f2 = ltl::negative_normal_form(f1); ltl::destroy(f1); // Traverse the formula and draft the automaton in a factory. tgba_bdd_concrete_factory fact(dict); ltl_trad_visitor v(fact, true); f2->accept(v); ltl::destroy(f2); fact.finish(); // Finally setup the resulting automaton. return new tgba_bdd_concrete(fact, v.result()); } }