* src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add
comments. * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise. Soheib and I had a hard time figuring why we did this...
This commit is contained in:
parent
f1c3af808f
commit
478844dad8
3 changed files with 20 additions and 0 deletions
|
|
@ -1,3 +1,10 @@
|
||||||
|
2004-07-07 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add
|
||||||
|
comments.
|
||||||
|
* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise.
|
||||||
|
Soheib and I had a hard time figuring why we did this...
|
||||||
|
|
||||||
2004-07-02 Thomas Martinez <martinez@src.lip6.fr>
|
2004-07-02 Thomas Martinez <martinez@src.lip6.fr>
|
||||||
|
|
||||||
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
|
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
|
||||||
|
|
|
||||||
|
|
@ -909,6 +909,11 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
|
|
||||||
|
// If a new state includes an older state, we may have to add new
|
||||||
|
// 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 int*
|
||||||
find_state(const state* s)
|
find_state(const state* s)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -135,6 +135,14 @@ namespace spot
|
||||||
typedef std::pair<const state*, succ_queue> pair_state_successors;
|
typedef std::pair<const state*, succ_queue> pair_state_successors;
|
||||||
std::stack<pair_state_successors> todo;
|
std::stack<pair_state_successors> todo;
|
||||||
|
|
||||||
|
/// \brief find the SCC number of a unprocessed state.
|
||||||
|
///
|
||||||
|
/// Sometimes we want to modify some of the above structures when
|
||||||
|
/// looking up a new state. This happens for instance when find()
|
||||||
|
/// must perform inclusion checking and add new states to process
|
||||||
|
/// 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 int* find_state(const state* s);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue