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

Make it easy to filter states while iterating over an automaton.

Browse source 
* src/tgbaalgos/reachiter.hh (tgba_reachable_iterator::want_state):
New method.
* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::want_state):
Implement it.
(tgba_reachable_iterator::run): Call want_state before processing
a state.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-18 14:54:53 +01:00
parent 38148f87f8
commit ac5dda1032
3 changed files with 33 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2009-11-18 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make it easy to filter states while iterating over an automaton.
* src/tgbaalgos/reachiter.hh (tgba_reachable_iterator::want_state):
New method.
* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::want_state):
Implement it.
(tgba_reachable_iterator::run): Call want_state before processing
a state.
2009-11-17 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead * src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead

22
src/tgbaalgos/reachiter.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2009 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.
// //
@ -50,7 +50,8 @@ namespace spot
int n = 0; int n = 0;
start(); start();
state* i = automata_->get_init_state(); state* i = automata_->get_init_state();
add_state(i); if (want_state(i))
add_state(i);
seen[i] = ++n; seen[i] = ++n;
const state* t; const state* t;
while ((t = next_state())) while ((t = next_state()))
@ -63,15 +64,20 @@ namespace spot
{ {
const state* current = si->current_state(); const state* current = si->current_state();
seen_map::const_iterator s = seen.find(current); seen_map::const_iterator s = seen.find(current);
bool ws = want_state(current);
if (s == seen.end()) if (s == seen.end())
{ {
seen[current] = ++n; seen[current] = ++n;
add_state(current); if (ws)
process_link(t, tn, current, n, si); {
add_state(current);
process_link(t, tn, current, n, si);
}
} }
else else
{ {
process_link(t, tn, s->first, s->second, si); if (ws)
process_link(t, tn, s->first, s->second, si);
delete current; delete current;
} }
} }
@ -80,6 +86,12 @@ namespace spot
end(); end();
} }
bool
tgba_reachable_iterator::want_state(const state*) const
{
return true;
}
void void
tgba_reachable_iterator::start() tgba_reachable_iterator::start()
{ {

6
src/tgbaalgos/reachiter.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003, 2004, 2008, 2009 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
@ -56,6 +56,10 @@ namespace spot
virtual const state* next_state() = 0; virtual const state* next_state() = 0;
/// \} /// \}
/// Called by add_state or next_states implementations to filter
/// states. Default implementation always return true.
virtual bool want_state(const state* s) const;
/// Called by run() before starting its iteration. /// Called by run() before starting its iteration.
virtual void start(); virtual void start();
/// Called by run() once all states have been explored. /// Called by run() once all states have been explored.