diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 678b5b202..12f36f7a0 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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. @@ -37,8 +37,7 @@ tgba_HEADERS = \ tgbamask.hh \ tgbaproxy.hh \ tgbaproduct.hh \ - tgbasafracomplement.hh \ - tgbasl.hh + tgbasafracomplement.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -51,5 +50,4 @@ libtgba_la_SOURCES = \ tgbaproduct.cc \ tgbamask.cc \ tgbaproxy.cc \ - tgbasafracomplement.cc \ - tgbasl.cc + tgbasafracomplement.cc diff --git a/src/tgba/tgbasl.cc b/src/tgba/tgbasl.cc deleted file mode 100644 index 12a8141b1..000000000 --- a/src/tgba/tgbasl.cc +++ /dev/null @@ -1,234 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014 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 3 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 this program. If not, see . - -#include "tgbasl.hh" -#include "bddprint.hh" - -namespace spot -{ - namespace - { - class state_tgbasl: public state - { - public: - state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond) - { - } - - virtual - ~state_tgbasl() - { - s_->destroy(); - } - - virtual int - compare(const state* other) const - { - const state_tgbasl* o = - down_cast(other); - assert(o); - int res = s_->compare(o->real_state()); - if (res != 0) - return res; - return cond_.id() - o->cond_.id(); - } - - virtual size_t - hash() const - { - return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id()); - } - - virtual - state_tgbasl* clone() const - { - return new state_tgbasl(*this); - } - - state* - real_state() const - { - return s_; - } - - bdd - cond() const - { - return cond_; - } - - private: - state* s_; - bdd cond_; - }; - - class tgbasl_succ_iterator : public tgba_succ_iterator - { - public: - tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state, - bdd_dict_ptr d, bdd atomic_propositions) - : it_(it), state_(state), aps_(atomic_propositions), d_(d) - { - } - - virtual - ~tgbasl_succ_iterator() - { - delete it_; - } - - // iteration - - bool - first() - { - loop_ = false; - done_ = false; - need_loop_ = true; - if (it_->first()) - { - cond_ = it_->current_condition(); - next_edge(); - } - return true; - } - - bool - next() - { - if (cond_ != bddfalse) - { - next_edge(); - return true; - } - if (!it_->next()) - { - if (loop_ || !need_loop_) - done_ = true; - loop_ = true; - return !done_; - } - else - { - cond_ = it_->current_condition(); - next_edge(); - return true; - } - } - - bool - done() const - { - return it_->done() && done_; - } - - // inspection - - state_tgbasl* - current_state() const - { - if (loop_) - return new state_tgbasl(state_->real_state(), state_->cond()); - return new state_tgbasl(it_->current_state(), one_); - } - - bdd - current_condition() const - { - if (loop_) - return state_->cond(); - return one_; - } - - acc_cond::mark_t - current_acceptance_conditions() const - { - if (loop_) - return 0U; - return it_->current_acceptance_conditions(); - } - - private: - void - next_edge() - { - one_ = bdd_satoneset(cond_, aps_, bddtrue); - cond_ -= one_; - if (need_loop_ && (state_->cond() == one_) - && (state_ == it_->current_state())) - need_loop_ = false; - } - - tgba_succ_iterator* it_; - const state_tgbasl* state_; - bdd cond_; - bdd one_; - bdd aps_; - bdd_dict_ptr d_; - bool loop_; - bool need_loop_; - bool done_; - }; - } - - tgbasl::tgbasl(const const_tgba_ptr& a, bdd atomic_propositions) - : tgba(a->get_dict()), a_(a), aps_(atomic_propositions) - { - auto d = get_dict(); - d->register_all_propositions_of(&a_, this); - assert(acc_.num_sets() == 0); - acc_.add_sets(a_->acc().num_sets()); - } - - tgbasl::~tgbasl() - { - get_dict()->unregister_all_my_variables(this); - } - - state* - tgbasl::get_init_state() const - { - return new state_tgbasl(a_->get_init_state(), bddfalse); - } - - tgba_succ_iterator* - tgbasl::succ_iter(const state* state) const - { - const state_tgbasl* s = down_cast(state); - assert(s); - return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s, - a_->get_dict(), aps_); - } - - bdd - tgbasl::compute_support_conditions(const state*) const - { - return bddtrue; - } - - std::string - tgbasl::format_state(const state* state) const - { - const state_tgbasl* s = down_cast(state); - assert(s); - return (a_->format_state(s->real_state()) - + ", " - + bdd_format_formula(a_->get_dict(), s->cond())); - } -} diff --git a/src/tgba/tgbasl.hh b/src/tgba/tgbasl.hh deleted file mode 100644 index 00195c717..000000000 --- a/src/tgba/tgbasl.hh +++ /dev/null @@ -1,56 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013, 2014 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBA_TGBASL_HH -# define SPOT_TGBA_TGBASL_HH - -#include "tgba.hh" - -namespace spot -{ - class SPOT_API tgbasl : public tgba - { - public: - tgbasl(const const_tgba_ptr& a, bdd ap); - - virtual ~tgbasl(); - - virtual state* get_init_state() const; - - virtual tgba_succ_iterator* succ_iter(const state* state) const; - - virtual std::string format_state(const state* state) const; - - protected: - virtual bdd compute_support_conditions(const state* state) const; - - private: - const_tgba_ptr a_; - bdd aps_; - }; - - typedef std::shared_ptr tgbasl_ptr; - - inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap) - { - return std::make_shared(aut, ap); - } -} - -#endif diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 2de18b746..4587115e2 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 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), @@ -31,7 +31,6 @@ tgbaalgos_HEADERS = \ are_isomorphic.hh \ bfssteps.hh \ canonicalize.hh \ - closure.hh \ complete.hh \ compsusp.hh \ cycles.hh \ @@ -73,8 +72,7 @@ tgbaalgos_HEADERS = \ simulation.hh \ stats.hh \ stripacc.hh \ - stutter_invariance.hh \ - stutterize.hh \ + stutter.hh \ tau03.hh \ tau03opt.hh \ translate.hh \ @@ -85,7 +83,6 @@ libtgbaalgos_la_SOURCES = \ are_isomorphic.cc \ bfssteps.cc \ canonicalize.cc \ - closure.cc \ complete.cc \ compsusp.cc \ cycles.cc \ @@ -127,8 +124,7 @@ libtgbaalgos_la_SOURCES = \ simulation.cc \ stats.cc \ stripacc.cc \ - stutter_invariance.cc \ - stutterize.cc \ + stutter.cc \ tau03.cc \ tau03opt.cc \ translate.cc \ diff --git a/src/tgbaalgos/closure.cc b/src/tgbaalgos/closure.cc deleted file mode 100644 index da0ca9f06..000000000 --- a/src/tgbaalgos/closure.cc +++ /dev/null @@ -1,102 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita. -// -// 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 3 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 this program. If not, see . - - -#include -#include -#include "closure.hh" -#include "dupexp.hh" -#include - -namespace spot -{ - tgba_digraph_ptr - closure(tgba_digraph_ptr&& a) - { - a->prop_keep({false, // state_based - true, // single_acc - false, // inherently_weak - false, // deterministic - }); - - unsigned n = a->num_states(); - std::vector todo; - std::vector > dst2trans(n); - - for (unsigned state = 0; state < n; ++state) - { - auto trans = a->out(state); - - for (auto it = trans.begin(); it != trans.end(); ++it) - { - todo.push_back(it.trans()); - dst2trans[it->dst].push_back(it.trans()); - } - - while (!todo.empty()) - { - auto t1 = a->trans_storage(todo.back()); - todo.pop_back(); - - for (auto& t2 : a->out(t1.dst)) - { - bdd cond = t1.cond & t2.cond; - if (cond != bddfalse) - { - bool need_new_trans = true; - acc_cond::mark_t acc = t1.acc | t2.acc; - for (auto& t: dst2trans[t2.dst]) - { - auto& ts = a->trans_storage(t); - if (acc == ts.acc) - { - if (!bdd_implies(cond, ts.cond)) - { - ts.cond = ts.cond | cond; - if (std::find(todo.begin(), todo.end(), t) - == todo.end()) - todo.push_back(t); - } - need_new_trans = false; - } - } - if (need_new_trans) - { - // Load t2.dst first, because t2 can be - // invalidated by new_transition(). - auto dst = t2.dst; - auto i = a->new_transition(state, dst, cond, acc); - dst2trans[dst].push_back(i); - todo.push_back(i); - } - } - } - } - for (auto& it: dst2trans) - it.clear(); - } - return a; - } - - tgba_digraph_ptr - closure(const const_tgba_digraph_ptr& a) - { - return closure(make_tgba_digraph(a, {true, true, true, true})); - } -} diff --git a/src/tgbaalgos/closure.hh b/src/tgbaalgos/closure.hh deleted file mode 100644 index f4e2ea090..000000000 --- a/src/tgbaalgos/closure.hh +++ /dev/null @@ -1,36 +0,0 @@ -// Copyright (C) 2014 Laboratoire de Recherche et Développement -// de l'Epita. -// -// 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 3 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 this program. If not, see . - - -#ifndef SPOT_TGBAALGOS_CLOSURE_HH -# define SPOT_TGBAALGOS_CLOSURE_HH - -#include "tgba/tgbagraph.hh" - -namespace spot -{ - SPOT_API tgba_digraph_ptr - closure(const const_tgba_digraph_ptr&); - -#ifndef SWIG - SPOT_API tgba_digraph_ptr - closure(tgba_digraph_ptr&&); -#endif -} - -#endif diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc new file mode 100644 index 000000000..57b66d8cb --- /dev/null +++ b/src/tgbaalgos/stutter.cc @@ -0,0 +1,587 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014, 2015 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 3 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 this program. If not, see . + +#include "stutter.hh" +#include "tgba/tgba.hh" +#include "dupexp.hh" +#include "misc/hash.hh" +#include "misc/hashfunc.hh" +#include "ltlvisit/apcollect.hh" +#include "translate.hh" +#include "ltlast/unop.hh" +#include "ltlvisit/remove_x.hh" +#include "tgbaalgos/product.hh" +#include "tgba/tgbaproduct.hh" +#include "tgba/bddprint.hh" +#include +#include +#include +#include + +namespace spot +{ + namespace + { + class state_tgbasl: public state + { + public: + state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond) + { + } + + virtual + ~state_tgbasl() + { + s_->destroy(); + } + + virtual int + compare(const state* other) const + { + const state_tgbasl* o = + down_cast(other); + assert(o); + int res = s_->compare(o->real_state()); + if (res != 0) + return res; + return cond_.id() - o->cond_.id(); + } + + virtual size_t + hash() const + { + return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id()); + } + + virtual + state_tgbasl* clone() const + { + return new state_tgbasl(*this); + } + + state* + real_state() const + { + return s_; + } + + bdd + cond() const + { + return cond_; + } + + private: + state* s_; + bdd cond_; + }; + + class tgbasl_succ_iterator : public tgba_succ_iterator + { + public: + tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state, + bdd_dict_ptr d, bdd atomic_propositions) + : it_(it), state_(state), aps_(atomic_propositions), d_(d) + { + } + + virtual + ~tgbasl_succ_iterator() + { + delete it_; + } + + // iteration + + bool + first() + { + loop_ = false; + done_ = false; + need_loop_ = true; + if (it_->first()) + { + cond_ = it_->current_condition(); + next_edge(); + } + return true; + } + + bool + next() + { + if (cond_ != bddfalse) + { + next_edge(); + return true; + } + if (!it_->next()) + { + if (loop_ || !need_loop_) + done_ = true; + loop_ = true; + return !done_; + } + else + { + cond_ = it_->current_condition(); + next_edge(); + return true; + } + } + + bool + done() const + { + return it_->done() && done_; + } + + // inspection + + state_tgbasl* + current_state() const + { + if (loop_) + return new state_tgbasl(state_->real_state(), state_->cond()); + return new state_tgbasl(it_->current_state(), one_); + } + + bdd + current_condition() const + { + if (loop_) + return state_->cond(); + return one_; + } + + acc_cond::mark_t + current_acceptance_conditions() const + { + if (loop_) + return 0U; + return it_->current_acceptance_conditions(); + } + + private: + void + next_edge() + { + one_ = bdd_satoneset(cond_, aps_, bddtrue); + cond_ -= one_; + if (need_loop_ && (state_->cond() == one_) + && (state_ == it_->current_state())) + need_loop_ = false; + } + + tgba_succ_iterator* it_; + const state_tgbasl* state_; + bdd cond_; + bdd one_; + bdd aps_; + bdd_dict_ptr d_; + bool loop_; + bool need_loop_; + bool done_; + }; + + + class SPOT_API tgbasl final : public tgba + { + public: + tgbasl(const const_tgba_ptr& a, bdd atomic_propositions) + : tgba(a->get_dict()), a_(a), aps_(atomic_propositions) + { + get_dict()->register_all_propositions_of(&a_, this); + assert(acc_.num_sets() == 0); + acc_.add_sets(a_->acc().num_sets()); + } + + virtual ~tgbasl() + { + get_dict()->unregister_all_my_variables(this); + } + + virtual state* get_init_state() const override + { + return new state_tgbasl(a_->get_init_state(), bddfalse); + } + + virtual tgba_succ_iterator* succ_iter(const state* state) const override + { + const state_tgbasl* s = down_cast(state); + assert(s); + return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s, + a_->get_dict(), aps_); + } + + virtual std::string format_state(const state* state) const override + { + const state_tgbasl* s = down_cast(state); + assert(s); + return (a_->format_state(s->real_state()) + + ", " + + bdd_format_formula(a_->get_dict(), s->cond())); + } + + protected: + virtual bdd compute_support_conditions(const state*) const override + { + return bddtrue; + } + + private: + const_tgba_ptr a_; + bdd aps_; + }; + + typedef std::shared_ptr tgbasl_ptr; + + inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap) + { + return std::make_shared(aut, ap); + } + + + + typedef std::pair stutter_state; + + struct stutter_state_hash + { + size_t + operator()(const stutter_state& s) const + { + return wang32_hash(s.first) ^ wang32_hash(s.second.id()); + } + }; + + // Associate the stutter state to its number. + typedef std::unordered_map ss2num_map; + + // Queue of state to be processed. + typedef std::deque queue_t; + + static bdd + get_all_ap(const const_tgba_digraph_ptr& a) + { + bdd res = bddtrue; + for (auto& i: a->transitions()) + res &= bdd_support(i.cond); + return res; + } + + } + + tgba_digraph_ptr + sl(const const_tgba_digraph_ptr& a, const ltl::formula* f) + { + bdd aps = f + ? atomic_prop_collect_as_bdd(f, a) + : get_all_ap(a); + return sl(a, aps); + } + + tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f) + { + bdd aps = f + ? atomic_prop_collect_as_bdd(f, a) + : get_all_ap(a); + return sl2(a, aps); + } + + tgba_digraph_ptr + sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + { + // The result automaton uses numbered states. + tgba_digraph_ptr res = make_tgba_digraph(a->get_dict()); + // We use the same BDD variables as the input. + res->copy_ap_of(a); + res->copy_acceptance_conditions_of(a); + // These maps make it possible to convert stutter_state to number + // and vice-versa. + ss2num_map ss2num; + + queue_t todo; + + unsigned s0 = a->get_init_state_number(); + stutter_state s(s0, bddfalse); + ss2num[s] = 0; + res->new_state(); + todo.push_back(s); + + while (!todo.empty()) + { + s = todo.front(); + todo.pop_front(); + unsigned src = ss2num[s]; + + bool self_loop_needed = true; + + for (auto& t : a->out(s.first)) + { + bdd all = t.cond; + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); + all -= one; + + stutter_state d(t.dst, one); + + auto r = ss2num.emplace(d, ss2num.size()); + unsigned dest = r.first->second; + + if (r.second) + { + todo.push_back(d); + unsigned u = res->new_state(); + assert(u == dest); + (void)u; + } + + // Create the transition. + res->new_transition(src, dest, one, t.acc); + + if (src == dest) + self_loop_needed = false; + } + } + + if (self_loop_needed && s.second != bddfalse) + res->new_transition(src, src, s.second, 0U); + } + res->merge_transitions(); + return res; + } + + tgba_digraph_ptr + sl2(tgba_digraph_ptr&& a, bdd atomic_propositions) + { + if (atomic_propositions == bddfalse) + atomic_propositions = get_all_ap(a); + unsigned num_states = a->num_states(); + unsigned num_transitions = a->num_transitions(); + for (unsigned src = 0; src < num_states; ++src) + { + auto trans = a->out(src); + + for (auto it = trans.begin(); it != trans.end() + && it.trans() <= num_transitions; ++it) + if (it->dst != src) + { + bdd all = it->cond; + while (all != bddfalse) + { + unsigned dst = it->dst; + bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); + unsigned tmp = a->new_state(); + unsigned i = a->new_transition(src, tmp, one, it->acc); + assert(i > num_transitions); + i = a->new_transition(tmp, tmp, one, 0U); + assert(i > num_transitions); + // No acceptance here to preserve the state-based property. + i = a->new_transition(tmp, dst, one, 0U); + assert(i > num_transitions); + all -= one; + } + } + } + if (num_states != a->num_states()) + a->prop_keep({true, // state_based + true, // single_acc + false, // inherently_weak + false, // deterministic + }); + a->merge_transitions(); + return a; + } + + tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + { + return sl2(make_tgba_digraph(a, tgba::prop_set::all()), + atomic_propositions); + } + + + tgba_digraph_ptr + closure(tgba_digraph_ptr&& a) + { + a->prop_keep({false, // state_based + true, // single_acc + false, // inherently_weak + false, // deterministic + }); + + unsigned n = a->num_states(); + std::vector todo; + std::vector > dst2trans(n); + + for (unsigned state = 0; state < n; ++state) + { + auto trans = a->out(state); + + for (auto it = trans.begin(); it != trans.end(); ++it) + { + todo.push_back(it.trans()); + dst2trans[it->dst].push_back(it.trans()); + } + + while (!todo.empty()) + { + auto t1 = a->trans_storage(todo.back()); + todo.pop_back(); + + for (auto& t2 : a->out(t1.dst)) + { + bdd cond = t1.cond & t2.cond; + if (cond != bddfalse) + { + bool need_new_trans = true; + acc_cond::mark_t acc = t1.acc | t2.acc; + for (auto& t: dst2trans[t2.dst]) + { + auto& ts = a->trans_storage(t); + if (acc == ts.acc) + { + if (!bdd_implies(cond, ts.cond)) + { + ts.cond = ts.cond | cond; + if (std::find(todo.begin(), todo.end(), t) + == todo.end()) + todo.push_back(t); + } + need_new_trans = false; + } + } + if (need_new_trans) + { + // Load t2.dst first, because t2 can be + // invalidated by new_transition(). + auto dst = t2.dst; + auto i = a->new_transition(state, dst, cond, acc); + dst2trans[dst].push_back(i); + todo.push_back(i); + } + } + } + } + for (auto& it: dst2trans) + it.clear(); + } + return a; + } + + tgba_digraph_ptr + closure(const const_tgba_digraph_ptr& a) + { + return closure(make_tgba_digraph(a, {true, true, true, true})); + } + + // The stutter check algorithm to use can be overridden via an + // environment variable. + static int default_stutter_check_algorithm() + { + static const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); + if (stutter_check) + { + char* endptr; + long res = strtol(stutter_check, &endptr, 10); + if (*endptr || res < 0 || res > 8) + throw + std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); + return res; + } + else + { + return 8; // The best variant, according to our benchmarks. + } + } + + bool + is_stutter_invariant(const ltl::formula* f) + { + if (f->is_ltl_formula() && f->is_X_free()) + return true; + + int algo = default_stutter_check_algorithm(); + + if (algo == 0) // Etessami's check via syntactic transformation. + { + if (!f->is_ltl_formula()) + throw std::runtime_error("Cannot use the syntactic " + "stutter-invariance check " + "for non-LTL formulas"); + const ltl::formula* g = remove_x(f); + ltl::ltl_simplifier ls; + bool res = ls.are_equivalent(f, g); + g->destroy(); + return res; + } + + // Prepare for an automata-based check. + const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone()); + translator trans; + auto aut_f = trans.run(f); + auto aut_nf = trans.run(nf); + bdd aps = atomic_prop_collect_as_bdd(f, aut_f); + nf->destroy(); + return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps, algo); + } + + bool + is_stutter_invariant(tgba_digraph_ptr&& aut_f, + tgba_digraph_ptr&& aut_nf, bdd aps, int algo) + { + if (algo == 0) + algo = default_stutter_check_algorithm(); + + switch (algo) + { + case 1: // sl(aut_f) x sl(aut_nf) + return product(sl(std::move(aut_f), aps), + sl(std::move(aut_nf), aps))->is_empty(); + case 2: // sl(cl(aut_f)) x aut_nf + return product(sl(closure(std::move(aut_f)), aps), + std::move(aut_nf))->is_empty(); + case 3: // (cl(sl(aut_f)) x aut_nf + return product(closure(sl(std::move(aut_f), aps)), + std::move(aut_nf))->is_empty(); + case 4: // sl2(aut_f) x sl2(aut_nf) + return product(sl2(std::move(aut_f), aps), + sl2(std::move(aut_nf), aps))->is_empty(); + case 5: // sl2(cl(aut_f)) x aut_nf + return product(sl2(closure(std::move(aut_f)), aps), + std::move(aut_nf))->is_empty(); + case 6: // (cl(sl2(aut_f)) x aut_nf + return product(closure(sl2(std::move(aut_f), aps)), + std::move(aut_nf))->is_empty(); + case 7: // on-the-fly sl(aut_f) x sl(aut_nf) + return otf_product(make_tgbasl(aut_f, aps), + make_tgbasl(aut_nf, aps))->is_empty(); + case 8: // cl(aut_f) x cl(aut_nf) + return product(closure(std::move(aut_f)), + closure(std::move(aut_nf)))->is_empty(); + default: + throw std::runtime_error("invalid algorithm number for " + "is_stutter_invariant()"); + SPOT_UNREACHABLE(); + } + } +} diff --git a/src/tgbaalgos/stutterize.hh b/src/tgbaalgos/stutter.hh similarity index 67% rename from src/tgbaalgos/stutterize.hh rename to src/tgbaalgos/stutter.hh index f4bc6b86a..e0c54efd2 100644 --- a/src/tgbaalgos/stutterize.hh +++ b/src/tgbaalgos/stutter.hh @@ -1,9 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche +// Copyright (C) 2014, 2015 Laboratoire de Recherche // et Développement de l'Epita (LRDE). -// Copyright (C) 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. // @@ -20,8 +17,8 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#ifndef SPOT_TGBAALGOS_STUTTERIZE_HH -# define SPOT_TGBAALGOS_STUTTERIZE_HH +#ifndef SPOT_TGBAALGOS_STUTTER_HH +# define SPOT_TGBAALGOS_STUTTER_HH #include "tgba/tgbagraph.hh" @@ -43,6 +40,24 @@ namespace spot SPOT_API tgba_digraph_ptr sl2(tgba_digraph_ptr&&, bdd = bddfalse); #endif + + SPOT_API tgba_digraph_ptr + closure(const const_tgba_digraph_ptr&); + +#ifndef SWIG + SPOT_API tgba_digraph_ptr + closure(tgba_digraph_ptr&&); +#endif + + /// \ingroup ltl_misc + /// \brief Check if a formula has the stutter invariance property. + SPOT_API bool + is_stutter_invariant(const ltl::formula* f); + + SPOT_API bool + is_stutter_invariant(tgba_digraph_ptr&& aut_f, + tgba_digraph_ptr&& aut_nf, bdd aps, + int algo = 0); } -#endif +#endif // SPOT_TGBAALGOS_STUTTER_HH diff --git a/src/tgbaalgos/stutter_invariance.cc b/src/tgbaalgos/stutter_invariance.cc deleted file mode 100644 index 3e0e0e778..000000000 --- a/src/tgbaalgos/stutter_invariance.cc +++ /dev/null @@ -1,125 +0,0 @@ -// Copyright (C) 2014 Laboratoire de Recherche et Développement -// de l'Epita. -// -// 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 3 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 this program. If not, see . - - -#include -#include "tgba/tgbagraph.hh" -#include "closure.hh" -#include "stutterize.hh" -#include "ltlvisit/remove_x.hh" -#include "tgbaalgos/translate.hh" -#include "ltlast/allnodes.hh" -#include "ltlvisit/apcollect.hh" -#include "stutter_invariance.hh" -#include "tgba/tgbasl.hh" -#include "tgba/tgbaproduct.hh" -#include "tgbaalgos/dupexp.hh" - -namespace spot -{ - // The stutter check algorithm to use can be overridden via an - // environment variable. - static int default_stutter_check_algorithm() - { - static const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); - if (stutter_check) - { - char* endptr; - long res = strtol(stutter_check, &endptr, 10); - if (*endptr || res < 0 || res > 8) - throw - std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); - return res; - } - else - { - return 8; // The best variant, according to our benchmarks. - } - } - - bool - is_stutter_invariant(const ltl::formula* f) - { - if (f->is_ltl_formula() && f->is_X_free()) - return true; - - int algo = default_stutter_check_algorithm(); - - if (algo == 0) // Etessami's check via syntactic transformation. - { - if (!f->is_ltl_formula()) - throw std::runtime_error("Cannot use the syntactic " - "stutter-invariance check " - "for non-LTL formulas"); - const ltl::formula* g = remove_x(f); - ltl::ltl_simplifier ls; - bool res = ls.are_equivalent(f, g); - g->destroy(); - return res; - } - - // Prepare for an automata-based check. - const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone()); - translator trans; - auto aut_f = trans.run(f); - auto aut_nf = trans.run(nf); - bdd aps = atomic_prop_collect_as_bdd(f, aut_f); - nf->destroy(); - return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps, algo); - } - - bool - is_stutter_invariant(tgba_digraph_ptr&& aut_f, - tgba_digraph_ptr&& aut_nf, bdd aps, int algo) - { - if (algo == 0) - algo = default_stutter_check_algorithm(); - - switch (algo) - { - case 1: // sl(aut_f) x sl(aut_nf) - return product(sl(std::move(aut_f), aps), - sl(std::move(aut_nf), aps))->is_empty(); - case 2: // sl(cl(aut_f)) x aut_nf - return product(sl(closure(std::move(aut_f)), aps), - std::move(aut_nf))->is_empty(); - case 3: // (cl(sl(aut_f)) x aut_nf - return product(closure(sl(std::move(aut_f), aps)), - std::move(aut_nf))->is_empty(); - case 4: // sl2(aut_f) x sl2(aut_nf) - return product(sl2(std::move(aut_f), aps), - sl2(std::move(aut_nf), aps))->is_empty(); - case 5: // sl2(cl(aut_f)) x aut_nf - return product(sl2(closure(std::move(aut_f)), aps), - std::move(aut_nf))->is_empty(); - case 6: // (cl(sl2(aut_f)) x aut_nf - return product(closure(sl2(std::move(aut_f), aps)), - std::move(aut_nf))->is_empty(); - case 7: // on-the-fly sl(aut_f) x sl(aut_nf) - return product(make_tgbasl(aut_f, aps), - make_tgbasl(aut_nf, aps))->is_empty(); - case 8: // cl(aut_f) x cl(aut_nf) - return product(closure(std::move(aut_f)), - closure(std::move(aut_nf)))->is_empty(); - default: - throw std::runtime_error("invalid algorithm number for " - "is_stutter_invariant()"); - SPOT_UNREACHABLE(); - } - } -} diff --git a/src/tgbaalgos/stutter_invariance.hh b/src/tgbaalgos/stutter_invariance.hh deleted file mode 100644 index 2edbcfff3..000000000 --- a/src/tgbaalgos/stutter_invariance.hh +++ /dev/null @@ -1,38 +0,0 @@ -// Copyright (C) 2014 Laboratoire de Recherche et Développement -// de l'Epita. -// -// 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 3 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 this program. If not, see . - - -#ifndef SPOT_TGBAALGOS_STUTTER_INVARIANCE_HH -# define SPOT_TGBAALGOS_STUTTER_INVARIANCE_HH - -#include "tgba/tgbagraph.hh" - -namespace spot -{ - /// \ingroup ltl_misc - /// \brief Check if a formula has the stutter invariance property. - SPOT_API bool - is_stutter_invariant(const ltl::formula* f); - - SPOT_API bool - is_stutter_invariant(tgba_digraph_ptr&& aut_f, - tgba_digraph_ptr&& aut_nf, bdd aps, - int algo = 0); -} - -#endif diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc deleted file mode 100644 index 7aee575ca..000000000 --- a/src/tgbaalgos/stutterize.cc +++ /dev/null @@ -1,193 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 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 3 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 this program. If not, see . - -#include "stutterize.hh" -#include "tgba/tgba.hh" -#include "dupexp.hh" -#include "misc/hash.hh" -#include "misc/hashfunc.hh" -#include "ltlvisit/apcollect.hh" -#include -#include -#include -#include - -namespace spot -{ - namespace - { - typedef std::pair stutter_state; - - struct stutter_state_hash - { - size_t - operator()(const stutter_state& s) const - { - return wang32_hash(s.first) ^ wang32_hash(s.second.id()); - } - }; - - // Associate the stutter state to its number. - typedef std::unordered_map ss2num_map; - - // Queue of state to be processed. - typedef std::deque queue_t; - } - - static bdd - get_all_ap(const const_tgba_digraph_ptr& a) - { - bdd res = bddtrue; - for (auto& i: a->transitions()) - res &= bdd_support(i.cond); - return res; - } - - tgba_digraph_ptr - sl(const const_tgba_digraph_ptr& a, const ltl::formula* f) - { - bdd aps = f - ? atomic_prop_collect_as_bdd(f, a) - : get_all_ap(a); - return sl(a, aps); - } - - tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f) - { - bdd aps = f - ? atomic_prop_collect_as_bdd(f, a) - : get_all_ap(a); - return sl2(a, aps); - } - - tgba_digraph_ptr - sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions) - { - // The result automaton uses numbered states. - tgba_digraph_ptr res = make_tgba_digraph(a->get_dict()); - // We use the same BDD variables as the input. - res->copy_ap_of(a); - res->copy_acceptance_conditions_of(a); - // These maps make it possible to convert stutter_state to number - // and vice-versa. - ss2num_map ss2num; - - queue_t todo; - - unsigned s0 = a->get_init_state_number(); - stutter_state s(s0, bddfalse); - ss2num[s] = 0; - res->new_state(); - todo.push_back(s); - - while (!todo.empty()) - { - s = todo.front(); - todo.pop_front(); - unsigned src = ss2num[s]; - - bool self_loop_needed = true; - - for (auto& t : a->out(s.first)) - { - bdd all = t.cond; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - all -= one; - - stutter_state d(t.dst, one); - - auto r = ss2num.emplace(d, ss2num.size()); - unsigned dest = r.first->second; - - if (r.second) - { - todo.push_back(d); - unsigned u = res->new_state(); - assert(u == dest); - (void)u; - } - - // Create the transition. - res->new_transition(src, dest, one, t.acc); - - if (src == dest) - self_loop_needed = false; - } - } - - if (self_loop_needed && s.second != bddfalse) - res->new_transition(src, src, s.second, 0U); - } - res->merge_transitions(); - return res; - } - - tgba_digraph_ptr - sl2(tgba_digraph_ptr&& a, bdd atomic_propositions) - { - if (atomic_propositions == bddfalse) - atomic_propositions = get_all_ap(a); - unsigned num_states = a->num_states(); - unsigned num_transitions = a->num_transitions(); - for (unsigned src = 0; src < num_states; ++src) - { - auto trans = a->out(src); - - for (auto it = trans.begin(); it != trans.end() - && it.trans() <= num_transitions; ++it) - if (it->dst != src) - { - bdd all = it->cond; - while (all != bddfalse) - { - unsigned dst = it->dst; - bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - unsigned tmp = a->new_state(); - unsigned i = a->new_transition(src, tmp, one, it->acc); - assert(i > num_transitions); - i = a->new_transition(tmp, tmp, one, 0U); - assert(i > num_transitions); - // No acceptance here to preserve the state-based property. - i = a->new_transition(tmp, dst, one, 0U); - assert(i > num_transitions); - all -= one; - } - } - } - if (num_states != a->num_states()) - a->prop_keep({true, // state_based - true, // single_acc - false, // inherently_weak - false, // deterministic - }); - a->merge_transitions(); - return a; - } - - tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) - { - return sl2(make_tgba_digraph(a, tgba::prop_set::all()), - atomic_propositions); - } -} diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 3613cdd61..094b746fe 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique // de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -131,8 +131,7 @@ namespace std { #include "tgbaalgos/isdet.hh" #include "tgbaalgos/simulation.hh" #include "tgbaalgos/postproc.hh" -#include "tgbaalgos/closure.hh" -#include "tgbaalgos/stutterize.hh" +#include "tgbaalgos/stutter.hh" #include "tgbaparse/public.hh" @@ -265,8 +264,7 @@ namespace spot { %include "tgbaalgos/isdet.hh" %include "tgbaalgos/simulation.hh" %include "tgbaalgos/postproc.hh" -%include "tgbaalgos/closure.hh" -%include "tgbaalgos/stutterize.hh" +%include "tgbaalgos/stutter.hh" %include "tgbaparse/public.hh"