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

* src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call

Browse source 
erase() after splice(), splice() already removes the elements.
This commit is contained in:
Alexandre Duret-Lutz 2005-01-03 12:11:28 +00:00
parent 000c041a95
commit 13183893dd
2 changed files with 284 additions and 284 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,5 +1,8 @@
2005-01-03 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-01-03 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call
erase() after splice(), splice() already removes the elements.
* src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh, * src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh,
src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh, src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh,
src/misc/bareword.hh, src/tgba/succiter.hh, src/misc/bareword.hh, src/tgba/succiter.hh,
@ -46,7 +49,7 @@
2004-12-16 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-12-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/reducerun.cc (reduce_run): Do not call erase() after * src/tgbaalgos/reducerun.cc (reduce_run): Do not call erase() after
splice(), splice() already remove the elements. splice(), splice() already removes the elements.
* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run):
Likewise. Likewise.

563
src/tgbaalgos/ndfs_result.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -61,7 +61,7 @@ namespace spot
typedef std::list<stack_item> stack_type; typedef std::list<stack_item> stack_type;
template < typename ndfs_search, typename heap > template <typename ndfs_search, typename heap>
class ndfs_result : public emptiness_check_result class ndfs_result : public emptiness_check_result
{ {
public: public:
@ -161,7 +161,7 @@ namespace spot
{ {
bool b = dfs(start, acc_trans, covered_acc); bool b = dfs(start, acc_trans, covered_acc);
assert(b); assert(b);
(void)b; (void) b;
} }
delete start; delete start;
@ -177,8 +177,7 @@ namespace spot
construct_prefix(run); construct_prefix(run);
for (typename accepting_transitions_list::const_iterator i = for (typename accepting_transitions_list::const_iterator i =
acc_trans.begin(); acc_trans.begin(); i != acc_trans.end(); ++i)
i != acc_trans.end(); ++i)
{ {
delete i->source; delete i->source;
delete i->dest; delete i->dest;
@ -203,146 +202,146 @@ namespace spot
state_ptr_hash, state_ptr_equal> state_set; state_ptr_hash, state_ptr_equal> state_set;
void clean(stack_type& st1, state_set& seen, state_set& dead) void clean(stack_type& st1, state_set& seen, state_set& dead)
{ {
while (!st1.empty()) while (!st1.empty())
{ {
delete st1.front().it; delete st1.front().it;
st1.pop_front(); st1.pop_front();
} }
for (state_set::iterator i = seen.begin(); i != seen.end();) for (state_set::iterator i = seen.begin(); i != seen.end();)
{ {
const state* s = *i; const state* s = *i;
++i; ++i;
delete s; delete s;
} }
for (state_set::iterator i = dead.begin(); i != dead.end();) for (state_set::iterator i = dead.begin(); i != dead.end();)
{ {
const state* s = *i; const state* s = *i;
++i; ++i;
delete s; delete s;
} }
} }
bool dfs(const state* target, accepting_transitions_list& acc_trans, bool dfs(const state* target, accepting_transitions_list& acc_trans,
bdd& covered_acc) bdd& covered_acc)
{ {
assert(h_.has_been_visited(target)); assert(h_.has_been_visited(target));
stack_type st1; stack_type st1;
state_set seen, dead; state_set seen, dead;
const state* start = target->clone(); const state* start = target->clone();
seen.insert(start); seen.insert(start);
tgba_succ_iterator* i = a_->succ_iter(start); tgba_succ_iterator* i = a_->succ_iter(start);
i->first(); i->first();
st1.push_front(stack_item(start, i, bddfalse, bddfalse)); st1.push_front(stack_item(start, i, bddfalse, bddfalse));
while (!st1.empty()) while (!st1.empty())
{ {
stack_item& f = st1.front(); stack_item& f = st1.front();
ndfsr_trace << "DFS1 treats: " << a_->format_state(f.s) ndfsr_trace << "DFS1 treats: " << a_->format_state(f.s)
<< std::endl; << std::endl;
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
ndfsr_trace << " Visit the successor: " ndfsr_trace << " Visit the successor: "
<< a_->format_state(s_prime) << std::endl; << a_->format_state(s_prime) << std::endl;
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
f.it->next(); f.it->next();
if (h_.has_been_visited(s_prime)) if (h_.has_been_visited(s_prime))
{ {
if (dead.find(s_prime) != dead.end()) if (dead.find(s_prime) != dead.end())
{ {
ndfsr_trace << " it is dead, pop it" << std::endl; ndfsr_trace << " it is dead, pop it" << std::endl;
delete s_prime; delete s_prime;
} }
else if (seen.find(s_prime) == seen.end()) else if (seen.find(s_prime) == seen.end())
{ {
ndfsr_trace << " it is not seen, go down" << std::endl; ndfsr_trace << " it is not seen, go down" << std::endl;
seen.insert(s_prime); seen.insert(s_prime);
tgba_succ_iterator* i = a_->succ_iter(s_prime); tgba_succ_iterator* i = a_->succ_iter(s_prime);
i->first(); i->first();
st1.push_front(stack_item(s_prime, i, label, acc)); st1.push_front(stack_item(s_prime, i, label, acc));
} }
else if ((acc & covered_acc) != acc) else if ((acc & covered_acc) != acc)
{ {
ndfsr_trace << " a propagation is needed, " ndfsr_trace << " a propagation is needed, "
<< "start a search" << std::endl; << "start a search" << std::endl;
if (search(s_prime, target, dead)) if (search(s_prime, target, dead))
{ {
transition t = { f.s->clone(), label, acc, transition t = { f.s->clone(), label, acc,
s_prime->clone() }; s_prime->clone() };
assert(h_.has_been_visited(t.source)); assert(h_.has_been_visited(t.source));
assert(h_.has_been_visited(t.dest)); assert(h_.has_been_visited(t.dest));
acc_trans.push_back(t); acc_trans.push_back(t);
covered_acc |= acc; covered_acc |= acc;
if (covered_acc == a_->all_acceptance_conditions()) if (covered_acc == a_->all_acceptance_conditions())
{ {
clean(st1, seen, dead); clean(st1, seen, dead);
delete s_prime; delete s_prime;
return true; return true;
} }
} }
delete s_prime; delete s_prime;
} }
else else
{ {
ndfsr_trace << " already seen, pop it" << std::endl; ndfsr_trace << " already seen, pop it" << std::endl;
delete s_prime; delete s_prime;
} }
} }
else else
{ {
ndfsr_trace << " not seen during the search, pop it" ndfsr_trace << " not seen during the search, pop it"
<< std::endl; << std::endl;
delete s_prime; delete s_prime;
} }
} }
else else
{ {
ndfsr_trace << " all the successors have been visited" ndfsr_trace << " all the successors have been visited"
<< std::endl; << std::endl;
stack_item f_dest(f); stack_item f_dest(f);
delete st1.front().it; delete st1.front().it;
st1.pop_front(); st1.pop_front();
if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc)
{ {
ndfsr_trace << " a propagation is needed, start a search" ndfsr_trace << " a propagation is needed, start a search"
<< std::endl; << std::endl;
if (search(f_dest.s, target, dead)) if (search(f_dest.s, target, dead))
{ {
transition t = { st1.front().s->clone(), transition t = { st1.front().s->clone(),
f_dest.label, f_dest.acc, f_dest.label, f_dest.acc,
f_dest.s->clone() }; f_dest.s->clone() };
assert(h_.has_been_visited(t.source)); assert(h_.has_been_visited(t.source));
assert(h_.has_been_visited(t.dest)); assert(h_.has_been_visited(t.dest));
acc_trans.push_back(t); acc_trans.push_back(t);
covered_acc |= f_dest.acc; covered_acc |= f_dest.acc;
if (covered_acc == a_->all_acceptance_conditions()) if (covered_acc == a_->all_acceptance_conditions())
{ {
clean(st1, seen, dead); clean(st1, seen, dead);
return true; return true;
} }
} }
} }
else else
{ {
ndfsr_trace << " no propagation needed, pop it" ndfsr_trace << " no propagation needed, pop it"
<< std::endl; << std::endl;
} }
} }
} }
clean(st1, seen, dead); clean(st1, seen, dead);
return false; return false;
} }
class test_path: public bfs_steps class test_path: public bfs_steps
{ {
public: public:
test_path(const tgba* a, const state* t, test_path(const tgba* a, const state* t,
const state_set& d, const heap& h) const state_set& d, const heap& h)
: bfs_steps(a), target(t), dead(d), h(h) : bfs_steps(a), target(t), dead(d), h(h)
{ {
} }
@ -369,8 +368,9 @@ namespace spot
const state* filter(const state* s) const state* filter(const state* s)
{ {
if (!h.has_been_visited(s) || seen.find(s) != seen.end() || if (!h.has_been_visited(s)
dead.find(s) != dead.end()) || seen.find(s) != seen.end()
|| dead.find(s) != dead.end())
{ {
delete s; delete s;
return 0; return 0;
@ -379,9 +379,9 @@ namespace spot
return s; return s;
} }
void finalize( void finalize(const std::map<const state*, tgba_run::step,
const std::map<const state*, tgba_run::step, state_ptr_less_than>&, state_ptr_less_than>&,
const tgba_run::step&, const state*, tgba_run::steps&) const tgba_run::step&, const state*, tgba_run::steps&)
{ {
} }
@ -403,29 +403,29 @@ namespace spot
}; };
bool search(const state* start, const state* target, state_set& dead) bool search(const state* start, const state* target, state_set& dead)
{ {
tgba_run::steps path; tgba_run::steps path;
if (start->compare(target) == 0) if (start->compare(target) == 0)
return true; return true;
test_path s(a_, target, dead, h_); test_path s(a_, target, dead, h_);
const state* res = s.search(start->clone(), path); const state* res = s.search(start->clone(), path);
if (res) if (res)
{ {
assert(res->compare(target) == 0); assert(res->compare(target) == 0);
return true; return true;
} }
else else
{ {
state_set::const_iterator it; state_set::const_iterator it;
for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it) for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it)
dead.insert((*it)->clone()); dead.insert((*it)->clone());
return false; return false;
} }
} }
typedef Sgi::hash_multimap<const state*, transition, typedef Sgi::hash_multimap<const state*, transition,
state_ptr_hash, state_ptr_equal> m_source_trans; state_ptr_hash, state_ptr_equal> m_source_trans;
class min_path: public bfs_steps class min_path: public bfs_steps
{ {
@ -486,140 +486,137 @@ namespace spot
}; };
void construct_cycle(tgba_run* run, void construct_cycle(tgba_run* run,
const accepting_transitions_list& acc_trans) const accepting_transitions_list& acc_trans)
{ {
assert(!acc_trans.empty()); assert(!acc_trans.empty());
transition current = acc_trans.front(); transition current = acc_trans.front();
// insert the first accepting transition in the cycle // insert the first accepting transition in the cycle
ndfsr_trace << "the initial accepting transition is from " ndfsr_trace << "the initial accepting transition is from "
<< a_->format_state(current.source) << " to " << a_->format_state(current.source) << " to "
<< a_->format_state(current.dest) << std::endl; << a_->format_state(current.dest) << std::endl;
const state* begin = current.source; const state* begin = current.source;
m_source_trans target; m_source_trans target;
typename accepting_transitions_list::const_iterator i = typename accepting_transitions_list::const_iterator i =
acc_trans.begin(); acc_trans.begin();
ndfsr_trace << "targets are the source states: "; ndfsr_trace << "targets are the source states: ";
for (++i; i!=acc_trans.end(); ++i) for (++i; i != acc_trans.end(); ++i)
{ {
if (i->source->compare(begin) == 0 && if (i->source->compare(begin) == 0 &&
i->source->compare(i->dest) == 0) i->source->compare(i->dest) == 0)
{ {
ndfsr_trace << "(self loop " << a_->format_state(i->source) ndfsr_trace << "(self loop " << a_->format_state(i->source)
<< " -> " << a_->format_state(i->dest) << " -> " << a_->format_state(i->dest)
<< " ignored) "; << " ignored) ";
tgba_run::step st = { i->source->clone(), i->label, i->acc }; tgba_run::step st = { i->source->clone(), i->label, i->acc };
run->cycle.push_back(st); run->cycle.push_back(st);
} }
else else
{ {
ndfsr_trace << a_->format_state(i->source) << " (-> " ndfsr_trace << a_->format_state(i->source) << " (-> "
<< a_->format_state(i->dest) << ") "; << a_->format_state(i->dest) << ") ";
target.insert(std::make_pair(i->source, *i)); target.insert(std::make_pair(i->source, *i));
} }
} }
ndfsr_trace << std::endl; ndfsr_trace << std::endl;
tgba_run::step st = { current.source->clone(), current.label, tgba_run::step st = { current.source->clone(), current.label,
current.acc }; current.acc };
run->cycle.push_back(st); run->cycle.push_back(st);
while (!target.empty()) while (!target.empty())
{ {
// find a minimal path from current.dest to any source state in // find a minimal path from current.dest to any source state in
// target. // target.
ndfsr_trace << "looking for a path from " ndfsr_trace << "looking for a path from "
<< a_->format_state(current.dest) << std::endl; << a_->format_state(current.dest) << std::endl;
typename m_source_trans::iterator i = target.find(current.dest); typename m_source_trans::iterator i = target.find(current.dest);
if (i == target.end()) if (i == target.end())
{ {
min_path s(a_, target, h_); min_path s(a_, target, h_);
const state* res = s.search(current.dest->clone(), run->cycle); const state* res = s.search(current.dest->clone(), run->cycle);
// init current to the corresponding transition. // init current to the corresponding transition.
assert(res); assert(res);
ndfsr_trace << a_->format_state(res) << " reached" << std::endl; ndfsr_trace << a_->format_state(res) << " reached" << std::endl;
i = target.find(res); i = target.find(res);
assert(i != target.end()); assert(i != target.end());
} }
else else
{ {
ndfsr_trace << "this is a target" << std::endl; ndfsr_trace << "this is a target" << std::endl;
} }
current = i->second; current = i->second;
// complete the path with the corresponding transition // complete the path with the corresponding transition
tgba_run::step st = { current.source->clone(), current.label, tgba_run::step st = { current.source->clone(), current.label,
current.acc }; current.acc };
run->cycle.push_back(st); run->cycle.push_back(st);
// remove this source state of target // remove this source state of target
target.erase(i); target.erase(i);
} }
if (current.dest->compare(begin) != 0) if (current.dest->compare(begin) != 0)
{ {
// close the cycle by adding a path from the destination of the // close the cycle by adding a path from the destination of the
// last inserted transition to the source of the first one // last inserted transition to the source of the first one
ndfsr_trace << std::endl << "looking for a path from " ndfsr_trace << std::endl << "looking for a path from "
<< a_->format_state(current.dest) << " to " << a_->format_state(current.dest) << " to "
<< a_->format_state(begin) << std::endl; << a_->format_state(begin) << std::endl;
transition tmp; transition tmp;
target.insert(std::make_pair(begin, tmp)); target.insert(std::make_pair(begin, tmp));
min_path s(a_, target, h_); min_path s(a_, target, h_);
const state* res = s.search(current.dest->clone(), run->cycle); const state* res = s.search(current.dest->clone(), run->cycle);
assert(res); assert(res);
assert(res->compare(begin) == 0); assert(res->compare(begin) == 0);
(void)res; (void)res;
} }
} }
void construct_prefix(tgba_run* run) void construct_prefix(tgba_run* run)
{ {
m_source_trans target; m_source_trans target;
transition tmp; transition tmp;
// Register all states from the cycle as target of the BFS.
for (tgba_run::steps::const_iterator i = run->cycle.begin();
i != run->cycle.end(); ++i)
target.insert(std::make_pair(i->s, tmp));
// Register all states from the cycle as target of the BFS. const state* prefix_start = a_->get_init_state();
for (tgba_run::steps::const_iterator i = run->cycle.begin(); // There are two cases: either the initial state is already on
i != run->cycle.end(); ++i) // the cycle, or it is not. If it is, we will have to rotate
target.insert(std::make_pair(i->s, tmp)); // the cycle so it begins on this position. Otherwise we will shift
// the cycle so it begins on the state that follows the prefix.
// cycle_entry_point is that state.
const state* cycle_entry_point;
typename m_source_trans::const_iterator ps = target.find(prefix_start);
if (ps != target.end())
{
// The initial state is on the cycle.
delete prefix_start;
cycle_entry_point = ps->first->clone();
}
else
{
// This initial state is outside the cycle. Compute the prefix.
min_path s(a_, target, h_);
cycle_entry_point = s.search(prefix_start, run->prefix);
assert(cycle_entry_point);
cycle_entry_point = cycle_entry_point->clone();
}
const state* prefix_start = a_->get_init_state(); // Locate cycle_entry_point on the cycle.
// There are two cases: either the initial state is already on tgba_run::steps::iterator cycle_ep_it;
// the cycle, or it is not. If it is, we will have to rotate for (cycle_ep_it = run->cycle.begin();
// the cycle so it begins on this position. Otherwise we will shift cycle_ep_it != run->cycle.end()
// the cycle so it begins on the state that follows the prefix. && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
// cycle_entry_point is that state. continue;
const state* cycle_entry_point; assert(cycle_ep_it != run->cycle.end());
typename m_source_trans::const_iterator ps = target.find(prefix_start); delete cycle_entry_point;
if (ps != target.end())
{
// The initial state is on the cycle.
delete prefix_start;
cycle_entry_point = ps->first->clone();
}
else
{
// This initial state is outside the cycle. Compute the prefix.
min_path s(a_, target, h_);
cycle_entry_point = s.search(prefix_start, run->prefix);
assert(cycle_entry_point);
cycle_entry_point = cycle_entry_point->clone();
}
// Locate cycle_entry_point on the cycle.
tgba_run::steps::iterator cycle_ep_it;
for (cycle_ep_it = run->cycle.begin();
cycle_ep_it != run->cycle.end()
&& cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
continue;
assert(cycle_ep_it != run->cycle.end());
delete cycle_entry_point;
// Now shift the cycle so it starts on cycle_entry_point.
run->cycle.splice(run->cycle.end(), run->cycle,
run->cycle.begin(), cycle_ep_it);
run->cycle.erase(run->cycle.begin(), cycle_ep_it);
}
// Now shift the cycle so it starts on cycle_entry_point.
run->cycle.splice(run->cycle.end(), run->cycle,
run->cycle.begin(), cycle_ep_it);
}
}; };
} }