From 5a706300b0bd37d46ebe671298ce4ac66845eb8a Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Tue, 10 Apr 2012 23:30:03 +0200 Subject: [PATCH] Stable version of TGTA approach implementation (automaton + product) * src/ta/tgta.hh, src/ta/tgta.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/ta/tgtaproduct.cc, src/taalgos/minimize.cc, src/taalgos/minimize.hh, src/taalgos/emptinessta.hh, src/taalgos/emptinessta.hh, src/taalgos/emptinessta.cc, src/taalgos/tgba2ta.hh, src/taalgos/tgba2ta.cc: rename tgbta to tgta in this source files. * src/ta/tgbtaexplicit.hh, src/ta/tgbtaproduct.hh, src/ta/tgbta.cc, src/ta/tgbtaproduct.cc, src/ta/tgbta.hh, src/ta/tgbtaexplicit.cc: Rename as... * src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgtaexplicit.cc: ... these. * src/taalgos/sba2ta.hh, src/taalgos/sba2ta.cc: deleted because the implementation of all the transformations beteween TGBA and the different forms of TA are new implemented in src/taalgos/tgba2ta.hh and src/taalgos/tgba2ta.cc. * src/tgbatest/ltl2tgba.cc: rename the options of commands that build the different forms of TA. * src/ta/ta.hh: BUG Fix * src/ta/Makefile.am, src/tgbatest/ltl2ta.test: impacts of this renaming --- src/ta/Makefile.am | 12 +- src/ta/ta.hh | 8 +- src/ta/taexplicit.cc | 31 +- src/ta/taexplicit.hh | 1 + src/ta/taproduct.cc | 71 +- src/ta/taproduct.hh | 28 +- src/ta/tgbta.hh | 44 - src/ta/tgbtaexplicit.cc | 98 --- src/ta/{tgbta.cc => tgta.cc} | 6 +- src/ta/tgta.hh | 85 ++ src/ta/tgtaexplicit.cc | 97 +++ src/ta/{tgbtaexplicit.hh => tgtaexplicit.hh} | 54 +- src/ta/{tgbtaproduct.cc => tgtaproduct.cc} | 84 +- src/ta/{tgbtaproduct.hh => tgtaproduct.hh} | 22 +- src/taalgos/emptinessta.cc | 2 +- src/taalgos/emptinessta.hh | 31 +- src/taalgos/minimize.cc | 573 +++++++------ src/taalgos/minimize.hh | 45 +- src/taalgos/sba2ta.cc | 454 ---------- src/taalgos/sba2ta.hh | 49 -- src/taalgos/tgba2ta.cc | 859 ++++++++++--------- src/taalgos/tgba2ta.hh | 63 +- src/tgbatest/ltl2ta.test | 101 ++- src/tgbatest/ltl2tgba.cc | 70 +- 24 files changed, 1308 insertions(+), 1580 deletions(-) delete mode 100644 src/ta/tgbta.hh delete mode 100644 src/ta/tgbtaexplicit.cc rename src/ta/{tgbta.cc => tgta.cc} (93%) create mode 100644 src/ta/tgta.hh create mode 100644 src/ta/tgtaexplicit.cc rename src/ta/{tgbtaexplicit.hh => tgtaexplicit.hh} (50%) rename src/ta/{tgbtaproduct.cc => tgtaproduct.cc} (70%) rename src/ta/{tgbtaproduct.hh => tgtaproduct.hh} (81%) delete mode 100644 src/taalgos/sba2ta.cc delete mode 100644 src/taalgos/sba2ta.hh diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am index 75b4df8bd..b2e65c39d 100644 --- a/src/ta/Makefile.am +++ b/src/ta/Makefile.am @@ -27,16 +27,16 @@ ta_HEADERS = \ ta.hh \ taexplicit.hh \ taproduct.hh \ - tgbta.hh \ - tgbtaexplicit.hh \ - tgbtaproduct.hh + tgta.hh \ + tgtaexplicit.hh \ + tgtaproduct.hh noinst_LTLIBRARIES = libta.la libta_la_SOURCES = \ ta.cc \ taproduct.cc \ - tgbta.cc \ - tgbtaexplicit.cc \ + tgta.cc \ + tgtaexplicit.cc \ taexplicit.cc \ - tgbtaproduct.cc + tgtaproduct.cc diff --git a/src/ta/ta.hh b/src/ta/ta.hh index a589a13a7..f4ec39909 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -51,7 +51,7 @@ namespace spot /// /// The Testing Automata (TA) were introduced by /// Henri Hansen, Wojciech Penczek and Antti Valmari - /// in "Stuttering-insensitive automata for on-the-fly de- tection of livelock + /// in "Stuttering-insensitive automata for on-the-fly detection of livelock /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in /// Theoretical Computer Science.Elsevier. /// @@ -69,7 +69,7 @@ namespace spot /// Browsing such automaton can be achieved using two functions: /// \c get_initial_states_set or \c get_artificial_initial_state, and \c /// succ_iter. The former returns the initial state(s) while the latter lists - /// the successor states of any state (filtred by transition "changeset"). + /// the successor states of any state (filtred by "changeset"). /// /// Note that although this is a transition-based automata, /// we never represent transitions! Transition informations are @@ -98,7 +98,7 @@ namespace spot /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (For more details, see the paper cited above) - spot::state* + virtual spot::state* get_artificial_initial_state() const { return 0; @@ -114,7 +114,7 @@ namespace spot succ_iter(const spot::state* state) const = 0; /// \brief Get an iterator over the successors of \a state - /// filtred by the changeset labeling the transitions + /// filtred by the changeset on transitions /// /// The iterator has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index cd1e24d1b..651866316 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -105,7 +105,6 @@ namespace spot return (*i_)->acceptance_conditions; } - //////////////////////////////////////// // state_ta_explicit @@ -141,19 +140,19 @@ namespace spot if (transitions_ == 0) transitions_ = new transitions; - transitions* transitions_condition = get_transitions(t->condition); + transitions* trans_by_condition = get_transitions(t->condition); - if (transitions_condition == 0) + if (trans_by_condition == 0) { - transitions_condition = new transitions; - transitions_by_condition[(t->condition).id()] = transitions_condition; + trans_by_condition = new transitions; + transitions_by_condition[(t->condition).id()] = trans_by_condition; } state_ta_explicit::transitions::iterator it_trans; bool transition_found = false; - for (it_trans = transitions_condition->begin(); (it_trans - != transitions_condition->end() && !transition_found); it_trans++) + for (it_trans = trans_by_condition->begin(); (it_trans + != trans_by_condition->end() && !transition_found); it_trans++) { transition_found = ((*it_trans)->dest == t->dest); if (transition_found) @@ -166,12 +165,12 @@ namespace spot { if (add_at_beginning) { - transitions_condition->push_front(t); + trans_by_condition->push_front(t); transitions_->push_front(t); } else { - transitions_condition->push_back(t); + trans_by_condition->push_back(t); transitions_->push_back(t); } @@ -290,11 +289,16 @@ namespace spot == (dest)->get_tgba_condition()); bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); - //Before deleting stuttering transitions, propaged back livelock and initial state's properties + //Before deleting stuttering transitions, propaged back livelock + //and initial state's properties if (is_stuttering_transition) { - if (dest_is_livelock_accepting) - set_livelock_accepting_state(true); + if (!is_livelock_accepting_state() && dest_is_livelock_accepting) + { + set_livelock_accepting_state(true); + stuttering_reachable_livelock + = dest->stuttering_reachable_livelock; + } if (dest->is_initial_state()) set_initial_state(true); } @@ -321,7 +325,7 @@ namespace spot void state_ta_explicit::free_transitions() { - state_ta_explicit::transitions* trans = get_transitions(); + state_ta_explicit::transitions* trans = transitions_; state_ta_explicit::transitions::iterator it_trans; // We don't destroy the transitions in the state's destructor because // they are not cloned. @@ -340,6 +344,7 @@ namespace spot ++i; } + transitions_ = 0; } //////////////////////////////////////// diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index 1d81c2247..42f5d16f0 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -227,6 +227,7 @@ namespace spot void free_transitions(); + state_ta_explicit* stuttering_reachable_livelock; private: const state* tgba_state_; const bdd tgba_condition_; diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index bca321a60..a131ca872 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -81,7 +81,6 @@ namespace spot ta_succ_iterator_product::~ta_succ_iterator_product() { - // ta_->free_state(current_state_); delete current_state_; current_state_ = 0; delete ta_succ_it_; @@ -315,6 +314,17 @@ namespace spot return new ta_succ_iterator_product(stp, ta_, kripke_); } + + ta_succ_iterator_product* + ta_product::succ_iter(const spot::state* s, bdd changeset) const + { + const state_ta_product* stp = down_cast (s); + assert(s); + return new ta_succ_iterator_product_by_changeset(stp, ta_, kripke_, + changeset); + + } + bdd_dict* ta_product::get_dict() const { @@ -349,6 +359,7 @@ namespace spot } + bool ta_product::is_initial_state(const spot::state* s) const { @@ -400,4 +411,62 @@ namespace spot } + + ta_succ_iterator_product_by_changeset::ta_succ_iterator_product_by_changeset( + const state_ta_product* s, const ta* t, const kripke* k, bdd changeset) : + ta_succ_iterator_product(s, t, k) + { + current_condition_ = changeset; + } + + + + + void + ta_succ_iterator_product_by_changeset::next_kripke_dest() + { + if (!kripke_succ_it_) + return; + + if (kripke_current_dest_state == 0) + { + kripke_succ_it_->first(); + } + else + { + kripke_current_dest_state->destroy(); + kripke_current_dest_state = 0; + kripke_succ_it_->next(); + } + + // If one of the two successor sets is empty initially, we reset + // kripke_succ_it_, so that done() can detect this situation easily. (We + // choose to reset kripke_succ_it_ because this variable is already used by + // done().) + if (kripke_succ_it_->done()) + { + delete kripke_succ_it_; + kripke_succ_it_ = 0; + return; + } + + kripke_current_dest_state = kripke_succ_it_->current_state(); + bdd kripke_current_dest_condition = kripke_->state_condition( + kripke_current_dest_state); + + if (current_condition_ != bdd_setxor(kripke_source_condition, + kripke_current_dest_condition)) + next_kripke_dest(); + is_stuttering_transition_ = (kripke_source_condition + == kripke_current_dest_condition); + if (!is_stuttering_transition_) + { + ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), + current_condition_); + ta_succ_it_->first(); + } + + } + + } diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index 8a41fd1b3..a984f0b69 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -28,7 +28,7 @@ namespace spot { /// \brief A state for spot::ta_product. - /// \ingroup emptiness_check + /// \ingroup ta_emptiness_check /// /// This state is in fact a pair of state: the state from the TA /// automaton and that of Kripke structure. @@ -104,7 +104,7 @@ namespace spot bool is_stuttering_transition() const; - private: + protected: //@{ /// Internal routines to advance to the next successor. void @@ -135,7 +135,7 @@ namespace spot /// \brief A lazy product between a Testing automaton and a Kripke structure. /// (States are computed on the fly.) - /// \ingroup emptiness_check + /// \ingroup ta_emptiness_check class ta_product : public ta { public: @@ -153,6 +153,9 @@ namespace spot virtual ta_succ_iterator_product* succ_iter(const spot::state* s) const; + virtual ta_succ_iterator_product* + succ_iter(const spot::state* s, bdd changeset) const; + virtual bdd_dict* get_dict() const; @@ -169,7 +172,7 @@ namespace spot is_initial_state(const spot::state* s) const; /// \brief Return true if the state \a s has no succeseurs - /// in the ta automaton (the TA component of the product automaton) + /// in the TA automaton (the TA component of the product automaton) virtual bool is_hole_state_in_ta_component(const spot::state* s) const; @@ -205,6 +208,23 @@ namespace spot operator=(const ta_product&); }; + + class ta_succ_iterator_product_by_changeset : public ta_succ_iterator_product + { + public: + ta_succ_iterator_product_by_changeset(const state_ta_product* s, + const ta* t, const kripke* k, bdd changeset); + + + + /// \brief Move to the next successor in the kripke structure + void + next_kripke_dest(); + + + }; + + } #endif // SPOT_TA_TAPRODUCT_HH diff --git a/src/ta/tgbta.hh b/src/ta/tgbta.hh deleted file mode 100644 index e6a915405..000000000 --- a/src/ta/tgbta.hh +++ /dev/null @@ -1,44 +0,0 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita_explicit (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 MERCHANta_explicitBILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more deta_explicitils. -// -// 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_TA_TGBTA_HH -# define SPOT_TA_TGBTA_HH - -#include "tgba/tgba.hh" - -namespace spot -{ - class tgbta : public tgba - { - - protected: - tgbta(); - public: - - virtual - ~tgbta(); - virtual tgba_succ_iterator* - succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0; - - }; - -} - -#endif // SPOT_TA_TGBTA_HH diff --git a/src/ta/tgbtaexplicit.cc b/src/ta/tgbtaexplicit.cc deleted file mode 100644 index 8f94317c2..000000000 --- a/src/ta/tgbtaexplicit.cc +++ /dev/null @@ -1,98 +0,0 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// 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 "ltlast/atomic_prop.hh" -#include "ltlast/constant.hh" -#include "tgbtaexplicit.hh" -#include "tgba/formula2bdd.hh" -#include "misc/bddop.hh" -#include "ltlvisit/tostring.hh" - -#include "tgba/bddprint.hh" - -namespace spot -{ - - - tgbta_explicit::tgbta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state) : - ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state) - { - } - - - state* - tgbta_explicit::get_init_state() const - { - return ta_explicit::get_artificial_initial_state(); - } - - tgba_succ_iterator* - tgbta_explicit::succ_iter(const spot::state* state, - const spot::state*, - const tgba*) const - { - return ta_explicit::succ_iter(state); - } - - bdd - tgbta_explicit::compute_support_conditions(const spot::state* in) const - { - return get_tgba()->support_conditions(((const state_ta_explicit*) in)->get_tgba_state()); - } - - bdd - tgbta_explicit::compute_support_variables(const spot::state* in) const - { - return get_tgba()->support_variables(((const state_ta_explicit*) in)->get_tgba_state()); - } - - bdd_dict* - tgbta_explicit::get_dict() const - { - return ta_explicit::get_dict(); - } - - bdd - tgbta_explicit::all_acceptance_conditions() const - { - - return ta_explicit::all_acceptance_conditions(); - } - - bdd - tgbta_explicit::neg_acceptance_conditions() const - { - return get_tgba()->neg_acceptance_conditions(); - } - - std::string - tgbta_explicit::format_state(const spot::state* s) const - { - return ta_explicit::format_state(s); - } - - - spot::tgba_succ_iterator* tgbta_explicit::succ_iter_by_changeset(const spot::state* s, bdd change_set) const - { - return ta_explicit::succ_iter(s,change_set); - } - -} diff --git a/src/ta/tgbta.cc b/src/ta/tgta.cc similarity index 93% rename from src/ta/tgbta.cc rename to src/ta/tgta.cc index 14734d800..981afe4d1 100644 --- a/src/ta/tgbta.cc +++ b/src/ta/tgta.cc @@ -18,15 +18,15 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "tgbta.hh" +#include "tgta.hh" namespace spot { - tgbta::tgbta() + tgta::tgta() {}; - tgbta::~tgbta() + tgta::~tgta() {}; diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh new file mode 100644 index 000000000..e54a726d2 --- /dev/null +++ b/src/ta/tgta.hh @@ -0,0 +1,85 @@ +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement +// de l Epita_explicit (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 MERCHANta_explicitBILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more deta_explicitils. +// +// 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_TA_TGBTA_HH +# define SPOT_TA_TGBTA_HH + +#include "tgba/tgba.hh" + +namespace spot +{ + + /// \brief A Transition-based Generalized Testing Automaton (TGTA). + /// \ingroup ta_essentials + /// + /// Transition-based Generalized Testing Automaton (TGTA) is a new kind of + /// automaton that combines features from both TA and TGBA. + /// From TA, we take the idea of labeling transitions with changesets, + /// however we remove the use of livelock-acceptance (because it may require + /// a two-pass emptiness check), and the implicit stuttering. From TGBA, we + /// inherit the use of transition-based generalized acceptance conditions. + /// The resulting Chimera, which we call \emph{Transition-based + /// Generalized Testing Automaton} (TGTA), accepts only + /// stuttering-insensitive languages like TA, and inherits advantages from + /// both TA and TGBA: it has a simple one-pass emptiness-check procedure + /// (the same as algorithm the one for TGBA), and can benefit from reductions + /// based on the stuttering of the properties pretty much like a TA. + /// Livelock acceptance states, which are no longer supported are emulated + ///using states with a Büchi accepting self-loop labeled by empty changeset. + /// + /// Browsing such automaton can be achieved using two functions: + /// \c get_initial_state and \c + /// succ_iter. The former returns the initial state(s) while the latter lists + /// the successor states of any state. A second implementation of \c succ_iter + /// returns only the successors reached through a changeset passed as + /// a parameter. + /// + /// Note that although this is a transition-based automata, + /// we never represent transitions! Transition informations are + /// obtained by querying the iterator over the successors of + /// a state. + + + class tgta : public tgba + { + + protected: + tgta(); + public: + + virtual + ~tgta(); + + /// \brief Get an iterator over the successors of \a state + /// filtred by the value of the changeset on transitions between the + /// \a state and his successors + /// + /// The iterator has been allocated with \c new. It is the + /// responsability of the caller to \c delete it when no + /// longer needed. + /// + virtual tgba_succ_iterator* + succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0; + + }; + +} + +#endif // SPOT_TA_TGBTA_HH diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc new file mode 100644 index 000000000..6d6465a91 --- /dev/null +++ b/src/ta/tgtaexplicit.cc @@ -0,0 +1,97 @@ +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement +// 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 "ltlast/atomic_prop.hh" +#include "ltlast/constant.hh" +#include "tgtaexplicit.hh" +#include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" +#include "ltlvisit/tostring.hh" + +#include "tgba/bddprint.hh" + +namespace spot +{ + + tgta_explicit::tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, + state_ta_explicit* artificial_initial_state) : + ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state) + { + } + + state* + tgta_explicit::get_init_state() const + { + return ta_explicit::get_artificial_initial_state(); + } + + tgba_succ_iterator* + tgta_explicit::succ_iter(const spot::state* state, const spot::state*, + const tgba*) const + { + return ta_explicit::succ_iter(state); + } + + bdd + tgta_explicit::compute_support_conditions(const spot::state* in) const + { + return get_tgba()->support_conditions( + ((const state_ta_explicit*) in)->get_tgba_state()); + } + + bdd + tgta_explicit::compute_support_variables(const spot::state* in) const + { + return get_tgba()->support_variables( + ((const state_ta_explicit*) in)->get_tgba_state()); + } + + bdd_dict* + tgta_explicit::get_dict() const + { + return ta_explicit::get_dict(); + } + + bdd + tgta_explicit::all_acceptance_conditions() const + { + + return ta_explicit::all_acceptance_conditions(); + } + + bdd + tgta_explicit::neg_acceptance_conditions() const + { + return get_tgba()->neg_acceptance_conditions(); + } + + std::string + tgta_explicit::format_state(const spot::state* s) const + { + return ta_explicit::format_state(s); + } + + spot::tgba_succ_iterator* + tgta_explicit::succ_iter_by_changeset(const spot::state* s, bdd chngset) const + { + return ta_explicit::succ_iter(s, chngset); + } + +} diff --git a/src/ta/tgbtaexplicit.hh b/src/ta/tgtaexplicit.hh similarity index 50% rename from src/ta/tgbtaexplicit.hh rename to src/ta/tgtaexplicit.hh index 68f659704..366e8686e 100644 --- a/src/ta/tgbtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -18,8 +18,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TA_TGBTAEXPLICIT_HH -# define SPOT_TA_TGBTAEXPLICIT_HH +#ifndef SPOT_TA_TGTAEXPLICIT_HH +# define SPOT_TA_TGTAEXPLICIT_HH #include "misc/hash.hh" #include @@ -29,38 +29,46 @@ #include #include "misc/bddlt.hh" #include "taexplicit.hh" -#include "tgbta.hh" +#include "tgta.hh" namespace spot { - class tgbta_explicit : public tgbta, public ta_explicit + + /// Explicit representation of a spot::tgta. + /// \ingroup ta_representation + class tgta_explicit : public tgta, public ta_explicit { public: - tgbta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state) ; + tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, + state_ta_explicit* artificial_initial_state); - // tgba interface - virtual spot::state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const spot::state* local_state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const; - virtual bdd_dict* get_dict() const; + // tgba interface + virtual spot::state* + get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const spot::state* local_state, const spot::state* global_state = + 0, const tgba* global_automaton = 0) const; + virtual bdd_dict* + get_dict() const; - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; + virtual bdd + all_acceptance_conditions() const; + virtual bdd + neg_acceptance_conditions() const; - virtual std::string format_state(const spot::state* s) const; + virtual std::string + format_state(const spot::state* s) const; - virtual tgba_succ_iterator* succ_iter_by_changeset(const spot::state* s, bdd change_set) const; - protected: - virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; + virtual tgba_succ_iterator* + succ_iter_by_changeset(const spot::state* s, bdd change_set) const; + protected: + virtual bdd + compute_support_conditions(const spot::state* state) const; + virtual bdd + compute_support_variables(const spot::state* state) const; }; - - } -#endif // SPOT_TA_TGBTAEXPLICIT_HH +#endif // SPOT_TA_TGTAEXPLICIT_HH diff --git a/src/ta/tgbtaproduct.cc b/src/ta/tgtaproduct.cc similarity index 70% rename from src/ta/tgbtaproduct.cc rename to src/ta/tgtaproduct.cc index 878478504..bdbec7325 100644 --- a/src/ta/tgbtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -28,7 +28,7 @@ #define trace while (0) std::clog #endif -#include "tgbtaproduct.hh" +#include "tgtaproduct.hh" #include #include #include "misc/hashfunc.hh" @@ -38,19 +38,19 @@ namespace spot { //////////////////////////////////////////////////////////// - // tgbta_succ_iterator_product + // tgta_succ_iterator_product //////////////////////////////////////////////////////////// - // tgbta_product + // tgta_product - tgbta_product::tgbta_product(const kripke* left, const tgbta* right) : + tgta_product::tgta_product(const kripke* left, const tgta* right) : tgba_product(left, right) { } state* - tgbta_product::get_init_state() const + tgta_product::get_init_state() const { fixed_size_pool* p = const_cast (&pool_); return new (p->allocate()) state_product(left_->get_init_state(), @@ -58,7 +58,7 @@ namespace spot } tgba_succ_iterator* - tgbta_product::succ_iter(const state* local_state, const state*, + tgta_product::succ_iter(const state* local_state, const state*, const tgba*) const { const state_product* s = down_cast (local_state); @@ -66,20 +66,20 @@ namespace spot fixed_size_pool* p = const_cast (&pool_); - return new tgbta_succ_iterator_product(s, (const kripke*) left_, - (const tgbta *) right_, p); + return new tgta_succ_iterator_product(s, (const kripke*) left_, + (const tgta *) right_, p); } //////////////////////////////////////////////////////////// - // tgbtgbta_succ_iterator_product - tgbta_succ_iterator_product::tgbta_succ_iterator_product( - const state_product* s, const kripke* k, const tgbta* t, + // tgbtgta_succ_iterator_product + tgta_succ_iterator_product::tgta_succ_iterator_product( + const state_product* s, const kripke* k, const tgta* t, fixed_size_pool* pool) : - source_(s), tgbta_(t), kripke_(k), pool_(pool) + source_(s), tgta_(t), kripke_(k), pool_(pool) { - state * tgbta_init_state = tgbta_->get_init_state(); - if ((s->right())->compare(tgbta_init_state) == 0) + state * tgta_init_state = tgta_->get_init_state(); + if ((s->right())->compare(tgta_init_state) == 0) source_ = 0; if (source_ == 0) @@ -88,11 +88,11 @@ namespace spot kripke_current_dest_state = kripke_->get_init_state(); current_condition_ = kripke_->state_condition(kripke_current_dest_state); - tgbta_succ_it_ = tgbta_->succ_iter_by_changeset( - tgbta_init_state, current_condition_); - tgbta_succ_it_->first(); + tgta_succ_it_ = tgta_->succ_iter_by_changeset( + tgta_init_state, current_condition_); + tgta_succ_it_->first(); trace - << "*** tgbta_succ_it_->done() = ***" << tgbta_succ_it_->done() + << "*** tgta_succ_it_->done() = ***" << tgta_succ_it_->done() << std::endl; } @@ -101,40 +101,40 @@ namespace spot kripke_source_condition = kripke_->state_condition(s->left()); kripke_succ_it_ = kripke_->succ_iter(s->left()); kripke_current_dest_state = 0; - tgbta_succ_it_ = 0; + tgta_succ_it_ = 0; } - tgbta_init_state->destroy(); + tgta_init_state->destroy(); current_state_ = 0; } - tgbta_succ_iterator_product::~tgbta_succ_iterator_product() + tgta_succ_iterator_product::~tgta_succ_iterator_product() { // ta_->free_state(current_state_); if (current_state_ != 0) current_state_->destroy(); current_state_ = 0; - delete tgbta_succ_it_; + delete tgta_succ_it_; delete kripke_succ_it_; if (kripke_current_dest_state != 0) kripke_current_dest_state->destroy(); } void - tgbta_succ_iterator_product::step_() + tgta_succ_iterator_product::step_() { - if (!tgbta_succ_it_->done()) - tgbta_succ_it_->next(); - if (tgbta_succ_it_->done()) + if (!tgta_succ_it_->done()) + tgta_succ_it_->next(); + if (tgta_succ_it_->done()) { - delete tgbta_succ_it_; - tgbta_succ_it_ = 0; + delete tgta_succ_it_; + tgta_succ_it_ = 0; next_kripke_dest(); } } void - tgbta_succ_iterator_product::next_kripke_dest() + tgta_succ_iterator_product::next_kripke_dest() { if (!kripke_succ_it_) return; @@ -167,14 +167,14 @@ namespace spot current_condition_ = bdd_setxor(kripke_source_condition, kripke_current_dest_condition); - tgbta_succ_it_ = tgbta_->succ_iter_by_changeset(source_->right(), + tgta_succ_it_ = tgta_->succ_iter_by_changeset(source_->right(), current_condition_); - tgbta_succ_it_->first(); + tgta_succ_it_->first(); } void - tgbta_succ_iterator_product::first() + tgta_succ_iterator_product::first() { next_kripke_dest(); @@ -186,7 +186,7 @@ namespace spot } void - tgbta_succ_iterator_product::next() + tgta_succ_iterator_product::next() { current_state_->destroy(); current_state_ = 0; @@ -202,18 +202,18 @@ namespace spot } void - tgbta_succ_iterator_product::find_next_succ_() + tgta_succ_iterator_product::find_next_succ_() { while (!done()) { - if (!tgbta_succ_it_->done()) + if (!tgta_succ_it_->done()) { current_state_ = new (pool_->allocate()) state_product( kripke_current_dest_state->clone(), - tgbta_succ_it_->current_state(), pool_); + tgta_succ_it_->current_state(), pool_); current_acceptance_conditions_ - = tgbta_succ_it_->current_acceptance_conditions(); + = tgta_succ_it_->current_acceptance_conditions(); return; } @@ -222,11 +222,11 @@ namespace spot } bool - tgbta_succ_iterator_product::done() const + tgta_succ_iterator_product::done() const { if (source_ == 0) { - return !tgbta_succ_it_ || tgbta_succ_it_->done(); + return !tgta_succ_it_ || tgta_succ_it_->done(); } else { @@ -236,7 +236,7 @@ namespace spot } state_product* - tgbta_succ_iterator_product::current_state() const + tgta_succ_iterator_product::current_state() const { trace << "*** current_state() .... if(done()) = ***" << done() << std::endl; @@ -244,13 +244,13 @@ namespace spot } bdd - tgbta_succ_iterator_product::current_condition() const + tgta_succ_iterator_product::current_condition() const { return current_condition_; } bdd - tgbta_succ_iterator_product::current_acceptance_conditions() const + tgta_succ_iterator_product::current_acceptance_conditions() const { return current_acceptance_conditions_; } diff --git a/src/ta/tgbtaproduct.hh b/src/ta/tgtaproduct.hh similarity index 81% rename from src/ta/tgbtaproduct.hh rename to src/ta/tgtaproduct.hh index 4ee82632c..8d77592c7 100644 --- a/src/ta/tgbtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -21,24 +21,24 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBTA_TGBAPRODUCT_HH -# define SPOT_TGBTA_TGBAPRODUCT_HH +#ifndef SPOT_tgta_TGBAPRODUCT_HH +# define SPOT_tgta_TGBAPRODUCT_HH #include "tgba/tgba.hh" #include "tgba/tgbaproduct.hh" #include "misc/fixpool.hh" #include "kripke/kripke.hh" -#include "tgbta.hh" +#include "tgta.hh" namespace spot { /// \brief A lazy product. (States are computed on the fly.) - class tgbta_product : public tgba_product + class tgta_product : public tgba_product { public: - tgbta_product(const kripke* left, const tgbta* right); + tgta_product(const kripke* left, const tgta* right); virtual state* get_init_state() const; @@ -51,13 +51,13 @@ namespace spot }; /// \brief Iterate over the successors of a product computed on the fly. - class tgbta_succ_iterator_product : public tgba_succ_iterator + class tgta_succ_iterator_product : public tgba_succ_iterator { public: - tgbta_succ_iterator_product(const state_product* s, const kripke* k, const tgbta* tgbta, fixed_size_pool* pool); + tgta_succ_iterator_product(const state_product* s, const kripke* k, const tgta* tgta, fixed_size_pool* pool); virtual - ~tgbta_succ_iterator_product(); + ~tgta_succ_iterator_product(); // iteration void @@ -91,10 +91,10 @@ namespace spot protected: const state_product* source_; - const tgbta* tgbta_; + const tgta* tgta_; const kripke* kripke_; fixed_size_pool* pool_; - tgba_succ_iterator* tgbta_succ_it_; + tgba_succ_iterator* tgta_succ_it_; tgba_succ_iterator* kripke_succ_it_; state_product* current_state_; bdd current_condition_; @@ -107,4 +107,4 @@ namespace spot } -#endif // SPOT_TGBTA_TGBAPRODUCT_HH +#endif // SPOT_tgta_TGBAPRODUCT_HH diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 14869af89..2b5099489 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -47,7 +47,7 @@ namespace spot bool ta_check::check(bool disable_second_pass, - disable_heuristic_for_livelock_detection) + bool disable_heuristic_for_livelock_detection) { // We use five main data in this algorithm: diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh index 8055ce735..68b21281a 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -39,14 +39,15 @@ namespace spot typedef std::pair pair_state_iter; } - /// \addtogroup emptiness_check Emptiness-checks + /// \addtogroup ta_emptiness_check Emptiness-checks /// \ingroup ta_algorithms /// - /// \brief Check whether the language of a product between a Kripke structure - /// and a TA is empty. It works for both standard and generalized form of TA. + /// \brief Check whether the language of a product (spot::ta_product) between + /// a Kripke structure and a TA is empty. It works also for the product + /// using Generalized TA (GTA and SGTA). /// - /// you should call \c check to check the product automaton. - /// If \c check() returns false, then the product automaton + /// you should call spot::ta_check::check() to check the product automaton. + /// If spot::ta_check::check() returns false, then the product automaton /// was found empty. Otherwise the automaton accepts some run. /// /// This is based on the following paper. @@ -64,21 +65,22 @@ namespace spot /// } /// \endverbatim /// - /// the implementation of \c check is inspired from the two-pass algorithm - /// of the paper above: + /// the implementation of spot::ta_check::check() is inspired from the + /// two-pass algorithm of the paper above: /// - the fist-pass detect all Buchi-accepting cycles and includes - // the heuristic proposed in the paper to detect some + /// the heuristic proposed in the paper to detect some /// livelock-accepting cycles. /// - the second-pass detect all livelock-accepting cycles. /// In addition, we add some optimizations to the fist pass: - /// 1- Detection of all (livelock-accepting) cycles containing a least - /// one state that is both livelock and accepting states + /// 1- Detection of all cycles containing a least + /// one state that is both livelock and Buchi accepting states /// 2- Detection of all livelock-accepting cycles containing a least /// one state (k,t) such as its "TA component" t is a livelock-accepting /// state that has no successors in the TA automaton. /// - /// The implementation of each pass is a SCC-based algorithm inspired - /// from spot::gtec.hh. + /// The implementation of the algorithm of each pass is a SCC-based algorithm + /// inspired from spot::gtec.hh. + /// @{ /// \brief An implementation of the emptiness-check algorithm for a product /// between a TA and a Kripke structure @@ -153,7 +155,10 @@ namespace spot }; -/// @} + /// @} + + /// \addtogroup ta_emptiness_check_algorithms Emptiness-check algorithms + /// \ingroup ta_emptiness_check } #endif // SPOT_TAALGOS_EMPTINESS_HH diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index faf984456..6e435c81c 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -34,7 +34,7 @@ #include "ltlast/allnodes.hh" #include "misc/hash.hh" #include "misc/bddlt.hh" -#include "ta/tgbtaexplicit.hh" +#include "ta/tgtaexplicit.hh" #include "taalgos/statessetbuilder.hh" #include "tgba/tgbaexplicit.hh" #include "tgba/bddprint.hh" @@ -73,7 +73,8 @@ namespace spot // From the base automaton and the list of sets, build the minimal automaton void - build_result(const ta* a, std::list& sets, tgba_explicit_number* result_tgba, ta_explicit* result) + build_result(const ta* a, std::list& sets, + tgba_explicit_number* result_tgba, ta_explicit* result) { // For each set, create a state in the tgbaulting automaton. @@ -168,314 +169,331 @@ namespace spot else if (is_initial_state) result->add_to_initial_states_set(new_dst); - result->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst); + result->create_transition(ta_src, succit->current_condition(), + succit->current_acceptance_conditions(), ta_dst); } delete succit; } - } - partition_t build_partition(const ta* ta_){ + partition_t + build_partition(const ta* ta_) + { partition_t cur_run; - partition_t next_run; + partition_t next_run; - // The list of equivalent states. - partition_t done; + // The list of equivalent states. + partition_t done; - std::set states_set = get_states_set(ta_); + std::set states_set = get_states_set(ta_); - hash_set* I = new hash_set; + hash_set* I = new hash_set; - // livelock acceptance states - hash_set* G = new hash_set; + // livelock acceptance states + hash_set* G = new hash_set; - // Buchi acceptance states - hash_set* F = new hash_set; + // Buchi acceptance states + hash_set* F = new hash_set; - // Buchi and livelock acceptance states - hash_set* G_F = new hash_set; + // Buchi and livelock acceptance states + hash_set* G_F = new hash_set; - // the other states (non initial and not in G, F and G_F) - hash_set* S = new hash_set; + // the other states (non initial and not in G, F and G_F) + hash_set* S = new hash_set; - std::set::iterator it; + std::set::iterator it; - spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); it++) + { + const state* s = (*it); + + if (s == artificial_initial_state) { - const state* s = (*it); - - if (s == artificial_initial_state) - { - I->insert(s); - } - else if (artificial_initial_state == 0 && ta_->is_initial_state(s)) - { - I->insert(s); - } - else if (ta_->is_livelock_accepting_state(s) - && ta_->is_accepting_state(s)) - { - G_F->insert(s); - } - else if (ta_->is_accepting_state(s)) - { - F->insert(s); - } - - else if (ta_->is_livelock_accepting_state(s)) - { - G->insert(s); - } - else - { - S->insert(s); - } - + I->insert(s); + } + else if (artificial_initial_state == 0 && ta_->is_initial_state(s)) + { + I->insert(s); + } + else if (ta_->is_livelock_accepting_state(s) + && ta_->is_accepting_state(s)) + { + G_F->insert(s); + } + else if (ta_->is_accepting_state(s)) + { + F->insert(s); } - hash_map state_set_map; - - // Size of ta_ - unsigned size = states_set.size() + 6; - // Use bdd variables to number sets. set_num is the first variable - // available. - unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_); - - std::set free_var; - for (unsigned i = set_num; i < set_num + size; ++i) - free_var.insert(i); - std::map used_var; - + else if (ta_->is_livelock_accepting_state(s)) { - - for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i) - { - hash_set* cI = new hash_set; - cI->insert(*i); - done.push_back(cI); - - used_var[set_num] = 1; - free_var.erase(set_num); - state_set_map[*i] = set_num; - set_num++; - - } - - } - delete I; - - if (!G->empty()) - { - unsigned s = G->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(G); - else - done.push_back(G); - for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i) - state_set_map[*i] = num; - + G->insert(s); } else - delete G; - - if (!F->empty()) { - unsigned s = F->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(F); - else - done.push_back(F); - for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i) - state_set_map[*i] = num; + S->insert(s); } - else - delete F; - if (!G_F->empty()) + } + + hash_map state_set_map; + + // Size of ta_ + unsigned size = states_set.size() + 6; + // Use bdd variables to number sets. set_num is the first variable + // available. + unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_); + + std::set free_var; + for (unsigned i = set_num; i < set_num + size; ++i) + free_var.insert(i); + std::map used_var; + + { + + for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i) { - unsigned s = G_F->size(); - unsigned num = set_num; + hash_set* cI = new hash_set; + cI->insert(*i); + done.push_back(cI); + + used_var[set_num] = 1; + free_var.erase(set_num); + state_set_map[*i] = set_num; set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(G_F); - else - done.push_back(G_F); - for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i) - state_set_map[*i] = num; + } - else - delete G_F; - if (!S->empty()) - { - unsigned s = S->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(S); - else - done.push_back(S); - for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i) - state_set_map[*i] = num; - } - else - delete S; + } + delete I; - // A bdd_states_map is a list of formulae (in a BDD form) associated with a - // destination set of states. - typedef std::map bdd_states_map; - - bool did_split = true; + if (!G->empty()) + { + unsigned s = G->size(); unsigned num = set_num; set_num++; - used_var[num] = 1; + used_var[num] = s; free_var.erase(num); - bdd bdd_false_acceptance_condition = bdd_ithvar(num); + if (s > 1) + cur_run.push_back(G); + else + done.push_back(G); + for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i) + state_set_map[*i] = num; - while (did_split) + } + else + delete G; + + if (!F->empty()) + { + unsigned s = F->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(F); + else + done.push_back(F); + for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i) + state_set_map[*i] = num; + } + else + delete F; + + if (!G_F->empty()) + { + unsigned s = G_F->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(G_F); + else + done.push_back(G_F); + for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i) + state_set_map[*i] = num; + } + else + delete G_F; + + if (!S->empty()) + { + unsigned s = S->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(S); + else + done.push_back(S); + for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i) + state_set_map[*i] = num; + } + else + delete S; + + // A bdd_states_map is a list of formulae (in a BDD form) associated with a + // destination set of states. + typedef std::map bdd_states_map; + + bool did_split = true; + unsigned num = set_num; + set_num++; + used_var[num] = 1; + free_var.erase(num); + bdd bdd_false_acceptance_condition = bdd_ithvar(num); + + while (did_split) + { + did_split = false; + while (!cur_run.empty()) { - did_split = false; - while (!cur_run.empty()) + // Get a set to process. + hash_set* cur = cur_run.front(); + cur_run.pop_front(); + + trace + << "processing " << format_hash_set(cur, ta_) << std::endl; + + hash_set::iterator hi; + bdd_states_map bdd_map; + for (hi = cur->begin(); hi != cur->end(); ++hi) { - // Get a set to process. - hash_set* cur = cur_run.front(); - cur_run.pop_front(); - + const state* src = *hi; + bdd f = bddfalse; + ta_succ_iterator* si = ta_->succ_iter(src); trace - << "processing " << format_hash_set(cur, ta_) << std::endl; - - hash_set::iterator hi; - bdd_states_map bdd_map; - for (hi = cur->begin(); hi != cur->end(); ++hi) + << "+src: " << src << std::endl; + for (si->first(); !si->done(); si->next()) { - const state* src = *hi; - bdd f = bddfalse; - ta_succ_iterator* si = ta_->succ_iter(src); - trace << "+src: " << src << std::endl; - for (si->first(); !si->done(); si->next()) - { - const state* dst = si->current_state(); - hash_map::const_iterator i = state_set_map.find(dst); + const state* dst = si->current_state(); + hash_map::const_iterator i = state_set_map.find(dst); - assert(i != state_set_map.end()); - bdd current_acceptance_conditions = - si->current_acceptance_conditions(); - if (current_acceptance_conditions == bddfalse) - current_acceptance_conditions - = bdd_false_acceptance_condition; - f |= (bdd_ithvar(i->second) & si->current_condition() - & current_acceptance_conditions); - trace << "+f: " << bdd_format_accset(ta_->get_dict(),f) << std::endl;; - trace << " -bdd_ithvar(i->second): " << bdd_format_accset(ta_->get_dict(),bdd_ithvar(i->second)) << std::endl;; - trace << " -si->current_condition(): " << bdd_format_accset(ta_->get_dict(),si->current_condition()) << std::endl;; - trace << " -current_acceptance_conditions: " << bdd_format_accset(ta_->get_dict(),current_acceptance_conditions) << std::endl;; - - } - delete si; - - // Have we already seen this formula ? - bdd_states_map::iterator bsi = bdd_map.find(f); - if (bsi == bdd_map.end()) - { - // No, create a new set. - hash_set* new_set = new hash_set; - new_set->insert(src); - bdd_map[f] = new_set; - } - else - { - // Yes, add the current state to the set. - bsi->second->insert(src); - } - } - - bdd_states_map::iterator bsi = bdd_map.begin(); - if (bdd_map.size() == 1) - { - // The set was not split. + assert(i != state_set_map.end()); + bdd current_acceptance_conditions = + si->current_acceptance_conditions(); + if (current_acceptance_conditions == bddfalse) + current_acceptance_conditions + = bdd_false_acceptance_condition; + f |= (bdd_ithvar(i->second) & si->current_condition() + & current_acceptance_conditions); trace - << "set " << format_hash_set(bsi->second, ta_) - << " was not split" << std::endl; - next_run.push_back(bsi->second); + << "+f: " << bdd_format_accset(ta_->get_dict(), f) + << std::endl; + ; + trace + << " -bdd_ithvar(i->second): " << bdd_format_accset( + ta_->get_dict(), bdd_ithvar(i->second)) << std::endl; + ; + trace + << " -si->current_condition(): " + << bdd_format_accset(ta_->get_dict(), + si->current_condition()) << std::endl; + ; + trace + << " -current_acceptance_conditions: " + << bdd_format_accset(ta_->get_dict(), + current_acceptance_conditions) << std::endl; + ; + + } + delete si; + + // Have we already seen this formula ? + bdd_states_map::iterator bsi = bdd_map.find(f); + if (bsi == bdd_map.end()) + { + // No, create a new set. + hash_set* new_set = new hash_set; + new_set->insert(src); + bdd_map[f] = new_set; } else { - did_split = true; - for (; bsi != bdd_map.end(); ++bsi) + // Yes, add the current state to the set. + bsi->second->insert(src); + } + } + + bdd_states_map::iterator bsi = bdd_map.begin(); + if (bdd_map.size() == 1) + { + // The set was not split. + trace + << "set " << format_hash_set(bsi->second, ta_) + << " was not split" << std::endl; + next_run.push_back(bsi->second); + } + else + { + did_split = true; + for (; bsi != bdd_map.end(); ++bsi) + { + hash_set* set = bsi->second; + // Free the number associated to these states. + unsigned num = state_set_map[*set->begin()]; + assert(used_var.find(num) != used_var.end()); + unsigned left = (used_var[num] -= set->size()); + // Make sure LEFT does not become negative (hence bigger + // than SIZE when read as unsigned) + assert(left < size); + if (left == 0) { - hash_set* set = bsi->second; - // Free the number associated to these states. - unsigned num = state_set_map[*set->begin()]; - assert(used_var.find(num) != used_var.end()); - unsigned left = (used_var[num] -= set->size()); - // Make sure LEFT does not become negative (hence bigger - // than SIZE when read as unsigned) - assert(left < size); - if (left == 0) - { - used_var.erase(num); - free_var.insert(num); - } - // Pick a free number - assert(!free_var.empty()); - num = *free_var.begin(); - free_var.erase(free_var.begin()); - used_var[num] = set->size(); - for (hash_set::iterator hit = set->begin(); hit - != set->end(); ++hit) - state_set_map[*hit] = num; - // Trivial sets can't be splitted any further. - if (set->size() == 1) - { - trace - << "set " << format_hash_set(set, ta_) - << " is minimal" << std::endl; - done.push_back(set); - } - else - { - trace - << "set " << format_hash_set(set, ta_) - << " should be processed further" << std::endl; - next_run.push_back(set); - } + used_var.erase(num); + free_var.insert(num); + } + // Pick a free number + assert(!free_var.empty()); + num = *free_var.begin(); + free_var.erase(free_var.begin()); + used_var[num] = set->size(); + for (hash_set::iterator hit = set->begin(); hit + != set->end(); ++hit) + state_set_map[*hit] = num; + // Trivial sets can't be splitted any further. + if (set->size() == 1) + { + trace + << "set " << format_hash_set(set, ta_) + << " is minimal" << std::endl; + done.push_back(set); + } + else + { + trace + << "set " << format_hash_set(set, ta_) + << " should be processed further" << std::endl; + next_run.push_back(set); } } - delete cur; } - if (did_split) - trace - << "splitting did occur during this pass." << std::endl; - //elsetrace << "splitting did not occur during this pass." << std::endl; - std::swap(cur_run, next_run); + delete cur; } + if (did_split) + trace + << "splitting did occur during this pass." << std::endl; + //elsetrace << "splitting did not occur during this pass." << std::endl; + std::swap(cur_run, next_run); + } - done.splice(done.end(), cur_run); + done.splice(done.end(), cur_run); - #ifdef TRACE - trace << "Final partition: "; - for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) - trace << format_hash_set(*i, ta_) << " "; - trace << std::endl; - #endif +#ifdef TRACE + trace << "Final partition: "; + for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) + trace << format_hash_set(*i, ta_) << " "; + trace << std::endl; +#endif - return done; + return done; } ta* @@ -486,11 +504,8 @@ namespace spot ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions()); - partition_t partition = build_partition(ta_); - - // Build the ta automata result. build_result(ta_, partition, tgba, res); @@ -503,32 +518,30 @@ namespace spot return res; } - tgbta* - minimize_tgbta(const tgbta* tgbta_) - { + tgta* + minimize_tgta(const tgta* tgta_) + { - tgba_explicit_number* tgba = new tgba_explicit_number(tgbta_->get_dict()); + tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict()); - tgbta_explicit* res = new tgbta_explicit(tgba, tgbta_->all_acceptance_conditions(),0); + tgta_explicit* res = new tgta_explicit(tgba, + tgta_->all_acceptance_conditions(), 0); - const ta_explicit* tgbta = dynamic_cast (tgbta_); + //TODO copier le tgta_ dans un tgta_explicit au lieu de faire un cast... + const ta_explicit* tgta = dynamic_cast (tgta_); - partition_t partition = build_partition(tgbta); + partition_t partition = build_partition(tgta); + // Build the minimal tgta automaton. + build_result(tgta, partition, tgba, res); + // Free all the allocated memory. + std::list::iterator itdone; + for (itdone = partition.begin(); itdone != partition.end(); ++itdone) + delete *itdone; + //delete ta_; - // Build the tgbault. - build_result(tgbta, partition,tgba, res); - - // Free all the allocated memory. - std::list::iterator itdone; - for (itdone = partition.begin(); itdone != partition.end(); ++itdone) - delete *itdone; - //delete ta_; - - return res; - } - - + return res; + } } diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh index 1fc97fdd1..793db96cd 100644 --- a/src/taalgos/minimize.hh +++ b/src/taalgos/minimize.hh @@ -22,19 +22,58 @@ # define SPOT_TAALGOS_MINIMIZE_HH # include "ta/ta.hh" -# include "ta/tgbta.hh" +# include "ta/tgta.hh" # include "ta/taexplicit.hh" namespace spot { + /// \addtogroup ta_reduction + /// @{ + + /// \brief Construct a simplified TA by merging bisimilar states. + /// + /// A TA automaton can be simplified by merging bisimilar states: + /// Two states are bisimilar if the automaton can accept the + /// same executions starting for either of these states. This can be + /// achieved using any algorithm based on partition refinement + /// + /// For more detail about this type of algorithm, see the following paper: + /// \verbatim + /// @InProceedings{valmari.09.icatpn, + /// author = {Antti Valmari}, + /// title = {Bisimilarity Minimization in in O(m logn) Time}, + /// booktitle = {Proceedings of the 30th International Conference on + /// the Applications and Theory of Petri Nets + /// (ICATPN'09)}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer}, + /// isbn = {978-3-642-02423-8}, + /// pages = {123--142}, + /// volume = 5606, + /// url = {http://dx.doi.org/10.1007/978-3-642-02424-5_9}, + /// year = {2009} + /// } + /// \endverbatim + /// + /// \param ta_ the TA automaton to convert into a simplified TA ta* minimize_ta(const ta* ta_); - tgbta* - minimize_tgbta(const tgbta* tgbta_); + /// \brief Construct a simplified TGTA by merging bisimilar states. + /// + /// A TGTA automaton can be simplified by merging bisimilar states: + /// Two states are bisimilar if the automaton can accept the + /// same executions starting for either of these states. This can be + /// achieved using same algorithm used to simplify a TA taking into account + /// the acceptance conditions of the outgoing transitions. + /// + /// \param tgta_ the TGTA automaton to convert into a simplified TGTA + tgta* + minimize_tgta(const tgta* tgta_); + /// @} } diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc deleted file mode 100644 index 9c1ad64c4..000000000 --- a/src/taalgos/sba2ta.cc +++ /dev/null @@ -1,454 +0,0 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// 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 "ltlast/atomic_prop.hh" -#include "ltlast/constant.hh" -#include "tgba/formula2bdd.hh" -#include "misc/bddop.hh" -#include -#include "ltlvisit/tostring.hh" -#include -#include "tgba/bddprint.hh" -#include "tgbaalgos/gtec/nsheap.hh" -#include -#include "sba2ta.hh" -#include "taalgos/statessetbuilder.hh" - -using namespace std; - -namespace spot -{ - - ta* - sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_, - bool artificial_initial_state_mode, - bool artificial_livelock_accepting_state_mode) - { - - ta_explicit* ta; - std::stack todo; - - // build Initial states set: - state* tgba_init_state = tgba_->get_init_state(); - - if (artificial_initial_state_mode) - { - state_ta_explicit* ta_init_state = new state_ta_explicit( - tgba_init_state->clone(), bddtrue, true); - - ta = new spot::ta_explicit(tgba_, ta_init_state); - } - else - { - ta = new spot::ta_explicit(tgba_); - } - - bdd tgba_condition = tgba_->support_conditions(tgba_init_state); - - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) - { - tgba_condition -= satone_tgba_condition; - state_ta_explicit* init_state = new state_ta_explicit( - tgba_init_state->clone(), satone_tgba_condition, true, - tgba_->state_is_accepting(tgba_init_state)); - state_ta_explicit* s = ta->add_state(init_state); - assert(s == init_state); - ta->add_to_initial_states_set(s); - - todo.push(init_state); - } - tgba_init_state->destroy(); - - while (!todo.empty()) - { - state_ta_explicit* source = todo.top(); - todo.pop(); - - tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( - source->get_tgba_state()); - for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next()) - { - const state* tgba_state = tgba_succ_it->current_state(); - bdd tgba_condition = tgba_succ_it->current_condition(); - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) - { - - tgba_condition -= satone_tgba_condition; - - bdd all_props = bddtrue; - bdd dest_condition; - if (satone_tgba_condition == source->get_tgba_condition()) - while ((dest_condition = bdd_satoneset(all_props, - atomic_propositions_set_, bddtrue)) != bddfalse) - { - all_props -= dest_condition; - state_ta_explicit* new_dest = new state_ta_explicit( - tgba_state->clone(), dest_condition, false, - tgba_->state_is_accepting(tgba_state)); - - state_ta_explicit* dest = ta->add_state(new_dest); - - if (dest != new_dest) - { - // the state dest already exists in the testing automata - new_dest->get_tgba_state()->destroy(); - delete new_dest; - } - else - { - todo.push(dest); - } - - ta->create_transition(source, bdd_setxor( - source->get_tgba_condition(), - dest->get_tgba_condition()), bddfalse, dest); - } - - } - tgba_state->destroy(); - } - delete tgba_succ_it; - - } - - compute_livelock_acceptance_states(ta); - if (artificial_livelock_accepting_state_mode) - { - - state_ta_explicit* artificial_livelock_accepting_state = - new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse, - false, false, true, 0, true); - - add_artificial_livelock_accepting_state(ta, - artificial_livelock_accepting_state); - - } - - return ta; - - } - - void - add_artificial_livelock_accepting_state(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state) - { - - testing_automata->add_state(artificial_livelock_accepting_state); - - ta::states_set_t states_set = testing_automata->get_states_set(); - ta::states_set_t::iterator it; - - std::set* conditions_to_livelock_accepting_states = - new std::set; - - for (it = states_set.begin(); it != states_set.end(); it++) - { - - state_ta_explicit* source = static_cast (*it); - - conditions_to_livelock_accepting_states->clear(); - - state_ta_explicit::transitions* trans = source->get_transitions(); - state_ta_explicit::transitions::iterator it_trans; - - if (trans != 0) - for (it_trans = trans->begin(); it_trans != trans->end();) - { - state_ta_explicit* dest = (*it_trans)->dest; - - if (dest->is_livelock_accepting_state()) - { - conditions_to_livelock_accepting_states->insert( - (*it_trans)->condition); - - } - - //remove hole successors states - state_ta_explicit::transitions* dest_trans = - (dest)->get_transitions(); - bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); - if (dest_trans_empty) - { - source->get_transitions((*it_trans)->condition)->remove( - *it_trans); - delete (*it_trans); - it_trans = trans->erase(it_trans); - } - else - { - it_trans++; - } - } - - if (conditions_to_livelock_accepting_states != 0) - { - std::set::iterator it_conditions; - for (it_conditions - = conditions_to_livelock_accepting_states->begin(); it_conditions - != conditions_to_livelock_accepting_states->end(); it_conditions++) - { - - testing_automata->create_transition(source, (*it_conditions),bddfalse, - artificial_livelock_accepting_state); - - } - } - - } - delete conditions_to_livelock_accepting_states; - - } - - namespace - { - typedef std::pair pair_state_iter; - } - - void - compute_livelock_acceptance_states(ta_explicit* testing_automata) - { - // We use five main data in this algorithm: - // * sscc: a stack of strongly stuttering-connected components (SSCC) - scc_stack_ta sscc; - - // * h: a hash of all visited nodes, with their order, - // (it is called "Hash" in Couvreur's paper) - numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. - - // * num: the number of visited nodes. Used to set the order of each - // visited node, - int num = 0; - - // * todo: the depth-first search stack. This holds pairs of the - // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator - // over the successors of STATE. In our use, ITERATOR should - // always be freed when TODO is popped, but STATE should not because - // it is also used as a key in H. - std::stack todo; - - // * init: the set of the depth-first search initial states - std::stack init_set; - - ta::states_set_t::const_iterator it; - ta::states_set_t init_states = testing_automata->get_initial_states_set(); - for (it = init_states.begin(); it != init_states.end(); it++) - { - state* init_state = (*it); - init_set.push(init_state); - - } - - while (!init_set.empty()) - { - // Setup depth-first search from initial states. - { - state_ta_explicit* init = - down_cast (init_set.top()); - init_set.pop(); - state_ta_explicit* init_clone = init->clone(); - numbered_state_heap::state_index_p h_init = h->find(init_clone); - - if (h_init.first) - continue; - - h->insert(init_clone, ++num); - sscc.push(num); - sscc.top().is_accepting - = testing_automata->is_accepting_state(init); - tgba_succ_iterator* iter = testing_automata->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - - } - - while (!todo.empty()) - { - - state* curr = todo.top().first; - - numbered_state_heap::state_index_p spi = h->find(curr->clone()); - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - { - todo.pop(); - continue; - } - - // We are looking at the next successor in SUCC. - tgba_succ_iterator* succ = todo.top().second; - - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. - - // Backtrack TODO. - todo.pop(); - - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); - - sscc.rem().push_front(curr); - - // When backtracking the root of an SSCC, we must also - // remove that SSCC from the ROOT stacks. We must - // discard from H all reachable states from this SSCC. - assert(!sscc.empty()); - if (sscc.top().index == *spi.second) - { - // removing states - std::list::iterator i; - bool is_livelock_accepting_sscc = (sscc.top().is_accepting - && (sscc.rem().size() > 1)); - for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) - { - numbered_state_heap::state_index_p spi = h->index( - (*i)->clone()); - assert(spi.first->compare(*i) == 0); - assert(*spi.second != -1); - *spi.second = -1; - if (is_livelock_accepting_sscc) - {//if it is an accepting sscc - //add the state to G (=the livelock-accepting states set) - - state_ta_explicit * livelock_accepting_state = - down_cast (*i); - - livelock_accepting_state->set_livelock_accepting_state( - true); - } - - } - - sscc.pop(); - - } - - // automata reduction - testing_automata->delete_stuttering_and_hole_successors(curr); - - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } - - // Fetch the values destination state we are interested in... - state* dest = succ->current_state(); - - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. - - - // Are we going to a new state through a stuttering transition? - bool is_stuttering_transition = - testing_automata->get_state_condition(curr) - == testing_automata->get_state_condition(dest); - state* dest_clone = dest->clone(); - spi = h->find(dest_clone); - - // Is this a new state? - if (!spi.first) - { - if (!is_stuttering_transition) - { - init_set.push(dest); - dest_clone->destroy(); - continue; - } - - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest_clone, ++num); - sscc.push(num); - sscc.top().is_accepting = testing_automata->is_accepting_state( - dest); - - tgba_succ_iterator* iter = testing_automata->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - continue; - } - - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; - - if (!curr->compare(dest)) - { - state_ta_explicit * self_loop_state = - down_cast (curr); - assert(self_loop_state); - - if (testing_automata->is_accepting_state(self_loop_state)) - self_loop_state->set_livelock_accepting_state(true); - - } - - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SSCC. Any such - // non-dead SSCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SSCC too. We are going to merge all states between - // this S1 and S2 into this SSCC. - // - // This merge is easy to do because the order of the SSCC in - // ROOT is ascending: we just have to merge all SSCCs from the - // top of ROOT that have an index greater to the one of - // the SSCC of S2 (called the "threshold"). - int threshold = *spi.second; - std::list rem; - bool acc = false; - - while (threshold < sscc.top().index) - { - assert(!sscc.empty()); - - acc |= sscc.top().is_accepting; - - rem.splice(rem.end(), sscc.rem()); - sscc.pop(); - - } - // Note that we do not always have - // threshold == sscc.top().index - // after this loop, the SSCC whose index is threshold might have - // been merged with a lower SSCC. - - // Accumulate all acceptance conditions into the merged SSCC. - sscc.top().is_accepting |= acc; - - sscc.rem().splice(sscc.rem().end(), rem); - - } - - } - delete h; - - } -} diff --git a/src/taalgos/sba2ta.hh b/src/taalgos/sba2ta.hh deleted file mode 100644 index 56617d3c2..000000000 --- a/src/taalgos/sba2ta.hh +++ /dev/null @@ -1,49 +0,0 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement -// 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_TGBAALGOS_SBA2TA_HH -# define SPOT_TGBAALGOS_SBA2TA_HH - -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" -#include "ltlast/formula.hh" -#include -#include "misc/bddlt.hh" -#include "ta/taexplicit.hh" - -namespace spot -{ - ta* - sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set, bool artificial_initial_state_mode = true, - bool artificial_livelock_accepting_state_mode = false); - - void - compute_livelock_acceptance_states(ta_explicit* testing_automata); - - void - add_artificial_livelock_accepting_state(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state); - -} - -#endif // SPOT_TGBAALGOS_SBA2TA_HH diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 30782d923..dc76d1359 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -39,16 +39,412 @@ #include #include "tgba2ta.hh" #include "taalgos/statessetbuilder.hh" -#include "ta/tgbtaexplicit.hh" +#include "ta/tgtaexplicit.hh" using namespace std; namespace spot { + namespace + { + typedef std::pair pair_state_iter; + } + + void + transform_to_single_pass_automaton(ta_explicit* testing_automata, + state_ta_explicit* artificial_livelock_accepting_state = 0) + { + + if (artificial_livelock_accepting_state != 0) + { + state_ta_explicit* artificial_livelock_accepting_state_added = + testing_automata->add_state(artificial_livelock_accepting_state); + + // unique artificial_livelock_accepting_state + assert(artificial_livelock_accepting_state_added + == artificial_livelock_accepting_state); + artificial_livelock_accepting_state->set_livelock_accepting_state(true); + artificial_livelock_accepting_state->free_transitions(); + } + + + + ta::states_set_t states_set = testing_automata->get_states_set(); + ta::states_set_t::iterator it; + + state_ta_explicit::transitions* transitions_to_livelock_states = + new state_ta_explicit::transitions; + + for (it = states_set.begin(); it != states_set.end(); it++) + { + + state_ta_explicit* source = static_cast (*it); + + transitions_to_livelock_states->clear(); + + state_ta_explicit::transitions* trans = source->get_transitions(); + state_ta_explicit::transitions::iterator it_trans; + + if (trans != 0) + for (it_trans = trans->begin(); it_trans != trans->end();) + { + state_ta_explicit* dest = (*it_trans)->dest; + + state_ta_explicit::transitions* dest_trans = + (dest)->get_transitions(); + bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + + + + //select transitions where a destination is a livelock state + // which isn't a Buchi accepting state and has successors + if (dest->is_livelock_accepting_state() + && (!dest->is_accepting_state()) && (!dest_trans_empty)) + { + transitions_to_livelock_states->push_front(*it_trans); + + } + + //optimization to have, after + // minimization, an unique livelock state which has no successors + if (dest->is_livelock_accepting_state() && (dest_trans_empty)) + { + dest->set_accepting_state(false); + + } + + it_trans++; + + } + + if (transitions_to_livelock_states != 0) + { + state_ta_explicit::transitions::iterator it_trans; + + for (it_trans = transitions_to_livelock_states->begin(); it_trans + != transitions_to_livelock_states->end(); it_trans++) + { + if (artificial_livelock_accepting_state != 0) + { + testing_automata->create_transition(source, + (*it_trans)->condition, + (*it_trans)->acceptance_conditions, + artificial_livelock_accepting_state, true); + } + else + { + testing_automata->create_transition(source, + (*it_trans)->condition, + (*it_trans)->acceptance_conditions, + ((*it_trans)->dest)->stuttering_reachable_livelock, + true); + } + + } + } + + } + delete transitions_to_livelock_states; + + for (it = states_set.begin(); it != states_set.end(); it++) + { + + state_ta_explicit* state = static_cast (*it); + state_ta_explicit::transitions* state_trans = + (state)->get_transitions(); + bool state_trans_empty = state_trans == 0 || state_trans->empty(); + + if (state->is_livelock_accepting_state() + && (!state->is_accepting_state()) && (!state_trans_empty)) + state->set_livelock_accepting_state(false); + } + + } + +void +compute_livelock_acceptance_states(ta_explicit* testing_automata, + bool single_pass_emptiness_check, + state_ta_explicit* artificial_livelock_accepting_state) +{ + // We use five main data in this algorithm: + // * sscc: a stack of strongly stuttering-connected components (SSCC) + scc_stack_ta sscc; + + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + + // * h: a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + numbered_state_heap* h = + numbered_state_heap_hash_map_factory::instance()->build(); + ///< Heap of visited states. + + // * num: the number of visited nodes. Used to set the order of each + // visited node, + int num = 0; + + // * todo: the depth-first search stack. This holds pairs of the + // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator + // over the successors of STATE. In our use, ITERATOR should + // always be freed when TODO is popped, but STATE should not because + // it is also used as a key in H. + std::stack todo; + + // * init: the set of the depth-first search initial states + std::stack init_set; + + ta::states_set_t::const_iterator it; + ta::states_set_t init_states = testing_automata->get_initial_states_set(); + for (it = init_states.begin(); it != init_states.end(); it++) + { + state* init_state = (*it); + init_set.push(init_state); + + } + + while (!init_set.empty()) + { + // Setup depth-first search from initial states. + + { + state_ta_explicit* init = + down_cast (init_set.top()); + init_set.pop(); + state_ta_explicit* init_clone = init; + numbered_state_heap::state_index_p h_init = h->find(init_clone); + + if (h_init.first) + continue; + + h->insert(init_clone, ++num); + sscc.push(num); + arc.push(bddfalse); + sscc.top().is_accepting + = testing_automata->is_accepting_state(init); + tgba_succ_iterator* iter = testing_automata->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + + } + + while (!todo.empty()) + { + + state* curr = todo.top().first; + + numbered_state_heap::state_index_p spi = h->find(curr); + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + { + todo.pop(); + continue; + } + + // We are looking at the next successor in SUCC. + tgba_succ_iterator* succ = todo.top().second; + + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. + + // Backtrack TODO. + todo.pop(); + + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = h->index(curr); + assert(spi.first); + + sscc.rem().push_front(curr); + + // When backtracking the root of an SSCC, we must also + // remove that SSCC from the ROOT stacks. We must + // discard from H all reachable states from this SSCC. + assert(!sscc.empty()); + if (sscc.top().index == *spi.second) + { + // removing states + std::list::iterator i; + bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) + && ((sscc.top().is_accepting) || (sscc.top().condition + == testing_automata->all_acceptance_conditions())); + + trace + << "*** sscc.size() = ***" + << sscc.size() << std::endl; + for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) + { + numbered_state_heap::state_index_p spi = h->index((*i)); + assert(spi.first->compare(*i) == 0); + assert(*spi.second != -1); + *spi.second = -1; + + if (is_livelock_accepting_sscc) + {//if it is an accepting sscc add the state to + //G (=the livelock-accepting states set) + trace << "*** sscc.size() > 1: states: ***" + << testing_automata->format_state(*i) + << std::endl; + state_ta_explicit * livelock_accepting_state = + down_cast (*i); + + livelock_accepting_state->set_livelock_accepting_state( + true); + + if (single_pass_emptiness_check) + { + livelock_accepting_state->set_accepting_state( + true); + livelock_accepting_state->stuttering_reachable_livelock + = livelock_accepting_state; + } + + } + + } + + assert(!arc.empty()); + sscc.pop(); + arc.pop(); + + } + + // automata reduction + testing_automata->delete_stuttering_and_hole_successors(curr); + + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } + + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); + + bdd acc_cond = succ->current_acceptance_conditions(); + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. + + + // Are we going to a new state through a stuttering transition? + bool is_stuttering_transition = + testing_automata->get_state_condition(curr) + == testing_automata->get_state_condition(dest); + state* dest_clone = dest; + spi = h->find(dest_clone); + + // Is this a new state? + if (!spi.first) + { + if (!is_stuttering_transition) + { + init_set.push(dest); + dest_clone->destroy(); + continue; + } + + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest_clone, ++num); + sscc.push(num); + arc.push(acc_cond); + sscc.top().is_accepting = testing_automata->is_accepting_state( + dest); + + tgba_succ_iterator* iter = testing_automata->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + continue; + } + + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; + + trace + << "***compute_livelock_acceptance_states: CYCLE***" << std::endl; + + if (!curr->compare(dest)) + { + state_ta_explicit * self_loop_state = + down_cast (curr); + assert(self_loop_state); + + if (testing_automata->is_accepting_state(self_loop_state) + || (acc_cond + == testing_automata->all_acceptance_conditions())) + { + self_loop_state->set_livelock_accepting_state(true); + if (single_pass_emptiness_check) + { + self_loop_state->set_accepting_state(true); + self_loop_state->stuttering_reachable_livelock + = self_loop_state; + } + + } + + trace + << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" + << std::endl; + + } + + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // ROOT is ascending: we just have to merge all SSCCs from the + // top of ROOT that have an index greater to the one of + // the SSCC of S2 (called the "threshold"). + int threshold = *spi.second; + std::list rem; + bool acc = false; + + while (threshold < sscc.top().index) + { + assert(!sscc.empty()); + assert(!arc.empty()); + acc |= sscc.top().is_accepting; + acc_cond |= sscc.top().condition; + acc_cond |= arc.top(); + rem.splice(rem.end(), sscc.rem()); + sscc.pop(); + arc.pop(); + } + + // Note that we do not always have + // threshold == sscc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. + + // Accumulate all acceptance conditions into the merged SSCC. + sscc.top().is_accepting |= acc; + sscc.top().condition |= acc_cond; + + sscc.rem().splice(sscc.rem().end(), rem); + + } + + } + delete h; + + if ((artificial_livelock_accepting_state != 0) + || single_pass_emptiness_check) + transform_to_single_pass_automaton(testing_automata, + artificial_livelock_accepting_state); + +} + ta_explicit* - build_ta(ta_explicit* ta, bdd atomic_propositions_set_, - bool artificial_livelock_accepting_state_mode, bool degeneralized) + build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool degeneralized, + bool single_pass_emptiness_check, bool artificial_livelock_state_mode) { std::stack todo; @@ -115,17 +511,17 @@ namespace spot all_props -= dest_condition; state_ta_explicit* new_dest; if (degeneralized) - { + { - new_dest - = new state_ta_explicit( - tgba_state->clone(), - dest_condition, - false, + new_dest + = new state_ta_explicit( + tgba_state->clone(), + dest_condition, + false, ((const tgba_sba_proxy*) tgba_)->state_is_accepting( - tgba_state)); + tgba_state)); - } + } else { new_dest = new state_ta_explicit(tgba_state->clone(), @@ -136,7 +532,7 @@ namespace spot if (dest != new_dest) { - // the state dest already exists in the testing automata + // the state dest already exists in the automaton new_dest->get_tgba_state()->destroy(); delete new_dest; } @@ -163,11 +559,11 @@ namespace spot trace << "*** build_ta: artificial_livelock_accepting_state_mode = ***" - << artificial_livelock_accepting_state_mode << std::endl; + << artificial_livelock_state_mode << std::endl; - if (artificial_livelock_accepting_state_mode) + if (artificial_livelock_state_mode) { - + single_pass_emptiness_check = true; artificial_livelock_accepting_state = new state_ta_explicit( ta->get_tgba()->get_init_state(), bddtrue, false, false, true, 0); trace @@ -176,7 +572,8 @@ namespace spot } - compute_livelock_acceptance_states(ta, artificial_livelock_accepting_state); + compute_livelock_acceptance_states(ta, single_pass_emptiness_check, + artificial_livelock_accepting_state); return ta; @@ -184,19 +581,19 @@ namespace spot ta_explicit* tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_, - bool artificial_initial_state_mode, - bool artificial_livelock_accepting_state_mode, bool degeneralized) + bool degeneralized, bool artificial_initial_state_mode, + bool single_pass_emptiness_check, bool artificial_livelock_state_mode) { ta_explicit* ta; state* tgba_init_state = tgba_->get_init_state(); if (artificial_initial_state_mode) { - state_ta_explicit* ta_init_state = new state_ta_explicit( + state_ta_explicit* artificial_init_state = new state_ta_explicit( tgba_init_state->clone(), bddfalse, true); ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(), - ta_init_state); + artificial_init_state); } else { @@ -205,413 +602,38 @@ namespace spot tgba_init_state->destroy(); // build ta automata: - build_ta(ta, atomic_propositions_set_, - artificial_livelock_accepting_state_mode, degeneralized); + build_ta(ta, atomic_propositions_set_, degeneralized, + single_pass_emptiness_check, artificial_livelock_state_mode); return ta; } - void - add_artificial_livelock_accepting_state(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state) - { - - state_ta_explicit* artificial_livelock_accepting_state_added = - testing_automata->add_state(artificial_livelock_accepting_state); - - // unique artificial_livelock_accepting_state - assert(artificial_livelock_accepting_state_added - == artificial_livelock_accepting_state); - - trace - << "*** add_artificial_livelock_accepting_state: " - << "assert(artificial_livelock_accepting_state_added == " - << "artificial_livelock_accepting_state) = ***" - << (artificial_livelock_accepting_state_added - == artificial_livelock_accepting_state) << std::endl; - - ta::states_set_t states_set = testing_automata->get_states_set(); - ta::states_set_t::iterator it; - - std::set* conditions_to_livelock_accepting_states = - new std::set; - - for (it = states_set.begin(); it != states_set.end(); it++) - { - - state_ta_explicit* source = static_cast (*it); - - conditions_to_livelock_accepting_states->clear(); - - state_ta_explicit::transitions* trans = source->get_transitions(); - state_ta_explicit::transitions::iterator it_trans; - - if (trans != 0) - for (it_trans = trans->begin(); it_trans != trans->end();) - { - state_ta_explicit* dest = (*it_trans)->dest; - - state_ta_explicit::transitions* dest_trans = - (dest)->get_transitions(); - bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); - - //TA++ - if (dest->is_livelock_accepting_state() - && (!dest->is_accepting_state() || dest_trans_empty)) - { - conditions_to_livelock_accepting_states->insert( - (*it_trans)->condition); - - } - - //remove hole successors states - if (dest_trans_empty) - { - source->get_transitions((*it_trans)->condition)->remove( - *it_trans); - delete (*it_trans); - it_trans = trans->erase(it_trans); - } - else - { - it_trans++; - } - } - - if (conditions_to_livelock_accepting_states != 0) - { - std::set::iterator it_conditions; - for (it_conditions - = conditions_to_livelock_accepting_states->begin(); it_conditions - != conditions_to_livelock_accepting_states->end(); it_conditions++) - { - - testing_automata->create_transition(source, (*it_conditions), - bddfalse, artificial_livelock_accepting_state, true); - - } - } - - } - delete conditions_to_livelock_accepting_states; - - for (it = states_set.begin(); it != states_set.end(); it++) - { - - state_ta_explicit* state = static_cast (*it); - state_ta_explicit::transitions* state_trans = - (state)->get_transitions(); - bool state_trans_empty = state_trans == 0 || state_trans->empty(); - - if (state->is_livelock_accepting_state() - && (!state->is_accepting_state()) && (!state_trans_empty)) - state->set_livelock_accepting_state(false); - } - - } - - namespace - { - typedef std::pair pair_state_iter; - } - - void - compute_livelock_acceptance_states(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state) - { - // We use five main data in this algorithm: - // * sscc: a stack of strongly stuttering-connected components (SSCC) - scc_stack_ta sscc; - - // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; - - // * h: a hash of all visited nodes, with their order, - // (it is called "Hash" in Couvreur's paper) - numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); - ///< Heap of visited states. - - // * num: the number of visited nodes. Used to set the order of each - // visited node, - int num = 0; - - // * todo: the depth-first search stack. This holds pairs of the - // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator - // over the successors of STATE. In our use, ITERATOR should - // always be freed when TODO is popped, but STATE should not because - // it is also used as a key in H. - std::stack todo; - - // * init: the set of the depth-first search initial states - std::stack init_set; - - ta::states_set_t::const_iterator it; - ta::states_set_t init_states = testing_automata->get_initial_states_set(); - for (it = init_states.begin(); it != init_states.end(); it++) - { - state* init_state = (*it); - init_set.push(init_state); - - } - - while (!init_set.empty()) - { - // Setup depth-first search from initial states. - - { - state_ta_explicit* init = - down_cast (init_set.top()); - init_set.pop(); - state_ta_explicit* init_clone = init; - numbered_state_heap::state_index_p h_init = h->find(init_clone); - - if (h_init.first) - continue; - - h->insert(init_clone, ++num); - sscc.push(num); - arc.push(bddfalse); - sscc.top().is_accepting - = testing_automata->is_accepting_state(init); - tgba_succ_iterator* iter = testing_automata->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - - } - - while (!todo.empty()) - { - - state* curr = todo.top().first; - - numbered_state_heap::state_index_p spi = h->find(curr); - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - { - todo.pop(); - continue; - } - - // We are looking at the next successor in SUCC. - tgba_succ_iterator* succ = todo.top().second; - - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. - - // Backtrack TODO. - todo.pop(); - - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = h->index(curr); - assert(spi.first); - - sscc.rem().push_front(curr); - - // When backtracking the root of an SSCC, we must also - // remove that SSCC from the ROOT stacks. We must - // discard from H all reachable states from this SSCC. - assert(!sscc.empty()); - if (sscc.top().index == *spi.second) - { - // removing states - std::list::iterator i; - bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) - && ((sscc.top().is_accepting) || (sscc.top().condition - == testing_automata->all_acceptance_conditions())); - - for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) - { - numbered_state_heap::state_index_p spi = h->index((*i)); - assert(spi.first->compare(*i) == 0); - assert(*spi.second != -1); - *spi.second = -1; - if (is_livelock_accepting_sscc) - {//if it is an accepting sscc add the state to - //G (=the livelock-accepting states set) - - state_ta_explicit * livelock_accepting_state = - down_cast (*i); - - livelock_accepting_state->set_livelock_accepting_state( - true); - - //case STA (Single-pass Testing Automata) or case - //STGTA (Single-pass Transition-based Generalised Testing Automata) - if (artificial_livelock_accepting_state != 0) - livelock_accepting_state->set_accepting_state( - true); - } - - } - - assert(!arc.empty()); - sscc.pop(); - arc.pop(); - - } - - // automata reduction - testing_automata->delete_stuttering_and_hole_successors(curr); - - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } - - // Fetch the values destination state we are interested in... - state* dest = succ->current_state(); - - bdd acc_cond = succ->current_acceptance_conditions(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. - - - // Are we going to a new state through a stuttering transition? - bool is_stuttering_transition = - testing_automata->get_state_condition(curr) - == testing_automata->get_state_condition(dest); - state* dest_clone = dest; - spi = h->find(dest_clone); - - // Is this a new state? - if (!spi.first) - { - if (!is_stuttering_transition) - { - init_set.push(dest); - dest_clone->destroy(); - continue; - } - - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest_clone, ++num); - sscc.push(num); - arc.push(acc_cond); - sscc.top().is_accepting = testing_automata->is_accepting_state( - dest); - - tgba_succ_iterator* iter = testing_automata->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - continue; - } - - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; - - trace - << "***compute_livelock_acceptance_states: CYCLE***" << std::endl; - - if (!curr->compare(dest)) - { - state_ta_explicit * self_loop_state = - down_cast (curr); - assert(self_loop_state); - - if (testing_automata->is_accepting_state(self_loop_state) - || (acc_cond - == testing_automata->all_acceptance_conditions())) - { - self_loop_state->set_livelock_accepting_state(true); - if (artificial_livelock_accepting_state != 0) - self_loop_state->set_accepting_state(true); - - } - - trace - << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" - << std::endl; - - } - - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SSCC. Any such - // non-dead SSCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SSCC too. We are going to merge all states between - // this S1 and S2 into this SSCC. - // - // This merge is easy to do because the order of the SSCC in - // ROOT is ascending: we just have to merge all SSCCs from the - // top of ROOT that have an index greater to the one of - // the SSCC of S2 (called the "threshold"). - int threshold = *spi.second; - std::list rem; - bool acc = false; - - while (threshold < sscc.top().index) - { - assert(!sscc.empty()); - assert(!arc.empty()); - acc |= sscc.top().is_accepting; - acc_cond |= sscc.top().condition; - acc_cond |= arc.top(); - rem.splice(rem.end(), sscc.rem()); - sscc.pop(); - arc.pop(); - } - - // Note that we do not always have - // threshold == sscc.top().index - // after this loop, the SSCC whose index is threshold might have - // been merged with a lower SSCC. - - // Accumulate all acceptance conditions into the merged SSCC. - sscc.top().is_accepting |= acc; - sscc.top().condition |= acc_cond; - - sscc.rem().splice(sscc.rem().end(), rem); - - } - - } - delete h; - - trace - << "*** compute_livelock_acceptance_states: PRE call add_artificial_livelock_accepting_state() method ... (artificial_livelock_accepting_state != 0) :***" - << (artificial_livelock_accepting_state != 0) << std::endl; - - if (artificial_livelock_accepting_state != 0) - add_artificial_livelock_accepting_state(testing_automata, - artificial_livelock_accepting_state); - - trace - << "*** compute_livelock_acceptance_states: POST call add_artificial_livelock_accepting_state() method ***" - << std::endl; - } - - tgbta_explicit* - tgba_to_tgbta(const tgba* tgba_, bdd atomic_propositions_set_) + tgta_explicit* + tgba_to_tgta(const tgba* tgba_, bdd atomic_propositions_set_) { state* tgba_init_state = tgba_->get_init_state(); - state_ta_explicit* ta_init_state = new state_ta_explicit( + state_ta_explicit* artificial_init_state = new state_ta_explicit( tgba_init_state->clone(), bddfalse, true); tgba_init_state->destroy(); - tgbta_explicit* tgbta = new spot::tgbta_explicit(tgba_, - tgba_->all_acceptance_conditions(), ta_init_state); + tgta_explicit* tgta = new spot::tgta_explicit(tgba_, + tgba_->all_acceptance_conditions(), artificial_init_state); - // build ta automata: - build_ta(tgbta, atomic_propositions_set_, true, false); + // build a Generalized TA automaton involving a single_pass_emptiness_check + // (without an artificial livelock state): + build_ta(tgta, atomic_propositions_set_, false, true, false); trace << "***tgba_to_tgbta: POST build_ta***" << std::endl; - // adapt a ta automata to build tgbta automata : - ta::states_set_t states_set = tgbta->get_states_set(); + // adapt a ta automata to build tgta automata : + ta::states_set_t states_set = tgta->get_states_set(); ta::states_set_t::iterator it; - tgba_succ_iterator* initial_states_iter = tgbta->succ_iter( - tgbta->get_artificial_initial_state()); + tgba_succ_iterator* initial_states_iter = tgta->succ_iter( + tgta->get_artificial_initial_state()); initial_states_iter->first(); if (initial_states_iter->done()) - return tgbta; + return tgta; bdd first_state_condition = (initial_states_iter)->current_condition(); delete initial_states_iter; @@ -630,21 +652,14 @@ namespace spot bool trans_empty = (trans == 0 || trans->empty()); if (trans_empty || state->is_accepting_state()) { - trace - << "***tgba_to_tgbta: PRE if (state->is_livelock_accepting_state()) ... create_transition ***" - << std::endl; - tgbta->create_transition(state, bdd_stutering_transition, - tgbta->all_acceptance_conditions(), state); - trace - << "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***" - << std::endl; - + tgta->create_transition(state, bdd_stutering_transition, + tgta->all_acceptance_conditions(), state); } } - if (state->compare(tgbta->get_artificial_initial_state())) - tgbta->create_transition(state, bdd_stutering_transition, bddfalse, + if (state->compare(tgta->get_artificial_initial_state())) + tgta->create_transition(state, bdd_stutering_transition, bddfalse, state); state->set_livelock_accepting_state(false); @@ -654,7 +669,7 @@ namespace spot } - return tgbta; + return tgta; } diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index c0cf96ebf..bad425c15 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -30,11 +30,11 @@ #include #include "misc/bddlt.hh" #include "ta/taexplicit.hh" -#include "ta/tgbtaexplicit.hh" +#include "ta/tgtaexplicit.hh" namespace spot { - /// \brief Build a spot::tgba_explicit* from an LTL formula. + /// \brief Build a spot::ta_explicit* (TA) from an LTL formula. /// \ingroup tgba_ta /// /// This is based on the following paper. @@ -57,50 +57,53 @@ namespace spot /// \param atomic_propositions_set The set of atomic propositions used in the /// input TGBA \a tgba_to_convert /// + /// \param degeneralized When false, the returned automaton is a generalized + /// form of TA, called GTA (Generalized Testing Automaton). + /// Like TGBA, GTA use Generalized Büchi acceptance + /// conditions intead of Buchi-accepting states: there are several acceptance + /// sets (of transitions), and a path is accepted if it traverses + /// at least one transition of each set infinitely often or if it contains a + /// livelock-accepting cycle (like a TA). The spot emptiness check algorithm + /// for TA (spot::ta_check::check) can also be used to check GTA. + /// /// \param artificial_initial_state_mode When set, the algorithm will build /// a TA automaton with an unique initial state. This /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (see spot::ta::get_artificial_initial_state()) /// - /// \param STA_mode When set, the returned TA - /// automaton is a STA (Single-pass Testing Automata): a STA automaton is a TA + /// \param single_pass_emptiness_check When set, the product between the + /// returned automaton and a kripke structure requires only the fist pass of + /// the emptiness check algorithm (see the parameter \c disable_second_pass + /// of the method spot::ta_check::check) + /// + /// + /// \param artificial_livelock_state_mode When set, the returned TA automaton + /// is a STA (Single-pass Testing Automata): a STA automaton is a TA /// where: for every livelock-accepting state s, if s is not also a /// Buchi-accepting state, then s has no successors. A STA product requires /// only one-pass emptiness check algorithm (see spot::ta_check::check) /// - /// \param degeneralized When false, the returned automaton is a generalized - /// form of TA, called TGTA (Transition-based Generalized Testing Automaton). - /// Like TGBA, TGTA use Generalized Büchi acceptance - /// conditions intead of Büchi-accepting states: there are several acceptance - /// sets (of transitions), and a path is accepted if it traverses - /// at least one transition of each set infinitely often or if it contains a - /// livelock-accepting cycle. /// /// \return A spot::ta_explicit that recognizes the same language as the /// TGBA \a tgba_to_convert. ta_explicit* tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set, - bool artificial_initial_state_mode = true, bool STA_mode = false, - bool degeneralized = true); + bool degeneralized = true, bool artificial_initial_state_mode = true, + bool single_pass_emptiness_check = false, + bool artificial_livelock_state_mode = false); - stgta_explicit* - tgba_to_stgta(const tgba* tgba_to_convert, bdd atomic_propositions_set); - - - //artificial_livelock_accepting_state is used in the case of - //STA (Single-pass Testing Automata) or in the case - //STGTA (Single-pass Transition-based Generalised Testing Automata) - void - compute_livelock_acceptance_states(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state = 0); - - //artificial_livelock_accepting_state is added to transform TA into - //STA (Single-pass Testing Automata) or to transform TGTA into - //STGTA (Single-pass Transition-based Generalised Testing Automata) - void - add_artificial_livelock_accepting_state(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state); + /// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula. + /// \ingroup tgba_ta + /// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton + /// + /// \param atomic_propositions_set The set of atomic propositions used in the + /// input TGBA \a tgba_to_convert + /// + /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same + /// language as the TGBA \a tgba_to_convert. + tgta_explicit* + tgba_to_tgta(const tgba* tgba_to_convert, bdd atomic_propositions_set); } diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 26a604ecc..f84b7d938 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -1,9 +1,6 @@ #!/bin/sh -# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement +# 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 -# et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -29,8 +26,22 @@ set -e check () { - run 0 ../ltl2tgba -TA "$1" - run 0 ../ltl2tgba -TM "$1" + run 0 ../ltl2tgba -TA -ks "$1" + run 0 ../ltl2tgba -TA -Rm -ks "$1" + run 0 ../ltl2tgba -TA -lv -ks "$1" + run 0 ../ltl2tgba -TA -sp -ks "$1" + run 0 ../ltl2tgba -TA -Rm -lv "$1" + run 0 ../ltl2tgba -TA -Rm -sp -ks "$1" + run 0 ../ltl2tgba -TA -lv -sp -ks "$1" + run 0 ../ltl2tgba -TA -DS -ks "$1" + run 0 ../ltl2tgba -TA -Rm -DS -ks "$1" + run 0 ../ltl2tgba -TA -lv -DS -ks "$1" + run 0 ../ltl2tgba -TA -sp -DS -ks "$1" + run 0 ../ltl2tgba -TA -Rm -sp -DS -ks "$1" + run 0 ../ltl2tgba -TA -Rm -lv -DS -ks "$1" + run 0 ../ltl2tgba -TA -Rm -sp -lv -DS -ks "$1" + run 0 ../ltl2tgba -TGTA -ks "$1" + run 0 ../ltl2tgba -TGTA -Rm -ks "$1" } # We don't check the output, but just running these might be enough to @@ -52,8 +63,6 @@ check '((Gp2)U(F(1)))&(p1 R(p2 R p0))' -# Make sure 'a U (b U c)' has 21 states and 144 transitions, -# before and after degeneralization. for opt in -TA; do ../ltl2tgba -ks $opt -in 'a U (b U c)' > stdout grep 'transitions: 144$' stdout @@ -61,24 +70,23 @@ for opt in -TA; do done -for opt in -TM; do - ../ltl2tgba -ks $opt -in -DS 'a U (b U c)' > stdout +for opt in -TA; do + ../ltl2tgba -ks $opt -Rm -in -DS 'a U (b U c)' > stdout grep 'transitions: 69$' stdout grep 'states: 10$' stdout done -for opt in -TM; do - ../ltl2tgba -ks $opt -DS '!(Ga U b)' > stdout +for opt in -TA; do + ../ltl2tgba -ks $opt -Rm -DS '!(Ga U b)' > stdout grep 'transitions: 15$' stdout grep 'states: 5$' stdout done -# Make sure 'Ga U b' has 6 states and 12 transitions, -# before and after degeneralization. -for opt in -TM; do - ../ltl2tgba -ks $opt -DS 'Ga U b' > stdout + +for opt in -TA; do + ../ltl2tgba -ks $opt -Rm -DS 'Ga U b' > stdout grep 'transitions: 13$' stdout grep 'states: 6$' stdout done @@ -92,26 +100,21 @@ f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' grep 'transitions: 96$' stdout grep 'states: 21$' stdout -# Note: after minimization with -TM. +# Note: after minimization with -TA -Rm. # has 20 states and 89 transitions, after minimization. -../ltl2tgba -ks -TM -DS "$f" > stdout +../ltl2tgba -ks -TA -Rm -DS "$f" > stdout grep 'transitions: 89$' stdout grep 'states: 20$' stdout -# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' -# has 448 states and 28224 transitions. f='GFa & GFb & GFc & GFd & GFe & GFg' ../ltl2tgba -ks -TA -DS -x "$f" > stdout grep 'transitions: 28351$' stdout grep 'states: 449$' stdout -# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' -# has 290 states and 18527 transitions with artificial livelock state. - f='GFa & GFb & GFc & GFd & GFe & GFg' -../ltl2tgba -ks -TM -x -lv -DS "$f" > stdout +../ltl2tgba -ks -TA -Rm -x -lv -DS "$f" > stdout grep 'transitions: 18496$' stdout grep 'states: 290$' stdout @@ -121,61 +124,71 @@ run 0 ../ltl2tgba -ks -TA -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout grep 'transitions: 882$' stdout grep 'states: 78$' stdout -run 0 ../ltl2tgba -TM -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout grep 'transitions: 440$' stdout grep 'states: 28$' stdout +run 0 ../ltl2tgba -TGTA -Rm -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout +grep 'transitions: 294$' stdout +grep 'states: 21$' stdout -run 0 ../ltl2tgba -TM -ks -in -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -in -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 521$' stdout grep 'states: 43$' stdout -run 0 ../ltl2tgba -TM -ks -lv -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -lv -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 636$' stdout grep 'states: 45$' stdout -run 0 ../ltl2tgba -TM -ks -DS "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout -grep 'transitions: 2779$' stdout -grep 'states: 127$' stdout - - -run 0 ../ltl2tgba -TM -ks -lv -DS "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout -grep 'transitions: 2831$' stdout -grep 'states: 128$' stdout - - - -run 0 ../ltl2tgba -TM -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 498$' stdout grep 'states: 34$' stdout -run 0 ../ltl2tgba -TM -ks -lv -in "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -in "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 566$' stdout grep 'states: 35$' stdout -run 0 ../ltl2tgba -TM -ks -in -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -in -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 464$' stdout grep 'states: 36$' stdout -run 0 ../ltl2tgba -TM -ks -lv -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 565$' stdout grep 'states: 38$' stdout -run 0 ../ltl2tgba -TA -ks -lv -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -ks -sp -lv -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 831$' stdout grep 'states: 56$' stdout -run 0 ../ltl2tgba -TM -ks -lv "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout grep 'transitions: 585$' stdout grep 'states: 36$' stdout +run 0 ../ltl2tgba -TGTA -Rm -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 598$' stdout +grep 'states: 35$' stdout + + +run 0 ../ltl2tgba -TA -Rm -ks -DS "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +grep 'transitions: 2779$' stdout +grep 'states: 127$' stdout + + +run 0 ../ltl2tgba -TA -Rm -ks -sp "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +grep 'transitions: 1219$' stdout +grep 'states: 65$' stdout + +run 0 ../ltl2tgba -TGTA -Rm -ks "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +grep 'transitions: 1283$' stdout +grep 'states: 65$' stdout + echo '.................. TESTs: OK' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 061c530a4..da9da4581 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -282,19 +282,20 @@ syntax(char* prog) << "Options for Testing Automata:" << std::endl - << " -TA Translate an LTL formula into a Testing automata" + << " -TA Translate an LTL formula into a TA (Testing automata)" << std::endl << std::endl - << " -TM Translate an LTL formula into a minimal Testing automata" + << " -sp convert into a TA involving a single-pass emptiness check" + << std::endl << std::endl + << " -lv convert into a TA with an artificial livelock accepting" + << "state (single-pass emptiness check)" << std::endl << std::endl - << " -lv Translate an LTL formula into a Testing automata with an artificial livelock accepting state (Single-pass Testing Automata)" + << " -in convert into a TA without an artificial initial state" << std::endl << std::endl - << " -in Translate an LTL formula into a Testing automata without artificial initial state" - << std::endl - << std::endl - << " -STGTA Translate an LTL formula into a STGTA (Single-pass Transition-based Generalised Testing Automata)" + << " -TGTA Translate an LTL formula into a TGTA" + << "(Transition-based Generalised Testing Automata)" << std::endl; @@ -357,9 +358,10 @@ main(int argc, char** argv) bool reduction_dir_sim = false; spot::tgba* temp_dir_sim = 0; bool ta_opt = false; - bool tgbta_opt = false; - bool opt_with_artificial_livelock = false; + bool tgta_opt = false; bool opt_with_artificial_initial_state = true; + bool opt_single_pass_emptiness_check = false; + bool opt_with_artificial_livelock = false; for (;;) @@ -692,19 +694,18 @@ main(int argc, char** argv) { ta_opt = true; } - else if (!strcmp(argv[formula_index], "-TM")) + else if (!strcmp(argv[formula_index], "-TGTA")) { - ta_opt = true; - opt_minimize = true; - } - else if (!strcmp(argv[formula_index], "-STGTA")) - { - tgbta_opt = true; + tgta_opt = true; } else if (!strcmp(argv[formula_index], "-lv")) { opt_with_artificial_livelock = true; } + else if (!strcmp(argv[formula_index], "-sp")) + { + opt_single_pass_emptiness_check = true; + } else if (!strcmp(argv[formula_index], "-in")) { opt_with_artificial_initial_state = false; @@ -1004,7 +1005,7 @@ main(int argc, char** argv) const spot::tgba* degeneralized = 0; spot::tgba* minimized = 0; - if (opt_minimize && !ta_opt) + if (opt_minimize && !ta_opt && !tgta_opt) { tm.start("obligation minimization"); minimized = minimize_obligation(a, f); @@ -1113,24 +1114,14 @@ main(int argc, char** argv) if (ta_opt) { -// const spot::tgba_sba_proxy* degeneralized_new = 0; -// const spot::tgba_sba_proxy* degeneralized = -// dynamic_cast (a); -// if (degeneralized == 0) -// degeneralized_new = degeneralized = new spot::tgba_sba_proxy(a); - - - spot::ta* testing_automata = 0; - if (tgbta_opt) - { - testing_automata = (spot::ta_explicit *) tgba_to_tgbta(a, atomic_props_set_bdd); - } - else { - testing_automata = tgba_to_ta(a, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock, degeneralize_opt == DegenSBA); + testing_automata + = tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt + == DegenSBA, opt_with_artificial_initial_state, + opt_single_pass_emptiness_check, + opt_with_artificial_livelock); - } spot::ta* testing_automata_nm = 0; if (opt_minimize) { testing_automata_nm = testing_automata; @@ -1163,11 +1154,20 @@ main(int argc, char** argv) aut_red = 0; output = -1; - } else if (tgbta_opt) + } else if (tgta_opt) { - a = tgba_to_tgbta(a, atomic_props_set_bdd); - to_free = a; + spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd); + if (opt_minimize) + { + a = minimize_tgta(tgta); + minimized = a; + } + else + { + a = tgta; + } + to_free = tgta; } spot::tgba* product_degeneralized = 0;