From cb9549e4d4c5b5858ba2f28aa012985a19b8cea0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Jul 2006 07:27:51 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (language_containment_checker): Move ... * src/ltlvisit/contain.cc, src/ltlvisit/contain.hh (spot::ltl::language_containment_checker): ... in these new files. * src/ltlvisit/Makefile.am: Adjust. --- ChangeLog | 7 +++ src/ltlvisit/Makefile.am | 6 +- src/ltlvisit/contain.cc | 109 +++++++++++++++++++++++++++++++++++ src/ltlvisit/contain.hh | 76 ++++++++++++++++++++++++ src/tgbaalgos/ltl2tgba_fm.cc | 105 +-------------------------------- 5 files changed, 197 insertions(+), 106 deletions(-) create mode 100644 src/ltlvisit/contain.cc create mode 100644 src/ltlvisit/contain.hh diff --git a/ChangeLog b/ChangeLog index e2273d1f5..a7195c297 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2006-07-19 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.cc (language_containment_checker): Move ... + * src/ltlvisit/contain.cc, src/ltlvisit/contain.hh + (spot::ltl::language_containment_checker): ... in these new files. + * src/ltlvisit/Makefile.am: Adjust. + 2006-07-18 Alexandre Duret-Lutz * src/misc/memusage.cc, src/misc/memusage.hh: New files. diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index eeb8beca1..642b1a030 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -19,7 +19,7 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -AM_CPPFLAGS = -I$(srcdir)/.. +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) ltlvisitdir = $(pkgincludedir)/ltlvisit @@ -27,6 +27,7 @@ ltlvisitdir = $(pkgincludedir)/ltlvisit ltlvisit_HEADERS = \ apcollect.hh \ basicreduce.hh \ + contain.hh \ clone.hh \ destroy.hh \ dotty.hh \ @@ -46,6 +47,7 @@ noinst_LTLIBRARIES = libltlvisit.la libltlvisit_la_SOURCES = \ apcollect.cc \ basicreduce.cc \ + contain.cc \ clone.cc \ destroy.cc \ dotty.cc \ diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc new file mode 100644 index 000000000..f4a463bea --- /dev/null +++ b/src/ltlvisit/contain.cc @@ -0,0 +1,109 @@ +// Copyright (C) 2006 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 "contain.hh" +#include "destroy.hh" +#include "clone.hh" +#include "ltlast/unop.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/gtec/gtec.hh" + +namespace spot +{ + namespace ltl + { + + language_containment_checker::language_containment_checker + (bdd_dict* dict, bool exprop, bool symb_merge, + bool branching_postponement, bool fair_loop_approx) + : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), + branching_postponement_(branching_postponement), + fair_loop_approx_(fair_loop_approx) + { + } + + language_containment_checker::~language_containment_checker() + { + while (!translated_.empty()) + { + trans_map::iterator i = translated_.begin(); + delete i->second.translation; + const formula* f = i->first; + translated_.erase(i); + destroy(f); + } + } + + // Check whether L(l) is a subset of L(g). + bool + language_containment_checker::contained(const formula* l, const formula* g) + { + const record_* rl = register_formula_(l); + const formula* ng = unop::instance(unop::Not, clone(g)); + const record_* rng = register_formula_(ng); + destroy(ng); + bool res = rl->incompatible.find(rng) != rl->incompatible.end(); + return res; + } + + // Check whether L(l) = L(g). + bool + language_containment_checker::equal(const formula* l, const formula* g) + { + return contained(l,g) && contained(g,l); + } + + const language_containment_checker::record_* + language_containment_checker::register_formula_(const formula* f) + { + trans_map::iterator i = translated_.find(f); + if (i != translated_.end()) + return &i->second; + + const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, + branching_postponement_, + fair_loop_approx_); + record_& r = translated_[clone(f)]; + r.translation = e; + + // Check the emptiness of the product of this formula with any + // other registered formula. + for (i = translated_.begin(); i != translated_.end(); ++i) + { + if (f == i->first) + continue; + const tgba* p = new tgba_product(e, i->second.translation); + emptiness_check* ec = couvreur99(p); + emptiness_check_result* ecr = ec->check(); + if (!ecr) + { + r.incompatible.insert(&i->second); + i->second.incompatible.insert(&r); + } + else + delete ecr; + delete ec; + delete p; + } + return &r; + } + } +} diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh new file mode 100644 index 000000000..a0bad63f5 --- /dev/null +++ b/src/ltlvisit/contain.hh @@ -0,0 +1,76 @@ +// Copyright (C) 2006 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. + +#ifndef SPOT_LTLVISIT_CONTAIN_HH +# define SPOT_LTLVISIT_CONTAIN_HH + +#include "ltlast/formula.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "misc/hash.hh" +#include + +namespace spot +{ + namespace ltl + { + // Check containment of language represented by LTL formulae. + class language_containment_checker + { + struct record_ + { + const tgba* translation; + typedef std::set incomp_map; + incomp_map incompatible; + }; + typedef Sgi::hash_map trans_map; + public: + /// This class uses spot::ltl_to_tgba_fm to translate LTL + /// formulae. See that class for the meaning of these options. + language_containment_checker(bdd_dict* dict, bool exprop, + bool symb_merge, + bool branching_postponement, + bool fair_loop_approx); + + ~language_containment_checker(); + + /// Check whether L(l) is a subset of L(g). + bool contained(const formula* l, const formula* g); + + /// Check whether L(l) = L(g). + bool equal(const formula* l, const formula* g); + + protected: + const record_* register_formula_(const formula* f); + + /* Translation options */ + bdd_dict* dict_; + bool exprop_; + bool symb_merge_; + bool branching_postponement_; + bool fair_loop_approx_; + /* Translation Maps */ + trans_map translated_; + }; + } +} + +#endif // SPOT_LTLVISIT_CONTAIN_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 80e884f3c..01fd317d4 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -34,8 +34,7 @@ #include #include #include "ltl2tgba_fm.hh" -#include "tgba/tgbaproduct.hh" -#include "tgbaalgos/gtec/gtec.hh" +#include "ltlvisit/contain.hh" namespace spot { @@ -538,108 +537,6 @@ namespace spot pfl_map pfl_; }; - // Keep a map of the TGBA translation of all subformulae and their - // negations, for easy language containment check. - class language_containment_checker - { - struct record_ - { - const tgba* translation; - typedef std::set incomp_map; - incomp_map incompatible; - }; - typedef Sgi::hash_map trans_map; - public: - language_containment_checker(bdd_dict* dict, bool exprop, - bool symb_merge, - bool branching_postponement, - bool fair_loop_approx) - : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), - branching_postponement_(branching_postponement), - fair_loop_approx_(fair_loop_approx) - { - } - - ~language_containment_checker() - { - - while (!translated_.empty()) - { - trans_map::iterator i = translated_.begin(); - delete i->second.translation; - const formula* f = i->first; - translated_.erase(i); - destroy(f); - } - } - - // Check whether L(l) is a subset of L(g). - bool - contained(const formula* l, const formula* g) - { - const record_* rl = register_formula_(l); - const formula* ng = unop::instance(unop::Not, clone(g)); - const record_* rng = register_formula_(ng); - destroy(ng); - bool res = rl->incompatible.find(rng) != rl->incompatible.end(); - return res; - } - - // Check whether L(l) = L(g). - bool - equal(const formula* l, const formula* g) - { - return contained(l,g) && contained(g,l); - } - - protected: - const record_* - register_formula_(const formula* f) - { - trans_map::iterator i = translated_.find(f); - if (i != translated_.end()) - return &i->second; - - const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, - branching_postponement_, - fair_loop_approx_); - record_& r = translated_[clone(f)]; - r.translation = e; - - // Check the emptiness of the product of this formula with any - // other registered formula. - for (i = translated_.begin(); i != translated_.end(); ++i) - { - if (f == i->first) - continue; - const tgba* p = new tgba_product(e, i->second.translation); - emptiness_check* ec = couvreur99(p); - emptiness_check_result* ecr = ec->check(); - if (!ecr) - { - r.incompatible.insert(&i->second); - i->second.incompatible.insert(&r); - } - else - delete ecr; - delete ec; - delete p; - } - return &r; - } - - private: - /* Translation options */ - bdd_dict* dict_; - bool exprop_; - bool symb_merge_; - bool branching_postponement_; - bool fair_loop_approx_; - /* Translation Maps */ - trans_map translated_; - }; - class formula_canonizer { public: