diff --git a/ChangeLog b/ChangeLog index 06f38ca50..8b993e10f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2004-04-13 Alexandre Duret-Lutz + + * src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted + from ... + (emptiness_check): ... here. + (emptiness_check::root): Redefined as a scc_stack object. + * src/tgbaalgos/emptinesscheck.cc: Adjust. + 2004-04-05 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index eb9a47913..fc2233296 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -29,14 +29,45 @@ namespace spot { - typedef std::pair pair_state_iter; - emptiness_check::connected_component::connected_component(int i) + scc_stack::connected_component::connected_component(int i) { index = i; condition = bddfalse; } + scc_stack::connected_component& + scc_stack::top() + { + return s.top(); + } + + void + scc_stack::pop() + { + s.pop(); + } + + void + scc_stack::push(int index) + { + s.push(connected_component(index)); + } + + size_t + scc_stack::size() const + { + return s.size(); + } + + bool + scc_stack::empty() const + { + return s.empty(); + } + + typedef std::pair pair_state_iter; + bool emptiness_check::connected_component_set::has_state(const state* s) const { @@ -136,7 +167,7 @@ namespace spot { state* init = aut_->get_init_state(); h[init] = 1; - root.push(connected_component(1)); + root.push(1); arc.push(bddfalse); tgba_succ_iterator* iter = aut_->succ_iter(init); iter->first(); @@ -195,7 +226,7 @@ namespace spot // Yes. Number it, stack it, and register its successors // for later processing. h[dest] = ++num; - root.push(connected_component(num)); + root.push(num); arc.push(acc); tgba_succ_iterator* iter = aut_->succ_iter(dest); iter->first(); @@ -411,7 +442,7 @@ namespace spot successor succ = queue.front(); queue.pop_front(); h[succ.s] = ++num; - root.push(connected_component(num)); + root.push(num); arc.push(succ.acc); todo.push(pair_state_successors(succ.s, succ_queue())); succ_queue& new_queue = todo.top().second; diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 8b612b34b..e7a943113 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -32,6 +32,30 @@ namespace spot { + class scc_stack + { + public: + struct connected_component + { + // During the Depth path we keep the connected component that we met. + public: + connected_component(int index = -1); + + int index; + /// The bdd condition is the union of all acceptance conditions of + /// transitions which connect the states of the connected component. + bdd condition; + }; + + connected_component& top(); + void pop(); + void push(int index); + size_t size() const; + bool empty() const; + + std::stack s; + }; + /// \brief Check whether the language of an automate is empty. /// /// This is based on the following paper. @@ -100,19 +124,7 @@ namespace spot private: - struct connected_component - { - // During the Depth path we keep the connected component that we met. - public: - connected_component(int index = -1); - - int index; - /// The bdd condition is the union of all acceptance conditions of - /// transitions which connect the states of the connected component. - bdd condition; - }; - - struct connected_component_set: public connected_component + struct connected_component_set: public scc_stack::connected_component { typedef Sgi::hash_set set_type; @@ -125,7 +137,7 @@ namespace spot }; const tgba* aut_; - std::stack root; + scc_stack root; state_sequence suffix; cycle_path period;