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

* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check):

Browse source 
Reorganize this function so that syntactically there is only one
loop over the successors, and not two.  Call reintroduce the call
to couvreur99_check_shy::state_index(), needed by SSP, and
suppress that to index_and_insert introduced on 2004-12-29.  Also
split the "group" option in two: "group" and "group2".  "group2"
is the equivalent of the older "group", while the new "group" is
weaker and faster.
(couvreur99_check_shy::state_index): Change prototype as needed by
the algorithm.
* src/tgbaalgos/gtec/gtec.hh: Adjust.
* src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc
(index_and_insert): Remove.
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust
to new prototype.
* bench/emptchk/README, bench/emptchk/algorithms: Adjust references
to group/group2.
This commit is contained in:
Alexandre Duret-Lutz 2006-02-02 13:46:04 +00:00
parent d9d4804bc9
commit 236742aed8
8 changed files with 197 additions and 214 deletions
Download patch file Download diff file Expand all files Collapse all files

20
ChangeLog
View file

@ -1,3 +1,23 @@
2006-02-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check):
Reorganize this function so that syntactically there is only one
loop over the successors, and not two. Call reintroduce the call
to couvreur99_check_shy::state_index(), needed by SSP, and
suppress that to index_and_insert introduced on 2004-12-29. Also
split the "group" option in two: "group" and "group2". "group2"
is the equivalent of the older "group", while the new "group" is
weaker and faster.
(couvreur99_check_shy::state_index): Change prototype as needed by
the algorithm.
* src/tgbaalgos/gtec/gtec.hh: Adjust.
* src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc
(index_and_insert): Remove.
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust
to new prototype.
* bench/emptchk/README, bench/emptchk/algorithms: Adjust references
to group/group2.
2006-01-30 Alexandre Duret-Lutz <adl@src.lip6.fr>
* NEWS, configure.ac: Bump version to 0.3a.

4
bench/emptchk/README
View file

@ -194,9 +194,11 @@ This directory contains:
Cou99
Cou99(shy !group)
Cou99(shy group)
Cou99(shy group2)
> Cou99(poprem) # called `Cou99' in the paper
> Cou99(poprem shy !group) # called `Cou99 Shy-' in the paper
> Cou99(poprem shy group) # called `Cou99 Shy' in the paper
Cou99(poprem shy group)
> Cou99(poprem shy group2) # called `Cou99 Shy' in the paper
> CVWY90
> GV04
> SE05

2
bench/emptchk/algorithms
View file

@ -1,9 +1,11 @@
Cou99
Cou99(shy !group)
Cou99(shy group)
Cou99(shy group2)
Cou99(poprem)
Cou99(poprem shy !group)
Cou99(poprem shy group)
Cou99(poprem shy group2)
GV04
CVWY90
SE05

25
iface/gspn/ssp.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// 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.
//
@ -916,7 +916,7 @@ namespace spot
option_map(),
numbered_state_heap_ssp_factory_semi::instance())
{
}
}
protected:
@ -924,7 +924,7 @@ namespace spot
// children to the list of children of that older state. We cannot
// to this by sub-classing numbered_state_heap since TODO is not
// available. So we override find_state() instead.
virtual int*
virtual numbered_state_heap::state_index_p
find_state(const state* s)
{
typedef numbered_state_heap_ssp_semi::hash_type hash_type;
@ -979,11 +979,22 @@ namespace spot
}
}
}
state_index_p res;
if (i == h.end())
return 0;
if (i->first != s)
delete s;
return &i->second;
{
res.first = 0;
res.second = 0;
}
else
{
res.first = i->first;
res.second = &i->second;
if (s != i->first)
delete s;
}
return res;
}
};

318
src/tgbaalgos/gtec/gtec.cc
View file

@ -1,6 +1,6 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// 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.
//
@ -288,6 +288,20 @@ namespace spot
//////////////////////////////////////////////////////////////////////
couvreur99_check_shy::todo_item::todo_item(const state* s, int n,
couvreur99_check_shy* shy)
: s(s), n(n)
{
tgba_succ_iterator* iter = shy->ecs_->aut->succ_iter(s);
for (iter->first(); !iter->done(); iter->next(), shy->inc_transitions())
{
q.push_back(successor(iter->current_acceptance_conditions(),
iter->current_state()));
shy->inc_depth();
}
delete iter;
}
couvreur99_check_shy::couvreur99_check_shy(const tgba* a,
option_map o,
const numbered_state_heap_factory*
@ -295,11 +309,15 @@ namespace spot
: couvreur99_check(a, o, nshf), num(1)
{
group_ = o.get("group", 1);
group2_ = o.get("group2", 0);
group_ |= group2_;
// Setup depth-first search from the initial state.
todo.push_back(todo_item(0, 0));
todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state()));
inc_depth(2);
const state* i = ecs_->aut->get_init_state();
ecs_->h->insert(i, ++num);
ecs_->root.push(num);
todo.push_back(todo_item(i, num, this));
inc_depth(1);
}
couvreur99_check_shy::~couvreur99_check_shy()
@ -334,9 +352,12 @@ namespace spot
emptiness_check_result*
couvreur99_check_shy::check()
{
// Position in the loop seeking known successors.
succ_queue::iterator pos = todo.back().q.begin();
for (;;)
{
assert(ecs_->root.size() == arc.size());
assert(ecs_->root.size() == 1 + arc.size());
// Get the successors of the current state.
succ_queue& queue = todo.back().q;
@ -361,6 +382,8 @@ namespace spot
return 0;
}
pos = todo.back().q.begin();
// If poprem is used, fill rem with any component removed,
// so that remove_component() does not have to traverse
// the SCC again.
@ -386,193 +409,138 @@ namespace spot
continue;
}
// Pick one successor off the list.
successor succ = queue.front();
queue.pop_front();
dec_depth();
// We always make a first pass over the successors of a state
// to check whether it contains some state we have already seen.
// This way we hope to merge the most SCCs before stacking new
// states.
//
// So are we checking for known states ? If yes, POS tells us
// which state we are considering. Otherwise just pick the
// first one.
succ_queue::iterator old;
if (pos == queue.end())
old = queue.begin();
else
old = pos++;
successor succ = *old;
int& n = ecs_->h->index_and_insert(succ.s);
// Skip dead states.
if (n == -1)
continue;
// If it is known, it is necessarily in the current condition.
if (n != 0)
numbered_state_heap::state_index_p sip = find_state(succ.s);
int* i = sip.second;
if (!i)
{
assert(n >= ecs_->root.top().index);
ecs_->root.top().condition |= succ.acc;
// Have we found all acceptance conditions?
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = succ.s;
// We have found an accepting SCC. Clean up TODO.
clear_todo();
set_states(ecs_->states());
return new couvreur99_check_result(ecs_, options());
}
// It's a new state.
// If we are seeking known states, just skip it.
if (pos != queue.end())
continue;
// Otherwise, number it and stack it so we recurse.
queue.erase(old);
dec_depth();
ecs_->h->insert(succ.s, ++num);
ecs_->root.push(num);
arc.push(succ.acc);
todo.push_back(todo_item(succ.s, num, this));
pos = todo.back().q.begin();
inc_depth();
continue;
}
// It is a new state. Number it, and stack it.
n = ++num;
ecs_->root.push(num);
arc.push(succ.acc);
todo.push_back(todo_item(succ.s, num));
inc_depth();
succ_queue* new_queue = &todo.back().q;
tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
succ_queue::iterator merge_end;
bool merged = false;
for (iter->first(); !iter->done(); iter->next(), inc_transitions())
queue.erase(old);
dec_depth();
// Skip dead states.
if (*i == -1)
continue;
// Now this is the most interesting case. We have
// reached a state S1 which is already part of a
// non-dead SCC. Any such non-dead SCC has
// necessarily been crossed by our path to this
// state: there is a state S2 in our path which
// belongs to this SCC too. We are going to merge
// all states between this S1 and S2 into this
// SCC.
//
// This merge is easy to do because the order of
// the SCC in ROOT is ascending: we just have to
// merge all SCCs from the top of ROOT that have
// an index greater to the one of the SCC of S2
// (called the "threshold").
int threshold = *i;
std::list<const state*> rem;
bdd acc = succ.acc;
while (threshold < ecs_->root.top().index)
{
const state* dest = iter->current_state();
bdd acc = iter->current_acceptance_conditions();
numbered_state_heap::state_index_p sip = ecs_->h->find(dest);
int* i = sip.second;
// Add new states to the queue.
if (!i)
{
new_queue->push_back(successor(acc, dest));
inc_depth();
continue;
}
// Skip dead states.
if (*i == -1)
continue;
// Now this is the most interesting case. We have
// reached a state S1 which is already part of a
// non-dead SCC. Any such non-dead SCC has
// necessarily been crossed by our path to this
// state: there is a state S2 in our path which
// belongs to this SCC too. We are going to merge
// all states between this S1 and S2 into this
// SCC.
//
// This merge is easy to do because the order of
// the SCC in ROOT is ascending: we just have to
// merge all SCCs from the top of ROOT that have
// an index greater to the one of the SCC of S2
// (called the "threshold").
int threshold = *i;
std::list<const state*> rem;
while (threshold < ecs_->root.top().index)
{
assert(!ecs_->root.empty());
assert(!arc.empty());
acc |= ecs_->root.top().condition;
acc |= arc.top();
rem.splice(rem.end(), ecs_->root.rem());
ecs_->root.pop();
arc.pop();
}
// Note that we do not always have
// threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold
// might have been merged with a lower SCC.
// Accumulate all acceptance conditions into the
// merged SCC.
ecs_->root.top().condition |= acc;
ecs_->root.rem().splice(ecs_->root.rem().end(), rem);
// Have we found all acceptance conditions?
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = sip.first;
// We have found an accepting SCC. Clean up TODO.
clear_todo();
set_states(ecs_->states());
delete iter;
return new couvreur99_check_result(ecs_, options());
}
// Group the pending successors of formed SCC if requested.
if (group_)
{
assert(todo.back().s);
while (ecs_->root.top().index < todo.back().n)
{
todo_list::reverse_iterator prev = todo.rbegin();
todo_list::reverse_iterator last = prev++;
if (!merged)
{
merge_end = last->q.begin();
merged = true;
}
prev->q.splice(prev->q.end(), last->q);
if (poprem_)
{
numbered_state_heap::state_index_p spi =
ecs_->h->index(todo.back().s);
assert(spi.first);
ecs_->root.rem().push_front(spi.first);
// Don't change the stack depth, since
// we are just moving the state from TODO to REM.
}
else
{
dec_depth();
}
todo.pop_back();
}
new_queue = &todo.back().q;
}
assert(!ecs_->root.empty());
assert(!arc.empty());
acc |= ecs_->root.top().condition;
acc |= arc.top();
rem.splice(rem.end(), ecs_->root.rem());
ecs_->root.pop();
arc.pop();
}
delete iter;
if (merged)
// Note that we do not always have
// threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold
// might have been merged with a lower SCC.
// Accumulate all acceptance conditions into the
// merged SCC.
ecs_->root.top().condition |= acc;
ecs_->root.rem().splice(ecs_->root.rem().end(), rem);
// Have we found all acceptance conditions?
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
succ_queue::iterator q = new_queue->begin();
while (q != merge_end && q != new_queue->end())
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = sip.first;
// We have found an accepting SCC. Clean up TODO.
clear_todo();
set_states(ecs_->states());
return new couvreur99_check_result(ecs_, options());
}
// Group the pending successors of formed SCC if requested.
if (group_)
{
assert(todo.back().s);
while (ecs_->root.top().index < todo.back().n)
{
numbered_state_heap::state_index_p sip = ecs_->h->find(q->s);
succ_queue::iterator old = q++;
int* i = sip.second;
// Skip new states.
if (!i)
continue;
bdd acc = old->acc;
// Delete other states.
new_queue->erase(old);
dec_depth();
// Delete dead states.
if (*i == -1)
continue;
todo_list::reverse_iterator prev = todo.rbegin();
todo_list::reverse_iterator last = prev++;
// If group2 is used we insert the last->q in front
// of prev->q so that the states in prev->q are checked
// for existence again after we have done with the states
// of last->q. Otherwise we just append to the end.
prev->q.splice(group2_ ? prev->q.begin() : prev->q.end(),
last->q);
// Merge existing states.
assert(n >= ecs_->root.top().index);
ecs_->root.top().condition |= acc;
// Have we found all acceptance conditions?
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
if (poprem_)
{
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = sip.first;
// We have found an accepting SCC. Clean up TODO.
clear_todo();
set_states(ecs_->states());
return new couvreur99_check_result(ecs_, options());
numbered_state_heap::state_index_p spi =
ecs_->h->index(todo.back().s);
assert(spi.first);
ecs_->root.rem().push_front(spi.first);
// Don't change the stack depth, since
// we are just moving the state from TODO to REM.
}
else
{
dec_depth();
}
todo.pop_back();
}
pos = todo.back().q.begin();
}
}
}
int*
numbered_state_heap::state_index_p
couvreur99_check_shy::find_state(const state* s)
{
return ecs_->h->find(s).second;
return ecs_->h->find(s);
}
emptiness_check*

18
src/tgbaalgos/gtec/gtec.hh
View file

@ -1,6 +1,6 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// 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.
//
@ -222,11 +222,8 @@ namespace spot
{
const state* s;
int n;
succ_queue q;
todo_item(const state* s, int n)
: s(s), n(n)
{
}
succ_queue q; // Unprocessed successors of S
todo_item(const state* s, int n, couvreur99_check_shy* shy);
};
typedef std::list<todo_item> todo_list;
@ -237,6 +234,9 @@ namespace spot
// Whether successors should be grouped for states in the same
// SCC.
bool group_;
// If the "group2" option is set (it implies "group"), we
// reprocess the successor states of SCC that have been merged.
bool group2_;
/// \brief find the SCC number of a unprocessed state.
///
@ -246,7 +246,7 @@ namespace spot
/// to TODO during this step. (Because TODO must be known,
/// sub-classing spot::numbered_state_heap is not enough.) Then
/// overriding this method is the way to go.
virtual int* find_state(const state* s);
virtual numbered_state_heap::state_index_p find_state(const state* s);
};

15
src/tgbaalgos/gtec/nsheap.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -150,19 +150,6 @@ namespace spot
h[s] = index;
}
int&
numbered_state_heap_hash_map::index_and_insert(const state*& s)
{
std::pair<hash_type::iterator, bool> r
= h.insert(hash_type::value_type(s, 0));
if (!r.second)
{
delete s;
s = r.first->first;
}
return r.first->second;
}
int
numbered_state_heap_hash_map::size() const
{

9
src/tgbaalgos/gtec/nsheap.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -89,12 +89,6 @@ namespace spot
/// Add a new state \a s with index \a index
virtual void insert(const state* s, int index) = 0;
/// \brief Get the index of a state, and insert that state if it is missing.
///
/// If a clone of \a s is already in the hash table, \a s will be deleted
/// and replaced by the address of the clone used.
virtual int& index_and_insert(const state*& s) = 0;
/// The number of stored states.
virtual int size() const = 0;
@ -120,7 +114,6 @@ namespace spot
virtual state_index_p find(const state* s);
virtual state_index index(const state* s) const;
virtual state_index_p index(const state* s);
virtual int& index_and_insert(const state*& s);
virtual void insert(const state* s, int index);
virtual int size() const;