diff --git a/ChangeLog b/ChangeLog index 9188ddca4..b5468de3f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2004-07-07 Alexandre Duret-Lutz + + * 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 * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 81d820916..5b6a950bd 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -909,6 +909,11 @@ namespace spot } 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* find_state(const state* s) { diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 22dbfec8e..032186c8b 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -135,6 +135,14 @@ namespace spot typedef std::pair pair_state_successors; std::stack 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); };