alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Use downcast when appropriate.

Browse source 
* src/taalgos/sba2ta.cc, src/ta/ta.cc, src/ta/taexplicit.cc,
src/ta/taproduct.cc, src/taalgos/emptinessta.cc: Use downcast
and cleanup whitespace.
This commit is contained in:
Alexandre Duret-Lutz 2011-04-06 11:03:29 +02:00
parent bf01501e15
commit c774ba141d
5 changed files with 684 additions and 678 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ta/ta.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developpement // Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement
// de l Epita (LRDE). // de l Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -78,5 +78,3 @@ namespace spot
} }

157
src/ta/taexplicit.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developpement // Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement
// de l Epita (LRDE). // de l Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -103,15 +103,15 @@ namespace spot
{ {
Sgi::hash_map<int, transitions*, Sgi::hash<int> >::const_iterator i = Sgi::hash_map<int, transitions*, Sgi::hash<int> >::const_iterator i =
transitions_by_condition.find(condition.id()); transitions_by_condition.find(condition.id());
if (i == transitions_by_condition.end()) if (i == transitions_by_condition.end())
{ {
return 0; return 0;
} }
else else
{ {
return i->second; return i->second;
} }
} }
@ -128,8 +128,8 @@ namespace spot
if (transitions_condition == 0) if (transitions_condition == 0)
{ {
transitions_condition = new transitions; transitions_condition = new transitions;
transitions_by_condition[(t->condition).id()] = transitions_condition; transitions_by_condition[(t->condition).id()] = transitions_condition;
} }
transitions_condition->push_back(t); transitions_condition->push_back(t);
@ -188,7 +188,7 @@ namespace spot
int int
state_ta_explicit::compare(const spot::state* other) const state_ta_explicit::compare(const spot::state* other) const
{ {
const state_ta_explicit* o = dynamic_cast<const state_ta_explicit*> (other); const state_ta_explicit* o = down_cast<const state_ta_explicit*> (other);
assert(o); assert(o);
int compare_value = tgba_state_->compare(o->tgba_state_); int compare_value = tgba_state_->compare(o->tgba_state_);
@ -219,37 +219,37 @@ namespace spot
if (trans != 0) if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end();) for (it_trans = trans->begin(); it_trans != trans->end();)
{ {
state_ta_explicit* dest = (*it_trans)->dest; state_ta_explicit* dest = (*it_trans)->dest;
bool is_stuttering_transition = (get_tgba_condition() bool is_stuttering_transition = (get_tgba_condition()
== (dest)->get_tgba_condition()); == (dest)->get_tgba_condition());
bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); 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 (is_stuttering_transition)
{ {
if (dest_is_livelock_accepting) if (dest_is_livelock_accepting)
set_livelock_accepting_state(true); set_livelock_accepting_state(true);
if (dest->is_initial_state()) if (dest->is_initial_state())
set_initial_state(true); set_initial_state(true);
} }
//remove hole successors states //remove hole successors states
state_ta_explicit::transitions* dest_trans = state_ta_explicit::transitions* dest_trans =
(dest)->get_transitions(); (dest)->get_transitions();
bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();
if (is_stuttering_transition || (dest_trans_empty if (is_stuttering_transition || (dest_trans_empty
&& (!dest_is_livelock_accepting))) && (!dest_is_livelock_accepting)))
{ {
get_transitions((*it_trans)->condition)->remove(*it_trans); get_transitions((*it_trans)->condition)->remove(*it_trans);
delete (*it_trans); delete (*it_trans);
it_trans = trans->erase(it_trans); it_trans = trans->erase(it_trans);
} }
else else
{ {
it_trans++; it_trans++;
} }
} }
} }
@ -262,18 +262,18 @@ namespace spot
// they are not cloned. // they are not cloned.
if (trans != 0) if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++)
{ {
delete *it_trans; delete *it_trans;
} }
delete trans; delete trans;
get_tgba_state()->destroy(); get_tgba_state()->destroy();
Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i = Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i =
transitions_by_condition.begin(); transitions_by_condition.begin();
while (i != transitions_by_condition.end()) while (i != transitions_by_condition.end())
{ {
delete i->second; delete i->second;
++i; ++i;
} }
} }
@ -293,10 +293,10 @@ namespace spot
ta::states_set_t::iterator it; ta::states_set_t::iterator it;
for (it = states_set_.begin(); it != states_set_.end(); it++) for (it = states_set_.begin(); it != states_set_.end(); it++)
{ {
state_ta_explicit* s = dynamic_cast<state_ta_explicit*> (*it); state_ta_explicit* s = down_cast<state_ta_explicit*> (*it);
s->free_transitions(); s->free_transitions();
delete s; delete s;
} }
get_dict()->unregister_all_my_variables(this); get_dict()->unregister_all_my_variables(this);
delete tgba_; delete tgba_;
@ -306,17 +306,17 @@ namespace spot
ta_explicit::add_state(state_ta_explicit* s) ta_explicit::add_state(state_ta_explicit* s)
{ {
std::pair<ta::states_set_t::iterator, bool> add_state_to_ta = std::pair<ta::states_set_t::iterator, bool> add_state_to_ta =
states_set_.insert(s); states_set_.insert(s);
return dynamic_cast<state_ta_explicit*> (*add_state_to_ta.first); return static_cast<state_ta_explicit*> (*add_state_to_ta.first);
} }
void void
ta_explicit::add_to_initial_states_set(state* state) ta_explicit::add_to_initial_states_set(state* state)
{ {
state_ta_explicit * s = dynamic_cast<state_ta_explicit*> (state); state_ta_explicit * s = down_cast<state_ta_explicit*> (state);
assert(s);
s->set_initial_state(true); s->set_initial_state(true);
initial_states_set_.insert(s); initial_states_set_.insert(s);
@ -326,7 +326,8 @@ namespace spot
void void
ta_explicit::delete_stuttering_and_hole_successors(spot::state* s) ta_explicit::delete_stuttering_and_hole_successors(spot::state* s)
{ {
state_ta_explicit * state = dynamic_cast<state_ta_explicit*> (s); state_ta_explicit * state = down_cast<state_ta_explicit*> (s);
assert(state);
state->delete_stuttering_and_hole_successors(); state->delete_stuttering_and_hole_successors();
if (state->is_initial_state()) add_to_initial_states_set(state); if (state->is_initial_state()) add_to_initial_states_set(state);
@ -354,35 +355,39 @@ namespace spot
ta_explicit::get_state_condition(const spot::state* initial_state) const ta_explicit::get_state_condition(const spot::state* initial_state) const
{ {
const state_ta_explicit* sta = const state_ta_explicit* sta =
dynamic_cast<const state_ta_explicit*> (initial_state); down_cast<const state_ta_explicit*> (initial_state);
assert(sta);
return sta->get_tgba_condition(); return sta->get_tgba_condition();
} }
bool bool
ta_explicit::is_accepting_state(const spot::state* s) const ta_explicit::is_accepting_state(const spot::state* s) const
{ {
const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s); const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
assert(sta);
return sta->is_accepting_state(); return sta->is_accepting_state();
} }
bool bool
ta_explicit::is_initial_state(const spot::state* s) const ta_explicit::is_initial_state(const spot::state* s) const
{ {
const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s); const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
assert(sta);
return sta->is_initial_state(); return sta->is_initial_state();
} }
bool bool
ta_explicit::is_livelock_accepting_state(const spot::state* s) const ta_explicit::is_livelock_accepting_state(const spot::state* s) const
{ {
const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s); const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
assert(sta);
return sta->is_livelock_accepting_state(); return sta->is_livelock_accepting_state();
} }
ta_succ_iterator* ta_succ_iterator*
ta_explicit::succ_iter(const spot::state* state) const ta_explicit::succ_iter(const spot::state* state) const
{ {
const state_ta_explicit* s = dynamic_cast<const state_ta_explicit*> (state); const state_ta_explicit* s = down_cast<const state_ta_explicit*> (state);
assert(s); assert(s);
return new ta_explicit_succ_iterator(s); return new ta_explicit_succ_iterator(s);
} }
@ -390,7 +395,7 @@ namespace spot
ta_succ_iterator* ta_succ_iterator*
ta_explicit::succ_iter(const spot::state* state, bdd condition) const ta_explicit::succ_iter(const spot::state* state, bdd condition) const
{ {
const state_ta_explicit* s = dynamic_cast<const state_ta_explicit*> (state); const state_ta_explicit* s = down_cast<const state_ta_explicit*> (state);
assert(s); assert(s);
return new ta_explicit_succ_iterator(s, condition); return new ta_explicit_succ_iterator(s, condition);
} }
@ -410,14 +415,14 @@ namespace spot
std::string std::string
ta_explicit::format_state(const spot::state* s) const ta_explicit::format_state(const spot::state* s) const
{ {
const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s); const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
assert(sta); assert(sta);
if (sta->get_tgba_condition() == bddtrue) if (sta->get_tgba_condition() == bddtrue)
return tgba_->format_state(sta->get_tgba_state()); return tgba_->format_state(sta->get_tgba_state());
return tgba_->format_state(sta->get_tgba_state()) + "\n" return tgba_->format_state(sta->get_tgba_state()) + "\n"
+ bdd_format_formula(get_dict(), sta->get_tgba_condition()); + bdd_format_formula(get_dict(), sta->get_tgba_condition());
} }
@ -428,26 +433,26 @@ namespace spot
for (it = states_set_.begin(); it != states_set_.end(); it++) for (it = states_set_.begin(); it != states_set_.end(); it++)
{ {
const state_ta_explicit* source = const state_ta_explicit* source =
dynamic_cast<const state_ta_explicit*> (*it); static_cast<const state_ta_explicit*> (*it);
state_ta_explicit::transitions* trans = source->get_transitions(); state_ta_explicit::transitions* trans = source->get_transitions();
state_ta_explicit::transitions::iterator it_trans; state_ta_explicit::transitions::iterator it_trans;
if (trans != 0) if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end();) for (it_trans = trans->begin(); it_trans != trans->end();)
{ {
if (source->get_tgba_condition() if (source->get_tgba_condition()
== ((*it_trans)->dest)->get_tgba_condition()) == ((*it_trans)->dest)->get_tgba_condition())
{ {
delete *it_trans; delete *it_trans;
it_trans = trans->erase(it_trans); it_trans = trans->erase(it_trans);
} }
else else
{ {
it_trans++; it_trans++;
} }
} }
} }
} }

121
src/ta/taproduct.cc
View file

@ -31,7 +31,7 @@ namespace spot
state_ta_product::state_ta_product(const state_ta_product& o) : state_ta_product::state_ta_product(const state_ta_product& o) :
state(), ta_state_(o.get_ta_state()), kripke_state_( state(), ta_state_(o.get_ta_state()), kripke_state_(
o.get_kripke_state()->clone()) o.get_kripke_state()->clone())
{ {
} }
@ -44,7 +44,7 @@ namespace spot
int int
state_ta_product::compare(const state* other) const state_ta_product::compare(const state* other) const
{ {
const state_ta_product* o = dynamic_cast<const state_ta_product*> (other); const state_ta_product* o = down_cast<const state_ta_product*> (other);
assert(o); assert(o);
int res = ta_state_->compare(o->get_ta_state()); int res = ta_state_->compare(o->get_ta_state());
if (res != 0) if (res != 0)
@ -91,9 +91,9 @@ namespace spot
ta_succ_it_->next(); ta_succ_it_->next();
if (ta_succ_it_->done()) if (ta_succ_it_->done())
{ {
delete ta_succ_it_; delete ta_succ_it_;
ta_succ_it_ = 0; ta_succ_it_ = 0;
kripke_succ_it_->next(); kripke_succ_it_->next();
} }
} }
@ -111,9 +111,9 @@ namespace spot
// done().) // done().)
if (kripke_succ_it_->done()) if (kripke_succ_it_->done())
{ {
delete kripke_succ_it_; delete kripke_succ_it_;
kripke_succ_it_ = 0; kripke_succ_it_ = 0;
return; return;
} }
next_non_stuttering_(); next_non_stuttering_();
@ -126,8 +126,8 @@ namespace spot
current_state_ = 0; current_state_ = 0;
if (is_stuttering_transition()) if (is_stuttering_transition())
{ {
ta_succ_it_ = 0; ta_succ_it_ = 0;
kripke_succ_it_->next(); kripke_succ_it_->next();
} }
else else
step_(); step_();
@ -144,34 +144,34 @@ namespace spot
while (!done()) while (!done())
{ {
state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
bdd dc = kripke_->state_condition(kripke_succ_it_current_state); bdd dc = kripke_->state_condition(kripke_succ_it_current_state);
is_stuttering_transition_ = (sc == dc); is_stuttering_transition_ = (sc == dc);
if (is_stuttering_transition_) if (is_stuttering_transition_)
{ {
//if stuttering transition, the TA automata stays in the same state //if stuttering transition, the TA automata stays in the same state
current_state_ = new state_ta_product(source_->get_ta_state(), current_state_ = new state_ta_product(source_->get_ta_state(),
kripke_succ_it_current_state); kripke_succ_it_current_state);
current_condition_ = bddtrue; current_condition_ = bddtrue;
return; return;
} }
if (ta_succ_it_ == 0){ if (ta_succ_it_ == 0){
current_condition_ = bdd_setxor(sc, dc); current_condition_ = bdd_setxor(sc, dc);
ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_); ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_);
ta_succ_it_->first(); ta_succ_it_->first();
} }
if (!ta_succ_it_->done()) if (!ta_succ_it_->done())
{ {
current_state_ = new state_ta_product(ta_succ_it_->current_state(), current_state_ = new state_ta_product(ta_succ_it_->current_state(),
kripke_succ_it_current_state); kripke_succ_it_current_state);
return; return;
} }
kripke_succ_it_current_state->destroy(); kripke_succ_it_current_state->destroy();
step_(); step_();
} }
} }
@ -227,7 +227,7 @@ namespace spot
ta_product::ta_product(const ta* testing_automata, ta_product::ta_product(const ta* testing_automata,
const kripke* kripke_structure) : const kripke* kripke_structure) :
dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_( dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_(
kripke_structure) kripke_structure)
{ {
assert(dict_ == kripke_structure->get_dict()); assert(dict_ == kripke_structure->get_dict());
dict_->register_all_variables_of(&ta_, this); dict_->register_all_variables_of(&ta_, this);
@ -252,19 +252,19 @@ namespace spot
for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++)
{ {
state* kripke_init_state = kripke_->get_init_state(); state* kripke_init_state = kripke_->get_init_state();
if ((kripke_->state_condition(kripke_init_state)) if ((kripke_->state_condition(kripke_init_state))
== (ta_->get_state_condition(*it))) == (ta_->get_state_condition(*it)))
{ {
state_ta_product* stp = new state_ta_product((*it), state_ta_product* stp = new state_ta_product((*it),
kripke_init_state); kripke_init_state);
initial_states_set.insert(stp); initial_states_set.insert(stp);
} }
else else
{ {
kripke_init_state->destroy(); kripke_init_state->destroy();
} }
} }
@ -274,7 +274,7 @@ namespace spot
ta_succ_iterator_product* ta_succ_iterator_product*
ta_product::succ_iter(const state* s) const ta_product::succ_iter(const state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(s); assert(s);
return new ta_succ_iterator_product(stp, ta_, kripke_); return new ta_succ_iterator_product(stp, ta_, kripke_);
@ -289,16 +289,17 @@ namespace spot
std::string std::string
ta_product::format_state(const state* state) const ta_product::format_state(const state* state) const
{ {
const state_ta_product* s = dynamic_cast<const state_ta_product*> (state); const state_ta_product* s = down_cast<const state_ta_product*> (state);
assert(s); assert(s);
return kripke_->format_state(s->get_kripke_state()) + " * \n" return kripke_->format_state(s->get_kripke_state()) + " * \n"
+ ta_->format_state(s->get_ta_state()); + ta_->format_state(s->get_ta_state());
} }
bool bool
ta_product::is_accepting_state(const spot::state* s) const ta_product::is_accepting_state(const spot::state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(stp);
return ta_->is_accepting_state(stp->get_ta_state()); return ta_->is_accepting_state(stp->get_ta_state());
} }
@ -306,7 +307,8 @@ namespace spot
bool bool
ta_product::is_livelock_accepting_state(const spot::state* s) const ta_product::is_livelock_accepting_state(const spot::state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(stp);
return ta_->is_livelock_accepting_state(stp->get_ta_state()); return ta_->is_livelock_accepting_state(stp->get_ta_state());
} }
@ -314,21 +316,23 @@ namespace spot
bool bool
ta_product::is_initial_state(const spot::state* s) const ta_product::is_initial_state(const spot::state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(stp);
state* ta_s = stp->get_ta_state(); state* ta_s = stp->get_ta_state();
state* kr_s = stp->get_kripke_state(); state* kr_s = stp->get_kripke_state();
return (ta_->is_initial_state(ta_s)) return (ta_->is_initial_state(ta_s))
&& ((kripke_->get_init_state())->compare(kr_s) == 0) && ((kripke_->get_init_state())->compare(kr_s) == 0)
&& ((kripke_->state_condition(kr_s)) && ((kripke_->state_condition(kr_s))
== (ta_->get_state_condition(ta_s))); == (ta_->get_state_condition(ta_s)));
} }
bdd bdd
ta_product::get_state_condition(const spot::state* s) const ta_product::get_state_condition(const spot::state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(stp);
state* ta_s = stp->get_ta_state(); state* ta_s = stp->get_ta_state();
return ta_->get_state_condition(ta_s); return ta_->get_state_condition(ta_s);
} }
@ -337,7 +341,8 @@ namespace spot
ta_product::free_state(const spot::state* s) const ta_product::free_state(const spot::state* s) const
{ {
const state_ta_product* stp = dynamic_cast<const state_ta_product*> (s); const state_ta_product* stp = down_cast<const state_ta_product*> (s);
assert(stp);
ta_->free_state(stp->get_ta_state()); ta_->free_state(stp->get_ta_state());
delete stp; delete stp;

681
src/taalgos/emptinessta.cc
View file

@ -1,8 +1,5 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement // Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -57,7 +54,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. 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 // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -74,7 +71,7 @@ namespace spot
std::stack<spot::state*> init_set; std::stack<spot::state*> init_set;
Sgi::hash_map<const state*, std::string, state_ptr_hash, state_ptr_equal> Sgi::hash_map<const state*, std::string, state_ptr_hash, state_ptr_equal>
colour; colour;
trace trace
<< "PASS 1" << std::endl; << "PASS 1" << std::endl;
@ -84,7 +81,7 @@ namespace spot
//const std::string BLACK = "BK"; //const std::string BLACK = "BK";
Sgi::hash_map<const state*, std::set<const state*, state_ptr_less_than>, Sgi::hash_map<const state*, std::set<const state*, state_ptr_less_than>,
state_ptr_hash, state_ptr_equal> liveset; state_ptr_hash, state_ptr_equal> liveset;
std::stack<spot::state*> livelock_roots; std::stack<spot::state*> livelock_roots;
@ -92,233 +89,233 @@ namespace spot
ta::states_set_t::const_iterator it; ta::states_set_t::const_iterator it;
for (it = init_states_set.begin(); it != init_states_set.end(); it++) for (it = init_states_set.begin(); it != init_states_set.end(); it++)
{ {
state* init_state = (*it); state* init_state = (*it);
init_set.push(init_state); init_set.push(init_state);
//colour[init_state] = WHITE; //colour[init_state] = WHITE;
} }
while (!init_set.empty()) while (!init_set.empty())
{ {
// Setup depth-first search from initial states. // Setup depth-first search from initial states.
{ {
state* init = dynamic_cast<state*> (init_set.top()); state* init = init_set.top();
init_set.pop(); init_set.pop();
numbered_state_heap::state_index_p h_init = h->find(init); numbered_state_heap::state_index_p h_init = h->find(init);
if (h_init.first) if (h_init.first)
continue; continue;
h->insert(init, ++num); h->insert(init, ++num);
scc.push(num); scc.push(num);
ta_succ_iterator* iter = a_->succ_iter(init); ta_succ_iterator* iter = a_->succ_iter(init);
iter->first(); iter->first();
todo.push(pair_state_iter(init, iter)); todo.push(pair_state_iter(init, iter));
//colour[init] = GREY; //colour[init] = GREY;
inc_depth(); inc_depth();
//push potential root of live-lock accepting cycle //push potential root of live-lock accepting cycle
if (a_->is_livelock_accepting_state(init)) if (a_->is_livelock_accepting_state(init))
livelock_roots.push(init); livelock_roots.push(init);
} }
while (!todo.empty()) while (!todo.empty())
{ {
state* curr = todo.top().first; state* curr = todo.top().first;
// We are looking at the next successor in SUCC. // We are looking at the next successor in SUCC.
ta_succ_iterator* succ = todo.top().second; ta_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack. // If there is no more successor, backtrack.
if (succ->done()) if (succ->done())
{ {
// We have explored all successors of state CURR. // We have explored all successors of state CURR.
// Backtrack TODO. // Backtrack TODO.
todo.pop(); todo.pop();
dec_depth(); dec_depth();
trace trace
<< "PASS 1 : backtrack" << std::endl; << "PASS 1 : backtrack" << std::endl;
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = numbered_state_heap::state_index_p spi =
h->index(curr->clone()); h->index(curr->clone());
assert(spi.first); assert(spi.first);
scc.rem().push_front(curr); scc.rem().push_front(curr);
inc_depth(); inc_depth();
// set the h value of the Backtracked state to negative value. // set the h value of the Backtracked state to negative value.
// colour[curr] = BLUE; // colour[curr] = BLUE;
*spi.second = -std::abs(*spi.second); *spi.second = -std::abs(*spi.second);
// Backtrack livelock_roots. // Backtrack livelock_roots.
if (!livelock_roots.empty() && !livelock_roots.top()->compare( if (!livelock_roots.empty() && !livelock_roots.top()->compare(
curr)) curr))
livelock_roots.pop(); livelock_roots.pop();
// When backtracking the root of an SSCC, we must also // When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!scc.empty()); assert(!scc.empty());
if (scc.top().index == std::abs(*spi.second)) if (scc.top().index == std::abs(*spi.second))
{ {
// removing states // removing states
std::list<state*>::iterator i; std::list<state*>::iterator i;
for (i = scc.rem().begin(); i != scc.rem().end(); ++i) for (i = scc.rem().begin(); i != scc.rem().end(); ++i)
{ {
numbered_state_heap::state_index_p spi = h->index( numbered_state_heap::state_index_p spi = h->index(
(*i)->clone()); (*i)->clone());
assert(spi.first->compare(*i) == 0); assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1); assert(*spi.second != -1);
*spi.second = -1; *spi.second = -1;
//colour[*i] = BLACK; //colour[*i] = BLACK;
} }
dec_depth(scc.rem().size()); dec_depth(scc.rem().size());
scc.pop(); scc.pop();
} }
delete succ; delete succ;
// Do not delete CURR: it is a key in H. // Do not delete CURR: it is a key in H.
continue; continue;
} }
// We have a successor to look at. // We have a successor to look at.
inc_transitions(); inc_transitions();
trace trace
<< "PASS 1: transition" << std::endl; << "PASS 1: transition" << std::endl;
// Fetch the values destination state we are interested in... // Fetch the values destination state we are interested in...
state* dest = succ->current_state(); state* dest = succ->current_state();
//may be Buchi accepting scc //may be Buchi accepting scc
scc.top().is_accepting = a_->is_accepting_state(curr) scc.top().is_accepting = a_->is_accepting_state(curr)
&& !succ->is_stuttering_transition(); && !succ->is_stuttering_transition();
bool is_stuttering_transition = succ->is_stuttering_transition(); bool is_stuttering_transition = succ->is_stuttering_transition();
// ... and point the iterator to the next successor, for // ... and point the iterator to the next successor, for
// the next iteration. // the next iteration.
succ->next(); succ->next();
// We do not need SUCC from now on. // We do not need SUCC from now on.
// Are we going to a new state? // Are we going to a new state?
numbered_state_heap::state_index_p spi = h->find(dest); numbered_state_heap::state_index_p spi = h->find(dest);
// Is this a new state? // Is this a new state?
if (!spi.first) if (!spi.first)
{ {
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest, ++num); h->insert(dest, ++num);
scc.push(num); scc.push(num);
ta_succ_iterator* iter = a_->succ_iter(dest); ta_succ_iterator* iter = a_->succ_iter(dest);
iter->first(); iter->first();
todo.push(pair_state_iter(dest, iter)); todo.push(pair_state_iter(dest, iter));
//colour[dest] = GREY; //colour[dest] = GREY;
inc_depth(); inc_depth();
//push potential root of live-lock accepting cycle //push potential root of live-lock accepting cycle
if (a_->is_livelock_accepting_state(dest) if (a_->is_livelock_accepting_state(dest)
&& !is_stuttering_transition) && !is_stuttering_transition)
livelock_roots.push(dest); livelock_roots.push(dest);
continue; continue;
} }
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (*spi.second == -1)
continue; continue;
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such // state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to // non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs // this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between // to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC. // this S1 and S2 into this SSCC.
// //
// This merge is easy to do because the order of the SSCC in // 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 // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = std::abs(*spi.second); int threshold = std::abs(*spi.second);
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
while (threshold < scc.top().index) while (threshold < scc.top().index)
{ {
assert(!scc.empty()); assert(!scc.empty());
acc |= scc.top().is_accepting; acc |= scc.top().is_accepting;
rem.splice(rem.end(), scc.rem()); rem.splice(rem.end(), scc.rem());
scc.pop(); scc.pop();
} }
// Note that we do not always have // Note that we do not always have
// threshold == scc.top().index // threshold == scc.top().index
// after this loop, the SSCC whose index is threshold might have // after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC. // been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC. // Accumulate all acceptance conditions into the merged SSCC.
scc.top().is_accepting |= acc; scc.top().is_accepting |= acc;
scc.rem().splice(scc.rem().end(), rem); scc.rem().splice(scc.rem().end(), rem);
if (scc.top().is_accepting) if (scc.top().is_accepting)
{ {
clear(h, todo, init_set); clear(h, todo, init_set);
trace trace
<< "PASS 1: SUCCESS" << std::endl; << "PASS 1: SUCCESS" << std::endl;
return true; return true;
} }
//ADDLINKS //ADDLINKS
if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr) if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr)
&& is_stuttering_transition) && is_stuttering_transition)
{ {
trace trace
<< "PASS 1: heuristic livelock detection " << std::endl; << "PASS 1: heuristic livelock detection " << std::endl;
const state* dest = spi.first; const state* dest = spi.first;
std::set<const state*, state_ptr_less_than> liveset_dest = std::set<const state*, state_ptr_less_than> liveset_dest =
liveset[dest]; liveset[dest];
std::set<const state*, state_ptr_less_than> liveset_curr = std::set<const state*, state_ptr_less_than> liveset_curr =
liveset[curr]; liveset[curr];
int h_livelock_root = 0; int h_livelock_root = 0;
if (!livelock_roots.empty()) if (!livelock_roots.empty())
h_livelock_root = *(h->find((livelock_roots.top()))).second; h_livelock_root = *(h->find((livelock_roots.top()))).second;
if (heuristic_livelock_detection(dest, h, h_livelock_root, if (heuristic_livelock_detection(dest, h, h_livelock_root,
liveset_curr)) liveset_curr))
{ {
clear(h, todo, init_set); clear(h, todo, init_set);
return true; return true;
} }
std::set<const state*, state_ptr_less_than>::const_iterator it; std::set<const state*, state_ptr_less_than>::const_iterator it;
for (it = liveset_dest.begin(); it != liveset_dest.end(); it++) for (it = liveset_dest.begin(); it != liveset_dest.end(); it++)
{ {
const state* succ = (*it); const state* succ = (*it);
if (heuristic_livelock_detection(succ, h, h_livelock_root, if (heuristic_livelock_detection(succ, h, h_livelock_root,
liveset_curr)) liveset_curr))
{ {
clear(h, todo, init_set); clear(h, todo, init_set);
return true; return true;
} }
} }
} }
} }
} }
@ -329,21 +326,21 @@ namespace spot
bool bool
ta_check::heuristic_livelock_detection(const state * u, ta_check::heuristic_livelock_detection(const state * u,
numbered_state_heap* h, int h_livelock_root, std::set<const state*, numbered_state_heap* h, int h_livelock_root, std::set<const state*,
state_ptr_less_than> liveset_curr) state_ptr_less_than> liveset_curr)
{ {
numbered_state_heap::state_index_p hu = h->find(u); numbered_state_heap::state_index_p hu = h->find(u);
if (*hu.second > 0) // colour[u] == GREY if (*hu.second > 0) // colour[u] == GREY
{ {
if (*hu.second >= h_livelock_root) if (*hu.second >= h_livelock_root)
{ {
trace trace
<< "PASS 1: heuristic livelock detection SUCCESS" << std::endl; << "PASS 1: heuristic livelock detection SUCCESS" << std::endl;
return true; return true;
} }
liveset_curr.insert(u); liveset_curr.insert(u);
} }
return false; return false;
@ -361,7 +358,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. 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 // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -387,8 +384,8 @@ namespace spot
ta::states_set_t::const_iterator it; ta::states_set_t::const_iterator it;
for (it = init_states_set.begin(); it != init_states_set.end(); it++) for (it = init_states_set.begin(); it != init_states_set.end(); it++)
{ {
state* init_state = (*it); state* init_state = (*it);
init_set.push(init_state); init_set.push(init_state);
} }
@ -396,180 +393,180 @@ namespace spot
while (!init_set.empty()) while (!init_set.empty())
{ {
// Setup depth-first search from initial states. // Setup depth-first search from initial states.
{ {
state* init = init_set.top(); state* init = init_set.top();
init_set.pop(); init_set.pop();
numbered_state_heap::state_index_p h_init = h->find(init); numbered_state_heap::state_index_p h_init = h->find(init);
if (h_init.first) if (h_init.first)
continue; continue;
h->insert(init, ++num); h->insert(init, ++num);
sscc.push(num); sscc.push(num);
sscc.top().is_accepting = t->is_livelock_accepting_state(init); sscc.top().is_accepting = t->is_livelock_accepting_state(init);
ta_succ_iterator* iter = t->succ_iter(init); ta_succ_iterator* iter = t->succ_iter(init);
iter->first(); iter->first();
todo.push(pair_state_iter(init, iter)); todo.push(pair_state_iter(init, iter));
inc_depth(); inc_depth();
} }
while (!todo.empty()) while (!todo.empty())
{ {
state* curr = todo.top().first; state* curr = todo.top().first;
// We are looking at the next successor in SUCC. // We are looking at the next successor in SUCC.
ta_succ_iterator* succ = todo.top().second; ta_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack. // If there is no more successor, backtrack.
if (succ->done()) if (succ->done())
{ {
// We have explored all successors of state CURR. // We have explored all successors of state CURR.
// Backtrack TODO. // Backtrack TODO.
todo.pop(); todo.pop();
dec_depth(); dec_depth();
trace trace
<< "PASS 2 : backtrack" << std::endl; << "PASS 2 : backtrack" << std::endl;
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = numbered_state_heap::state_index_p spi =
h->index(curr->clone()); h->index(curr->clone());
assert(spi.first); assert(spi.first);
sscc.rem().push_front(curr); sscc.rem().push_front(curr);
inc_depth(); inc_depth();
// When backtracking the root of an SSCC, we must also // When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!sscc.empty()); assert(!sscc.empty());
if (sscc.top().index == *spi.second) if (sscc.top().index == *spi.second)
{ {
// removing states // removing states
std::list<state*>::iterator i; std::list<state*>::iterator i;
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{ {
numbered_state_heap::state_index_p spi = h->index( numbered_state_heap::state_index_p spi = h->index(
(*i)->clone()); (*i)->clone());
assert(spi.first->compare(*i) == 0); assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1); assert(*spi.second != -1);
*spi.second = -1; *spi.second = -1;
} }
dec_depth(sscc.rem().size()); dec_depth(sscc.rem().size());
sscc.pop(); sscc.pop();
} }
delete succ; delete succ;
// Do not delete CURR: it is a key in H. // Do not delete CURR: it is a key in H.
continue; continue;
} }
// We have a successor to look at. // We have a successor to look at.
inc_transitions(); inc_transitions();
trace trace
<< "PASS 2 : transition" << std::endl; << "PASS 2 : transition" << std::endl;
// Fetch the values destination state we are interested in... // Fetch the values destination state we are interested in...
state* dest = succ->current_state(); state* dest = succ->current_state();
bool is_stuttering_transition = succ->is_stuttering_transition(); bool is_stuttering_transition = succ->is_stuttering_transition();
// ... and point the iterator to the next successor, for // ... and point the iterator to the next successor, for
// the next iteration. // the next iteration.
succ->next(); succ->next();
// We do not need SUCC from now on. // We do not need SUCC from now on.
numbered_state_heap::state_index_p spi = h->find(dest); numbered_state_heap::state_index_p spi = h->find(dest);
// Is this a new state? // Is this a new state?
if (!spi.first) if (!spi.first)
{ {
// Are we going to a new state through a stuttering transition? // Are we going to a new state through a stuttering transition?
if (!is_stuttering_transition) if (!is_stuttering_transition)
{ {
init_set.push(dest); init_set.push(dest);
continue; continue;
} }
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest, ++num); h->insert(dest, ++num);
sscc.push(num); sscc.push(num);
sscc.top().is_accepting = t->is_livelock_accepting_state(dest); sscc.top().is_accepting = t->is_livelock_accepting_state(dest);
ta_succ_iterator* iter = t->succ_iter(dest); ta_succ_iterator* iter = t->succ_iter(dest);
iter->first(); iter->first();
todo.push(pair_state_iter(dest, iter)); todo.push(pair_state_iter(dest, iter));
inc_depth(); inc_depth();
continue; continue;
} }
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (*spi.second == -1)
continue; continue;
//self loop state //self loop state
if (!curr->compare(spi.first)) if (!curr->compare(spi.first))
{ {
state * self_loop_state = (curr); state * self_loop_state = (curr);
if (t->is_livelock_accepting_state(self_loop_state)) if (t->is_livelock_accepting_state(self_loop_state))
{ {
clear(h, todo, init_set); clear(h, todo, init_set);
trace trace
<< "PASS 2: SUCCESS" << std::endl; << "PASS 2: SUCCESS" << std::endl;
return true; return true;
} }
} }
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such // state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to // non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs // this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between // to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC. // this S1 and S2 into this SSCC.
// //
// This merge is easy to do because the order of the SSCC in // 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 // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = *spi.second; int threshold = *spi.second;
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
while (threshold < sscc.top().index) while (threshold < sscc.top().index)
{ {
assert(!sscc.empty()); assert(!sscc.empty());
acc |= sscc.top().is_accepting; acc |= sscc.top().is_accepting;
rem.splice(rem.end(), sscc.rem()); rem.splice(rem.end(), sscc.rem());
sscc.pop(); sscc.pop();
} }
// Note that we do not always have // Note that we do not always have
// threshold == sscc.top().index // threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have // after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC. // been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC. // Accumulate all acceptance conditions into the merged SSCC.
sscc.top().is_accepting |= acc; sscc.top().is_accepting |= acc;
sscc.rem().splice(sscc.rem().end(), rem); sscc.rem().splice(sscc.rem().end(), rem);
if (sscc.top().is_accepting) if (sscc.top().is_accepting)
{ {
clear(h, todo, init_set); clear(h, todo, init_set);
trace trace
<< "PASS 2: SUCCESS" << std::endl; << "PASS 2: SUCCESS" << std::endl;
return true; return true;
} }
} }
} }
clear(h, todo, init_set); clear(h, todo, init_set);
@ -585,16 +582,16 @@ namespace spot
while (!init_states.empty()) while (!init_states.empty())
{ {
a_->free_state(init_states.top()); a_->free_state(init_states.top());
init_states.pop(); init_states.pop();
} }
// Release all iterators in TODO. // Release all iterators in TODO.
while (!todo.empty()) while (!todo.empty())
{ {
delete todo.top().second; delete todo.top().second;
todo.pop(); todo.pop();
dec_depth(); dec_depth();
} }
delete h; delete h;
} }
@ -607,7 +604,7 @@ namespace spot
//TODO sscc; //TODO sscc;
os << scc.size() << " strongly connected components in search stack" os << scc.size() << " strongly connected components in search stack"
<< std::endl; << std::endl;
os << transitions() << " transitions explored" << std::endl; os << transitions() << " transitions explored" << std::endl;
os << max_depth() << " items max in DFS search stack" << std::endl; os << max_depth() << " items max in DFS search stack" << std::endl;
return os; return os;

399
src/taalgos/sba2ta.cc
View file

@ -50,70 +50,70 @@ namespace spot
bdd satone_tgba_condition; bdd satone_tgba_condition;
while ((satone_tgba_condition = bdd_satoneset(tgba_condition, while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
atomic_propositions_set_, bddtrue)) != bddfalse) atomic_propositions_set_, bddtrue)) != bddfalse)
{ {
tgba_condition -= satone_tgba_condition; tgba_condition -= satone_tgba_condition;
state_ta_explicit* init_state = new state_ta_explicit( state_ta_explicit* init_state = new state_ta_explicit(
tgba_init_state->clone(), satone_tgba_condition, true, tgba_init_state->clone(), satone_tgba_condition, true,
tgba_->state_is_accepting(tgba_init_state)); tgba_->state_is_accepting(tgba_init_state));
state_ta_explicit* is = ta->add_state(init_state); state_ta_explicit* is = ta->add_state(init_state);
assert(is == init_state); assert(is == init_state);
ta->add_to_initial_states_set(is); ta->add_to_initial_states_set(is);
todo.push(init_state); todo.push(init_state);
} }
tgba_init_state->destroy(); tgba_init_state->destroy();
while (!todo.empty()) while (!todo.empty())
{ {
state_ta_explicit* source = todo.top(); state_ta_explicit* source = todo.top();
todo.pop(); todo.pop();
tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter(
source->get_tgba_state()); source->get_tgba_state());
for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next()) for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next())
{ {
const state* tgba_state = tgba_succ_it->current_state(); const state* tgba_state = tgba_succ_it->current_state();
bdd tgba_condition = tgba_succ_it->current_condition(); bdd tgba_condition = tgba_succ_it->current_condition();
bdd satone_tgba_condition; bdd satone_tgba_condition;
while ((satone_tgba_condition = bdd_satoneset(tgba_condition, while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
atomic_propositions_set_, bddtrue)) != bddfalse) atomic_propositions_set_, bddtrue)) != bddfalse)
{ {
tgba_condition -= satone_tgba_condition; tgba_condition -= satone_tgba_condition;
bdd all_props = bddtrue; bdd all_props = bddtrue;
bdd dest_condition; bdd dest_condition;
if (satone_tgba_condition == source->get_tgba_condition()) if (satone_tgba_condition == source->get_tgba_condition())
while ((dest_condition = bdd_satoneset(all_props, while ((dest_condition = bdd_satoneset(all_props,
atomic_propositions_set_, bddtrue)) != bddfalse) atomic_propositions_set_, bddtrue)) != bddfalse)
{ {
all_props -= dest_condition; all_props -= dest_condition;
state_ta_explicit* new_dest = new state_ta_explicit( state_ta_explicit* new_dest = new state_ta_explicit(
tgba_state->clone(), dest_condition, false, tgba_state->clone(), dest_condition, false,
tgba_->state_is_accepting(tgba_state)); tgba_->state_is_accepting(tgba_state));
state_ta_explicit* dest = ta->add_state(new_dest); state_ta_explicit* dest = ta->add_state(new_dest);
if (dest != new_dest) if (dest != new_dest)
{ {
// the state dest already exists in the testing automata // the state dest already exists in the testing automata
new_dest->get_tgba_state()->destroy(); new_dest->get_tgba_state()->destroy();
delete new_dest; delete new_dest;
} }
else else
{ {
todo.push(dest); todo.push(dest);
} }
ta->create_transition(source, bdd_setxor( ta->create_transition(source, bdd_setxor(
source->get_tgba_condition(), source->get_tgba_condition(),
dest->get_tgba_condition()), dest); dest->get_tgba_condition()), dest);
} }
} }
tgba_state->destroy(); tgba_state->destroy();
} }
delete tgba_succ_it; delete tgba_succ_it;
} }
@ -138,7 +138,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. 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 // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -158,196 +158,197 @@ namespace spot
ta::states_set_t init_states = testing_automata->get_initial_states_set(); ta::states_set_t init_states = testing_automata->get_initial_states_set();
for (it = init_states.begin(); it != init_states.end(); it++) for (it = init_states.begin(); it != init_states.end(); it++)
{ {
state* init_state = down_cast<state_ta_explicit*> (*it); state* init_state = down_cast<state_ta_explicit*> (*it);
init_set.push(init_state); init_set.push(init_state);
} }
while (!init_set.empty()) while (!init_set.empty())
{ {
// Setup depth-first search from initial states. // Setup depth-first search from initial states.
{ {
state_ta_explicit* init = state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top()); down_cast<state_ta_explicit*> (init_set.top());
init_set.pop(); init_set.pop();
state_ta_explicit* init_clone = init->clone(); state_ta_explicit* init_clone = init->clone();
numbered_state_heap::state_index_p h_init = h->find(init_clone); numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first) if (h_init.first)
continue; continue;
h->insert(init_clone, ++num); h->insert(init_clone, ++num);
sscc.push(num); sscc.push(num);
sscc.top().is_accepting sscc.top().is_accepting
= testing_automata->is_accepting_state(init); = testing_automata->is_accepting_state(init);
tgba_succ_iterator* iter = testing_automata->succ_iter(init); tgba_succ_iterator* iter = testing_automata->succ_iter(init);
iter->first(); iter->first();
todo.push(pair_state_iter(init, iter)); todo.push(pair_state_iter(init, iter));
} }
while (!todo.empty()) while (!todo.empty())
{ {
state* curr = todo.top().first; state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr->clone()); numbered_state_heap::state_index_p spi = h->find(curr->clone());
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (*spi.second == -1)
{ {
todo.pop(); todo.pop();
continue; continue;
} }
// We are looking at the next successor in SUCC. // We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second; tgba_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack. // If there is no more successor, backtrack.
if (succ->done()) if (succ->done())
{ {
// We have explored all successors of state CURR. // We have explored all successors of state CURR.
// Backtrack TODO. // Backtrack TODO.
todo.pop(); todo.pop();
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = numbered_state_heap::state_index_p spi =
h->index(curr->clone()); h->index(curr->clone());
assert(spi.first); assert(spi.first);
sscc.rem().push_front(curr); sscc.rem().push_front(curr);
// When backtracking the root of an SSCC, we must also // When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!sscc.empty()); assert(!sscc.empty());
if (sscc.top().index == *spi.second) if (sscc.top().index == *spi.second)
{ {
// removing states // removing states
std::list<state*>::iterator i; std::list<state*>::iterator i;
bool is_livelock_accepting_sscc = (sscc.top().is_accepting bool is_livelock_accepting_sscc = (sscc.top().is_accepting
&& (sscc.rem().size() > 1)); && (sscc.rem().size() > 1));
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{ {
numbered_state_heap::state_index_p spi = h->index( numbered_state_heap::state_index_p spi = h->index(
(*i)->clone()); (*i)->clone());
assert(spi.first->compare(*i) == 0); assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1); assert(*spi.second != -1);
*spi.second = -1; *spi.second = -1;
if (is_livelock_accepting_sscc) if (is_livelock_accepting_sscc)
{//if it is an accepting sscc {//if it is an accepting sscc
//add the state to G (=the livelock-accepting states set) //add the state to G (=the livelock-accepting states set)
state_ta_explicit * livelock_accepting_state = state_ta_explicit * livelock_accepting_state =
down_cast<state_ta_explicit*> (*i); down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state( livelock_accepting_state->set_livelock_accepting_state(
true); true);
} }
} }
sscc.pop(); sscc.pop();
} }
// automata reduction // automata reduction
testing_automata->delete_stuttering_and_hole_successors(curr); testing_automata->delete_stuttering_and_hole_successors(curr);
delete succ; delete succ;
// Do not delete CURR: it is a key in H. // Do not delete CURR: it is a key in H.
continue; continue;
} }
// Fetch the values destination state we are interested in... // Fetch the values destination state we are interested in...
state* dest = succ->current_state(); state* dest = succ->current_state();
// ... and point the iterator to the next successor, for // ... and point the iterator to the next successor, for
// the next iteration. // the next iteration.
succ->next(); succ->next();
// We do not need SUCC from now on. // We do not need SUCC from now on.
// Are we going to a new state through a stuttering transition? // Are we going to a new state through a stuttering transition?
bool is_stuttering_transition = bool is_stuttering_transition =
testing_automata->get_state_condition(curr) testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest); == testing_automata->get_state_condition(dest);
state* dest_clone = dest->clone(); state* dest_clone = dest->clone();
spi = h->find(dest_clone); spi = h->find(dest_clone);
// Is this a new state? // Is this a new state?
if (!spi.first) if (!spi.first)
{ {
if (!is_stuttering_transition) if (!is_stuttering_transition)
{ {
init_set.push(dest); init_set.push(dest);
dest_clone->destroy(); dest_clone->destroy();
continue; continue;
} }
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest_clone, ++num); h->insert(dest_clone, ++num);
sscc.push(num); sscc.push(num);
sscc.top().is_accepting = testing_automata->is_accepting_state( sscc.top().is_accepting = testing_automata->is_accepting_state(
dest); dest);
tgba_succ_iterator* iter = testing_automata->succ_iter(dest); tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
iter->first(); iter->first();
todo.push(pair_state_iter(dest, iter)); todo.push(pair_state_iter(dest, iter));
continue; continue;
} }
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (*spi.second == -1)
continue; continue;
if (!curr->compare(dest)) if (!curr->compare(dest))
{ {
state_ta_explicit * self_loop_state = state_ta_explicit * self_loop_state =
dynamic_cast<state_ta_explicit*> (curr); down_cast<state_ta_explicit*> (curr);
assert(self_loop_state);
if (testing_automata->is_accepting_state(self_loop_state)) if (testing_automata->is_accepting_state(self_loop_state))
self_loop_state->set_livelock_accepting_state(true); self_loop_state->set_livelock_accepting_state(true);
} }
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such // state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to // non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs // this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between // to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC. // this S1 and S2 into this SSCC.
// //
// This merge is easy to do because the order of the SSCC in // 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 // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = *spi.second; int threshold = *spi.second;
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
while (threshold < sscc.top().index) while (threshold < sscc.top().index)
{ {
assert(!sscc.empty()); assert(!sscc.empty());
acc |= sscc.top().is_accepting; acc |= sscc.top().is_accepting;
rem.splice(rem.end(), sscc.rem()); rem.splice(rem.end(), sscc.rem());
sscc.pop(); sscc.pop();
} }
// Note that we do not always have // Note that we do not always have
// threshold == sscc.top().index // threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have // after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC. // been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC. // Accumulate all acceptance conditions into the merged SSCC.
sscc.top().is_accepting |= acc; sscc.top().is_accepting |= acc;
sscc.rem().splice(sscc.rem().end(), rem); sscc.rem().splice(sscc.rem().end(), rem);
} }
} }
delete h; delete h;