From 83e7f0fa18be8372fe7a15b911feca15ea51e28a Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Tue, 5 Jul 2011 21:26:22 +0200 Subject: [PATCH] GTA (Generalized Testing Automata) implementation * src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/taproduct.hh, src/taalgos/Makefile.am, src/taalgos/dotty.cc, src/taalgos/emptinessta.cc, src/taalgos/minimize.cc, src/taalgos/minimize.hh, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgbatest/ltl2tgba.cc: changes introduced to add a new form of TA called GTA (Generalized Testing Automata). GTA is a TA with acceptance- conditions added on transitions. --- src/ta/ta.cc | 1 + src/ta/ta.hh | 22 +- src/ta/taexplicit.cc | 30 ++- src/ta/taexplicit.hh | 34 ++- src/ta/taproduct.cc | 22 ++ src/ta/taproduct.hh | 8 +- src/taalgos/Makefile.am | 5 +- src/taalgos/dotty.cc | 3 +- src/taalgos/emptinessta.cc | 31 ++- src/taalgos/minimize.cc | 27 +- src/taalgos/minimize.hh | 1 + src/taalgos/tgba2ta.cc | 501 +++++++++++++++++++++++++++++++++++++ src/taalgos/tgba2ta.hh | 51 ++++ src/tgbatest/ltl2tgba.cc | 24 +- 14 files changed, 726 insertions(+), 34 deletions(-) create mode 100644 src/taalgos/tgba2ta.cc create mode 100644 src/taalgos/tgba2ta.hh diff --git a/src/ta/ta.cc b/src/ta/ta.cc index 3d33d5a8e..8121921e7 100644 --- a/src/ta/ta.cc +++ b/src/ta/ta.cc @@ -34,6 +34,7 @@ namespace spot { index = i; is_accepting = false; + condition = bddfalse; } scc_stack_ta::connected_component& diff --git a/src/ta/ta.hh b/src/ta/ta.hh index caa9fe9df..2561b72da 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -70,7 +70,6 @@ namespace spot virtual bool is_livelock_accepting_state(const spot::state* s) const = 0; - virtual bool is_initial_state(const spot::state* s) const = 0; @@ -80,6 +79,16 @@ namespace spot virtual void free_state(const spot::state* s) const = 0; + /// \brief Return the set of all acceptance conditions used + /// by this automaton. + /// + /// The goal of the emptiness check is to ensure that + /// a strongly connected component walks through each + /// of these acceptiong conditions. I.e., the union + /// of the acceptiong conditions of all transition in + /// the SCC should be equal to the result of this function. + virtual bdd all_acceptance_conditions() const = 0; + }; /// Successor iterators used by spot::ta. @@ -107,11 +116,8 @@ namespace spot is_stuttering_transition() const = 0; bdd - current_acceptance_conditions() const - { - assert(!done()); - return bddfalse; - } + current_acceptance_conditions() const = 0; + }; // A stack of Strongly-Connected Components @@ -128,6 +134,10 @@ namespace spot bool is_accepting; + /// The bdd condition is the union of all acceptance conditions of + /// transitions which connect the states of the connected component. + bdd condition; + std::list rem; }; diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 1882c3bb1..138cc3ae0 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -83,6 +83,13 @@ namespace spot return (*i_)->condition; } + bdd + ta_explicit_succ_iterator::current_acceptance_conditions() const + { + assert(!done()); + return (*i_)->acceptance_conditions; + } + bool ta_explicit_succ_iterator::is_stuttering_transition() const { @@ -138,6 +145,10 @@ namespace spot != transitions_condition->end() && !transition_found); it_trans++) { transition_found = ((*it_trans)->dest == t->dest); + if (transition_found) + { + (*it_trans)->acceptance_conditions |= t->acceptance_conditions; + } } if (!transition_found) @@ -313,9 +324,10 @@ namespace spot // ta_explicit - ta_explicit::ta_explicit(const tgba* tgba_, + ta_explicit::ta_explicit(const tgba* tgba, bdd all_acceptance_conditions, state_ta_explicit* artificial_initial_state) : - tgba_(tgba_), artificial_initial_state_(artificial_initial_state) + tgba_(tgba), all_acceptance_conditions_(all_acceptance_conditions), + artificial_initial_state_(artificial_initial_state) { get_dict()->register_all_variables_of(&tgba_, this); if (artificial_initial_state != 0) @@ -341,6 +353,7 @@ namespace spot delete tgba_; } + state_ta_explicit* ta_explicit::add_state(state_ta_explicit* s) { @@ -386,6 +399,19 @@ namespace spot state_ta_explicit::transition* t = new state_ta_explicit::transition; t->dest = dest; t->condition = condition; + t->acceptance_conditions = bddfalse; + source->add_transition(t); + + } + + void + ta_explicit::create_transition(state_ta_explicit* source, bdd condition, + bdd acceptance_conditions, state_ta_explicit* dest) + { + state_ta_explicit::transition* t = new state_ta_explicit::transition; + t->dest = dest; + t->condition = condition; + t->acceptance_conditions = acceptance_conditions; source->add_transition(t); } diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index 1bcce96fd..bc9e03da0 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -41,8 +41,8 @@ namespace spot class ta_explicit : public ta { public: - ta_explicit(const tgba* tgba_, state_ta_explicit* artificial_initial_state = - 0); + ta_explicit(const tgba* tgba, bdd all_acceptance_conditions, + state_ta_explicit* artificial_initial_state = 0); const tgba* get_tgba() const; @@ -57,6 +57,10 @@ namespace spot create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest); + void + create_transition(state_ta_explicit* source, bdd condition, + bdd acceptance_conditions, state_ta_explicit* dest); + void delete_stuttering_transitions(); // ta interface @@ -114,16 +118,32 @@ namespace spot return states_set_; } + /// \brief Return the set of all acceptance conditions used + /// by this automaton. + /// + /// The goal of the emptiness check is to ensure that + /// a strongly connected component walks through each + /// of these acceptiong conditions. I.e., the union + /// of the acceptiong conditions of all transition in + /// the SCC should be equal to the result of this function. + bdd + all_acceptance_conditions() const + { + return all_acceptance_conditions_;; + } + + private: // Disallow copy. ta_explicit(const ta_explicit& other); ta_explicit& operator=(const ta_explicit& other); + const tgba* tgba_; + bdd all_acceptance_conditions_; + state_ta_explicit* artificial_initial_state_; ta::states_set_t states_set_; ta::states_set_t initial_states_set_; - const tgba* tgba_; - state_ta_explicit* artificial_initial_state_; }; @@ -136,6 +156,7 @@ namespace spot struct transition { bdd condition; + bdd acceptance_conditions; state_ta_explicit* dest; }; @@ -201,6 +222,8 @@ namespace spot void free_transitions(); + + private: const state* tgba_state_; const bdd tgba_condition_; @@ -232,6 +255,9 @@ namespace spot virtual bdd current_condition() const; + virtual bdd + current_acceptance_conditions() const; + virtual bool is_stuttering_transition() const; diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 067e71303..1f16d2bfd 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -190,6 +190,7 @@ namespace spot //if stuttering transition, the TA automata stays in the same state current_state_ = new state_ta_product(source_->get_ta_state(), kripke_current_dest_state->clone()); + current_acceptance_conditions_ = bddfalse; return; } @@ -197,6 +198,8 @@ namespace spot { current_state_ = new state_ta_product(ta_succ_it_->current_state(), kripke_current_dest_state->clone()); + current_acceptance_conditions_ + = ta_succ_it_->current_acceptance_conditions(); return; } @@ -249,6 +252,19 @@ namespace spot return current_condition_; } + bdd + ta_succ_iterator_product::current_acceptance_conditions() const + { + // assert(!done()); + // bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state()); + // state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); + // bdd kripke_current_dest_condition = kripke_->state_condition(kripke_succ_it_current_state); + // delete kripke_succ_it_current_state; + // return bdd_setxor(kripke_source_condition, kripke_current_dest_condition); + + return current_acceptance_conditions_; + } + //////////////////////////////////////////////////////////// // ta_product @@ -392,6 +408,12 @@ namespace spot return is_hole_state; } + bdd + ta_product::all_acceptance_conditions() const + { + return get_ta()->all_acceptance_conditions(); + } + bdd ta_product::get_state_condition(const spot::state* s) const { diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index f5a975480..93cf9d4fc 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -97,6 +97,9 @@ namespace spot bdd current_condition() const; + bdd + current_acceptance_conditions() const; + bool is_stuttering_transition() const; @@ -121,6 +124,7 @@ namespace spot tgba_succ_iterator* kripke_succ_it_; state_ta_product* current_state_; bdd current_condition_; + bdd current_acceptance_conditions_; bool is_stuttering_transition_; bdd kripke_source_condition; state * kripke_current_dest_state; @@ -173,10 +177,12 @@ namespace spot virtual bool is_hole_state_in_ta_component(const spot::state* s) const; - virtual bdd get_state_condition(const spot::state* s) const; + virtual bdd + all_acceptance_conditions() const; + virtual void free_state(const spot::state* s) const; diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am index 918b82a1a..0f2a7345f 100644 --- a/src/taalgos/Makefile.am +++ b/src/taalgos/Makefile.am @@ -25,7 +25,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) taalgosdir = $(pkgincludedir)/taalgos taalgos_HEADERS = \ - sba2ta.hh \ + tgba2ta.hh \ dotty.hh \ reachiter.hh \ stats.hh \ @@ -33,10 +33,9 @@ taalgos_HEADERS = \ minimize.hh \ emptinessta.hh - noinst_LTLIBRARIES = libtaalgos.la libtaalgos_la_SOURCES = \ - sba2ta.cc \ + tgba2ta.cc \ dotty.cc \ reachiter.cc \ stats.cc \ diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 251cbe48d..a4716d9b0 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -119,7 +119,8 @@ namespace spot os_ << " " << in << " -> " << out << " [label=\""; escape_str(os_, bdd_format_accset(t_automata_->get_dict(), - si->current_condition())) + si->current_condition()) + "\n" + bdd_format_accset( + t_automata_->get_dict(), si->current_acceptance_conditions())) << "\"]" << std::endl; diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index b9c214263..277dec58f 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -30,6 +30,7 @@ #include "emptinessta.hh" #include "misc/memusage.hh" #include +#include "tgba/bddprint.hh" namespace spot { @@ -51,6 +52,12 @@ namespace spot // We use five main data in this algorithm: + // * scc: a stack of strongly connected components (SCC) + scc; + + // * 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 = @@ -108,6 +115,7 @@ namespace spot h->insert(init, ++num); scc.push(num); + arc.push(bddfalse); ta_succ_iterator* iter = a_->succ_iter(init); iter->first(); @@ -187,6 +195,9 @@ namespace spot } dec_depth(scc.rem().size()); scc.pop(); + assert(!arc.empty()); + arc.pop(); + } delete succ; @@ -201,6 +212,8 @@ namespace spot // Fetch the values destination state we are interested in... state* dest = succ->current_state(); + bdd acc_cond = succ->current_acceptance_conditions(); + bool curr_is_livelock_hole_state_in_ta_component = (a_->is_hole_state_in_ta_component(curr)) && a_->is_livelock_accepting_state(curr); @@ -228,6 +241,7 @@ namespace spot // for later processing. h->insert(dest, ++num); scc.push(num); + arc.push(acc_cond); ta_succ_iterator* iter = a_->succ_iter(dest); iter->first(); @@ -265,13 +279,18 @@ namespace spot while (threshold < scc.top().index) { assert(!scc.empty()); + assert(!arc.empty()); acc |= scc.top().is_accepting; + acc_cond |= scc.top().condition; + acc_cond |= arc.top(); rem.splice(rem.end(), scc.rem()); scc.pop(); + arc.pop(); } + // Note that we do not always have // threshold == scc.top().index // after this loop, the SSCC whose index is threshold might have @@ -279,13 +298,23 @@ namespace spot // Accumulate all acceptance conditions into the merged SSCC. scc.top().is_accepting |= acc; + scc.top().condition |= acc_cond; scc.rem().splice(scc.rem().end(), rem); - if (scc.top().is_accepting) + bool is_accepting_sscc = (scc.top().is_accepting) + || (scc.top().condition == a_->all_acceptance_conditions()); + + if (is_accepting_sscc) { clear(h, todo, init_set); trace << "PASS 1: SUCCESS" << std::endl; + trace + << "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(), + scc.top().condition) << std::endl; + trace + << "PASS 1: a_->all_acceptance_conditions() : " << bdd_format_accset(a_->get_dict(), + a_->all_acceptance_conditions()) << std::endl; return true; } diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index c531e5142..dc43aec0e 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -37,6 +37,7 @@ #include "ta/taproduct.hh" #include "taalgos/statessetbuilder.hh" #include "tgba/tgbaexplicit.hh" +#include "tgba/bddprint.hh" namespace spot { @@ -75,7 +76,7 @@ namespace spot build_result(const ta* a, std::list& sets) { tgba_explicit_number* tgba = new tgba_explicit_number(a->get_dict()); - ta_explicit* ta = new ta_explicit(tgba); + ta_explicit* ta = new ta_explicit(tgba, a->all_acceptance_conditions()); // For each set, create a state in the tgbaulting automaton. // For a state s, state_num[s] is the number of the state in the minimal @@ -111,7 +112,7 @@ namespace spot bool is_accepting_state = a->is_accepting_state(src); bool is_livelock_accepting_state = a->is_livelock_accepting_state(src); - state_ta_explicit* new_src = new state_ta_explicit(tgba_state, + state_ta_explicit* new_src = new state_ta_explicit(tgba_state->clone(), tgba_condition, is_initial_state, is_accepting_state, is_livelock_accepting_state); @@ -150,7 +151,7 @@ namespace spot bool is_livelock_accepting_state = a->is_livelock_accepting_state( dst); - state_ta_explicit* new_dst = new state_ta_explicit(tgba_state, + state_ta_explicit* new_dst = new state_ta_explicit(tgba_state->clone(), tgba_condition, is_initial_state, is_accepting_state, is_livelock_accepting_state); @@ -169,7 +170,7 @@ namespace spot else if (is_initial_state) ta->add_to_initial_states_set(new_dst); - ta->create_transition(ta_src, succit->current_condition(), ta_dst); + ta->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst); } delete succit; @@ -245,7 +246,7 @@ namespace spot hash_map state_set_map; // Size of ta_ - unsigned size = states_set.size(); + 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_); @@ -347,6 +348,11 @@ namespace spot 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) { @@ -373,7 +379,14 @@ namespace spot hash_map::const_iterator i = state_set_map.find(dst); assert(i != state_set_map.end()); - f |= (bdd_ithvar(i->second) & si->current_condition()); + 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;; } delete si; @@ -470,7 +483,7 @@ namespace spot std::list::iterator itdone; for (itdone = done.begin(); itdone != done.end(); ++itdone) delete *itdone; - delete ta_; + //delete ta_; return res; } diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh index 367f4ae8e..547214e2c 100644 --- a/src/taalgos/minimize.hh +++ b/src/taalgos/minimize.hh @@ -30,6 +30,7 @@ namespace spot ta* minimize_ta(const ta* ta_); + /// @} } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc new file mode 100644 index 000000000..0bdb34aa0 --- /dev/null +++ b/src/taalgos/tgba2ta.cc @@ -0,0 +1,501 @@ +// 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 "tgba2ta.hh" +#include "taalgos/statessetbuilder.hh" + +using namespace std; + +namespace spot +{ + + ta* + tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_, + bool artificial_initial_state_mode, + bool artificial_livelock_accepting_state_mode, bool degeneralized) + { + + 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_, tgba_->all_acceptance_conditions(),ta_init_state); + } + else + { + ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions()); + } + + 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; + if (degeneralized) + { + init_state = new state_ta_explicit(tgba_init_state->clone(), + satone_tgba_condition, true, + ((tgba_sba_proxy*) tgba_)->state_is_accepting(tgba_init_state)); + } + else + { + init_state = new state_ta_explicit(tgba_init_state->clone(), + satone_tgba_condition, true, false); + } + + 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 tgba_acceptance_conditions = + tgba_succ_it->current_acceptance_conditions(); + 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; + if (degeneralized) + { + + new_dest = new state_ta_explicit(tgba_state->clone(), + dest_condition, false, + ((tgba_sba_proxy*) tgba_)->state_is_accepting( + tgba_state)); + + } + else + { + new_dest = new state_ta_explicit(tgba_state->clone(), + dest_condition, false, false); + + } + 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()), + tgba_acceptance_conditions, 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) + { + + 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); + + 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() + && !dest->is_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), + 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; + + // * 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->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); + 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->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)) || (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)->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); + } + + } + + 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->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); + 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; + + 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()); + 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; + + } +} diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh new file mode 100644 index 000000000..4e37e9857 --- /dev/null +++ b/src/taalgos/tgba2ta.hh @@ -0,0 +1,51 @@ +// 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* + tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set, + bool artificial_initial_state_mode = true, + bool artificial_livelock_accepting_state_mode = false, + bool degeneralized = true); + + 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/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 26e7095bc..33a0d3005 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -66,7 +66,7 @@ #include "kripkeparse/public.hh" #include "tgbaalgos/simulation.hh" -#include "taalgos/sba2ta.hh" +#include "taalgos/tgba2ta.hh" #include "taalgos/dotty.hh" #include "taalgos/stats.hh" @@ -1091,11 +1091,11 @@ 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); +// 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::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0); @@ -1104,15 +1104,19 @@ main(int argc, char** argv) != aps->end(); ++i) { bdd atomic_prop = bdd_ithvar( - (degeneralized->get_dict())->var_map[*i]); + (a->get_dict())->var_map[*i]); atomic_props_set_bdd &= atomic_prop; } delete aps; - spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock); - if (opt_minimize) testing_automata = minimize_ta(testing_automata); + spot::ta* testing_automata = tgba_to_ta(a, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock, degeneralize_opt == DegenSBA); + spot::ta* testing_automata_nm = 0; + if (opt_minimize) { + testing_automata_nm = testing_automata; + testing_automata = minimize_ta(testing_automata); + } if (output != -1) { @@ -1130,6 +1134,8 @@ main(int argc, char** argv) } tm.stop("producing output"); } + + delete testing_automata_nm; delete testing_automata; output = -1;