diff --git a/ChangeLog b/ChangeLog index 4d94a2311..82571cbbb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,8 +1,28 @@ +2004-04-14 Alexandre Duret-Lutz + + * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: + Delete and split into ... + * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, + src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh, + src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, + src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh, + src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh, + src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ... + these new files. + * src/tgbaalgos/gtec/Makefile.am: New file. + * src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD): + Recurse into gtec and link gtec/libgtec.la. + (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh + and emptinesscheck.cc. + * configure.ac: Output src/tgbalagos/gtec/Makefile. + * iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes. + * README: Update tree description. + 2004-04-13 Alexandre Duret-Lutz - * tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator, + * src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator, numbered_state_heap, numbered_state_heap_hash_map): New classes. - * tgbaalgos/emptinesscheck.cc + * src/tgbaalgos/emptinesscheck.cc (numbered_state_heap_hash_map_const_iterator): New class. (numbered_state_heap_hash_map): Implement it. diff --git a/README b/README index 0b9b995b1..fd0cff4e2 100644 --- a/README +++ b/README @@ -65,6 +65,7 @@ src/ Sources for libspot. misc/ Miscellaneous support files. tgba/ TGBA objects and cousins. tgbaalgos/ Algorithms on TGBAs. + gtec/ Generalized Tarjan Emptiness-Check. tgbaparse/ Parser for explicit TGBAs. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. doc/ Documentation for libspot. diff --git a/configure.ac b/configure.ac index 85cfdeca7..b60594ed0 100644 --- a/configure.ac +++ b/configure.ac @@ -64,6 +64,7 @@ AC_CONFIG_FILES([ src/ltlvisit/Makefile src/tgba/Makefile src/tgbaalgos/Makefile + src/tgbaalgos/gtec/Makefile src/tgbaparse/Makefile src/tgbatest/Makefile src/tgbatest/defs diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index d55e6f7b4..400f2b52f 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -35,7 +35,8 @@ #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/magic.hh" -#include "tgbaalgos/emptinesscheck.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/gtec/ce.hh" void diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 282ed7de3..8c9bfcb13 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -19,6 +19,8 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. +SUBDIRS = gtec + AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) @@ -27,7 +29,6 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ dotty.hh \ dupexp.hh \ - emptinesscheck.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ @@ -41,7 +42,6 @@ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ dotty.cc \ dupexp.cc \ - emptinesscheck.cc \ lbtt.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ @@ -50,3 +50,5 @@ libtgbaalgos_la_SOURCES = \ reachiter.cc \ save.cc \ stats.cc + +libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc deleted file mode 100644 index 28d4f3a71..000000000 --- a/src/tgbaalgos/emptinesscheck.cc +++ /dev/null @@ -1,1042 +0,0 @@ -// Copyright (C) 2003, 2004 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. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "emptinesscheck.hh" -#include "tgba/bddprint.hh" -#include -#include -#include -#include -#include - -namespace spot -{ - - 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(); - } - - ////////////////////////////////////////////////////////////////////// - - emptiness_check_status::emptiness_check_status(const tgba* aut) - : aut(aut) - { - } - - emptiness_check_status::~emptiness_check_status() - { - } - - void - emptiness_check_status::print_stats(std::ostream& os) const - { - os << h.size() << " unique states visited" << std::endl; - os << root.size() - << " strongly connected components in search stack" - << std::endl; - } - - - ////////////////////////////////////////////////////////////////////// - - class numbered_state_heap_hash_map_const_iterator : - public numbered_state_heap_const_iterator - { - public: - numbered_state_heap_hash_map_const_iterator - (const numbered_state_heap_hash_map::hash_type& h) - : numbered_state_heap_const_iterator(), h(h) - { - } - - ~numbered_state_heap_hash_map_const_iterator() - { - } - - virtual void - first() - { - i = h.begin(); - } - - virtual void - next() - { - ++i; - } - - virtual bool - done() const - { - return i == h.end(); - } - - virtual const state* - get_state() const - { - return i->first; - } - - virtual int - get_index() const - { - return i->second; - } - - private: - numbered_state_heap_hash_map::hash_type::const_iterator i; - const numbered_state_heap_hash_map::hash_type& h; - }; - - numbered_state_heap_hash_map::~numbered_state_heap_hash_map() - { - // Free keys in H. - hash_type::iterator i = h.begin(); - while (i != h.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - delete s; - } - } - - const int* - numbered_state_heap_hash_map::find(const state* s) const - { - hash_type::const_iterator i = h.find(s); - if (i == h.end()) - return 0; - return &i->second; - } - - int* - numbered_state_heap_hash_map::find(const state* s) - { - hash_type::iterator i = h.find(s); - if (i == h.end()) - return 0; - return &i->second; - } - - void - numbered_state_heap_hash_map::insert(const state* s, int index) - { - h[s] = index; - } - - int - numbered_state_heap_hash_map::size() const - { - return h.size(); - } - - numbered_state_heap_const_iterator* - numbered_state_heap_hash_map::iterator() const - { - return new numbered_state_heap_hash_map_const_iterator(h); - } - - const state* - numbered_state_heap_hash_map::filter(const state* s) const - { - hash_type::const_iterator i = h.find(s); - assert(i != h.end()); - if (s != i->first) - delete s; - return i->first; - } - - - - ////////////////////////////////////////////////////////////////////// - - typedef std::pair pair_state_iter; - - - emptiness_check::emptiness_check(const tgba* a) - { - ecs_ = new emptiness_check_status(a); - } - - emptiness_check::~emptiness_check() - { - delete ecs_; - } - - void - emptiness_check::remove_component(const state* from) - { - // Remove from H all states which are reachable from state FROM. - - // Stack of iterators towards states to remove. - std::stack to_remove; - - // Remove FROM itself, and prepare to remove its successors. - // (FROM should be in H, otherwise it means all reachable - // states from FROM have already been removed and there is no - // point in calling remove_component.) - int* hi = ecs_->h.find(from); - assert(hi); - assert(*hi != -1); - *hi = -1; - tgba_succ_iterator* i = ecs_->aut->succ_iter(from); - - for (;;) - { - // Remove each destination of this iterator. - for (i->first(); !i->done(); i->next()) - { - state* s = i->current_state(); - int *hi = ecs_->h.find(s); - assert(hi); - - if (*hi != -1) - { - *hi = -1; - to_remove.push(ecs_->aut->succ_iter(s)); - } - delete s; - } - delete i; - if (to_remove.empty()) - break; - i = to_remove.top(); - to_remove.pop(); - } - } - - bool - emptiness_check::check() - { - // We use five main data in this algorithm: - // * emptiness_check::root, a stack of strongly connected components (SCC), - // * emptiness_check::h, a hash of all visited nodes, with their order, - // (it is called "Hash" in Couvreur's paper) - // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; - // * num, the number of visited nodes. Used to set the order of each - // visited node, - int num = 1; - // * todo, the depth-first search stack. This holds pairs of the - // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator - // over the successors of STATE. In our use, ITERATOR should - // always be freed when TODO is popped, but STATE should not because - // it is also used as a key in H. - std::stack todo; - - // Setup depth-first search from the initial state. - { - state* init = ecs_->aut->get_init_state(); - ecs_->h.insert(init, 1); - ecs_->root.push(1); - arc.push(bddfalse); - tgba_succ_iterator* iter = ecs_->aut->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - } - - while (!todo.empty()) - { - assert(ecs_->root.size() == arc.size()); - - // We are looking at the next successor in SUCC. - tgba_succ_iterator* succ = todo.top().second; - - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. - const state* curr = todo.top().first; - - // Backtrack TODO. - todo.pop(); - - // When backtracking the root of an SCC, we must also - // remove that SCC from the ARC/ROOT stacks. We must - // discard from H all reachable states from this SCC. - int* i = ecs_->h.find(curr); - assert(i); - assert(!ecs_->root.empty()); - if (ecs_->root.top().index == *i) - { - assert(!arc.empty()); - arc.pop(); - ecs_->root.pop(); - remove_component(curr); - } - - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } - - // We have a successor to look at. Fetch the values - // (destination state, acceptance conditions of the arc) - // we are interested in... - const state* dest = succ->current_state(); - bdd acc = succ->current_acceptance_conditions(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. - - // Are we going to a new state? - int* i = ecs_->h.find(dest); - if (!i) - { - // Yes. Number it, stack it, and register its successors - // for later processing. - ecs_->h.insert(dest, ++num); - ecs_->root.push(num); - arc.push(acc); - tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - continue; - } - - // We know the state exists. Since a state can have several - // representations (i.e., objects), make sure we delete - // anything but the first one seen (the one used as key in H). - (void) ecs_->h.filter(dest); - - // If we have reached a dead component, ignore it. - 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; - while (threshold < ecs_->root.top().index) - { - assert(!ecs_->root.empty()); - assert(!arc.empty()); - acc |= ecs_->root.top().condition; - acc |= arc.top(); - 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; - - if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions()) - { - // We have found an accepting SCC. - // Release all iterators in TODO. - while (!todo.empty()) - { - delete todo.top().second; - todo.pop(); - } - return false; - } - } - // This automaton recognizes no word. - return true; - } - - const emptiness_check_status* - emptiness_check::result() const - { - return ecs_; - } - - ////////////////////////////////////////////////////////////////////// - - emptiness_check_shy::emptiness_check_shy(const tgba* a) - : emptiness_check(a) - { - } - - emptiness_check_shy::~emptiness_check_shy() - { - } - - struct successor { - bdd acc; - const spot::state* s; - successor(bdd acc, const spot::state* s): acc(acc), s(s) {} - }; - - bool - emptiness_check_shy::check() - { - // We use five main data in this algorithm: - // * emptiness_check::root, a stack of strongly connected components (SCC), - // * emptiness_check::h, a hash of all visited nodes, with their order, - // (it is called "Hash" in Couvreur's paper) - // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; - // * num, the number of visited nodes. Used to set the order of each - // visited node, - int num = 1; - // * todo, the depth-first search stack. This holds pairs of the - // form (STATE, SUCCESSORS) where SUCCESSORS is a list of - // (ACCEPTANCE_CONDITIONS, STATE) pairs. - typedef std::list succ_queue; - typedef std::pair pair_state_successors; - std::stack todo; - - // Setup depth-first search from the initial state. - todo.push(pair_state_successors(0, succ_queue())); - todo.top().second.push_front(successor(bddtrue, ecs_->aut->get_init_state())); - - for (;;) - { - assert(ecs_->root.size() == arc.size()); - - // Get the successors of the current state. - succ_queue& queue = todo.top().second; - - // First, we process all successors that we have already seen. - // This is an idea from Soheib Baarir. It helps to merge SCCs - // and get shorter traces faster. - succ_queue::iterator q = queue.begin(); - while (q != queue.end()) - { - int* i = ecs_->h.find(q->s); - if (!i) - { - // Skip unknown states. - ++q; - continue; - } - - // Skip states from dead SCCs. - if (*i != -1) - { - // 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; - bdd acc = q->acc; - while (threshold < ecs_->root.top().index) - { - assert(!ecs_->root.empty()); - assert(!arc.empty()); - acc |= ecs_->root.top().condition; - acc |= arc.top(); - 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; - - if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions()) - { - // We have found an accepting SCC. Clean up TODO. - // We must delete all states of apparing in TODO - // unless they are used as keys in H. - while (!todo.empty()) - { - succ_queue& queue = todo.top().second; - for (succ_queue::iterator q = queue.begin(); - q != queue.end(); ++q) - { - int* i = ecs_->h.find(q->s); - if (!i) - delete q->s; - else - // Delete the state if it is a clone - // of a state in the heap. - (void) ecs_->h.filter(q->s); - } - todo.pop(); - } - return false; - } - } - // We know the state exists. Since a state can have several - // representations (i.e., objects), make sure we delete - // anything but the first one seen (the one used as key in H). - (void) ecs_->h.filter(q->s); - // Remove that state from the queue, so we do not - // recurse into it. - succ_queue::iterator old = q++; - queue.erase(old); - } - - // If there is no more successor, backtrack. - if (queue.empty()) - { - // We have explored all successors of state CURR. - const state* curr = todo.top().first; - // Backtrack TODO. - todo.pop(); - if (todo.empty()) - // This automaton recognizes no word. - return true; - - // When backtracking the root of an SCC, we must also - // remove that SCC from the ARC/ROOT stacks. We must - // discard from H all reachable states from this SCC. - int* i = ecs_->h.find(curr); - assert(i); - assert(!ecs_->root.empty()); - if (ecs_->root.top().index == *i) - { - assert(!arc.empty()); - arc.pop(); - ecs_->root.pop(); - remove_component(curr); - } - continue; - } - - // Recurse. (Finally!) - - // Pick one successor off the list, and schedule its - // successors first on TODO. Update the various hashes and - // stacks. - successor succ = queue.front(); - queue.pop_front(); - ecs_->h.insert(succ.s, ++num); - ecs_->root.push(num); - arc.push(succ.acc); - todo.push(pair_state_successors(succ.s, succ_queue())); - succ_queue& new_queue = todo.top().second; - tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); - for (iter->first(); ! iter->done(); iter->next()) - new_queue.push_back(successor(iter->current_acceptance_conditions(), - iter->current_state())); - delete iter; - } - } - - ////////////////////////////////////////////////////////////////////// - - const state* - connected_component_hash_set::has_state(const state* s) const - { - set_type::const_iterator it = states.find(s); - if (it != states.end()) - { - if (s != *it) - delete s; - return *it; - } - else - return 0; - } - - void - connected_component_hash_set::insert(const state* s) - { - states.insert(s); - } - - ////////////////////////////////////////////////////////////////////// - - connected_component_hash_set_factory::connected_component_hash_set_factory() - : explicit_connected_component_factory() - { - } - - connected_component_hash_set* - connected_component_hash_set_factory::build() const - { - return new connected_component_hash_set(); - } - - const connected_component_hash_set_factory* - connected_component_hash_set_factory::instance() - { - static connected_component_hash_set_factory f; - return &f; - } - - ////////////////////////////////////////////////////////////////////// - - counter_example::counter_example(const emptiness_check_status* ecs, - const explicit_connected_component_factory* - eccf) - : ecs_(ecs) - { - assert(!ecs_->root.empty()); - assert(suffix.empty()); - - scc_stack::stack_type root = ecs_->root.s; - int comp_size = root.size(); - // Transform the stack of connected component into an array. - explicit_connected_component** scc = - new (explicit_connected_component*)[comp_size]; - for (int j = comp_size - 1; 0 <= j; --j) - { - scc[j] = eccf->build(); - scc[j]->index = root.top().index; - scc[j]->condition = root.top().condition; - root.pop(); - } - assert(root.empty()); - - // Build the set of states for all SCCs. - numbered_state_heap_const_iterator* i = ecs_->h.iterator(); - for (i->first(); !i->done(); i->next()) - { - int index = i->get_index(); - // Skip states from dead SCCs. - if (index < 0) - continue; - assert(index != 0); - - // Find the SCC this state belongs to. - int j; - for (j = 1; j < comp_size; ++j) - if (index < scc[j]->index) - break; - scc[j - 1]->insert(i->get_state()); - } - delete i; - - suffix.push_front(ecs_->h.filter(ecs_->aut->get_init_state())); - - // We build a path trough each SCC in the stack. For the - // first SCC, the starting state is the initial state of the - // automaton. The destination state is the closest state - // from the next SCC. This destination state becomes the - // starting state when building a path though the next SCC. - for (int k = 0; k < comp_size - 1; ++k) - { - // FIFO for the breadth-first search. - // (we are looking for the closest state in the next SCC.) - std::deque todo; - - // Record the father of each state, while performing the BFS. - typedef std::map father_map; - father_map father; - - // Initial state of the BFS. - const state* start = suffix.back(); - { - tgba_succ_iterator* i = ecs_->aut->succ_iter(start); - todo.push_back(pair_state_iter(start, i)); - } - - while (!todo.empty()) - { - const state* src = todo.front().first; - tgba_succ_iterator* i = todo.front().second; - todo.pop_front(); - - for (i->first(); !i->done(); i->next()) - { - const state* dest = i->current_state(); - - // Are we leaving this SCC? - const state* h_dest = scc[k]->has_state(dest); - if (!h_dest) - { - // If we have found a state in the next SCC. - // Unwind the path and populate SUFFIX. - h_dest = scc[k+1]->has_state(dest); - if (h_dest) - { - state_sequence seq; - - seq.push_front(h_dest); - while (src->compare(start)) - { - seq.push_front(src); - src = father[src]; - } - // Append SEQ to SUFFIX. - suffix.splice(suffix.end(), seq); - // Exit this BFS for this SCC. - while (!todo.empty()) - { - delete todo.front().second; - todo.pop_front(); - } - break; - } - // Restrict the BFS to state inside the SCC. - continue; - } - - if (father.find(h_dest) == father.end()) - { - todo.push_back - (pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest))); - father[h_dest] = src; - } - } - delete i; - } - } - - accepting_path(scc[comp_size - 1], suffix.back(), - scc[comp_size - 1]->condition); - - - for (int j = comp_size - 1; 0 <= j; --j) - delete scc[j]; - delete[] scc; - } - - void - counter_example::complete_cycle(const explicit_connected_component* scc, - const state* from, - const state* to) - { - // If by change or period already ends on the state we have - // to reach back, we are done. - if (from == to - && ! period.empty()) - return; - - // Records backlinks to parent state during the BFS. - // (This also stores the propositions of this link.) - std::map father; - - // BFS queue. - std::deque todo; - - // Initial state. - { - tgba_succ_iterator* i = ecs_->aut->succ_iter(from); - todo.push_back(pair_state_iter(from, i)); - } - - while (!todo.empty()) - { - const state* src = todo.front().first; - tgba_succ_iterator* i = todo.front().second; - todo.pop_front(); - for (i->first(); !i->done(); i->next()) - { - const state* dest = i->current_state(); - - // Do not escape this SCC or visit a state already visited. - const state* h_dest = scc->has_state(dest); - if (!h_dest) - { - delete dest; - continue; - } - if (father.find(h_dest) != father.end()) - continue; - - bdd cond = i->current_condition(); - - // If we have reached our destination, unwind the path - // and populate PERIOD. - if (h_dest == to) - { - cycle_path p; - p.push_front(state_proposition(h_dest, cond)); - while (src != from) - { - const state_proposition& psi = father[src]; - p.push_front(state_proposition(src, psi.second)); - src = psi.first; - } - period.splice(period.end(), p); - - // Exit the BFS, but release all iterators first. - while (!todo.empty()) - { - delete todo.front().second; - todo.pop_front(); - } - break; - } - - // Common case: record backlinks and continue BFS. - todo.push_back(pair_state_iter(h_dest, - ecs_->aut->succ_iter(h_dest))); - father[h_dest] = state_proposition(src, cond); - } - delete i; - } - } - - - namespace - { - struct triplet - { - const state* s; // Current state. - tgba_succ_iterator* iter; // Iterator to successor of the current state. - bdd acc; // All acceptance conditions traversed by - // the path so far. - - triplet (const state* s, tgba_succ_iterator* iter, bdd acc) - : s(s), iter(iter), acc(acc) - { - } - }; - - } - - void - counter_example::accepting_path(const explicit_connected_component* scc, - const state* start, bdd acc_to_traverse) - { - // State seen during the DFS. - typedef Sgi::hash_set set_type; - set_type seen; - // DFS stack. - std::stack todo; - - while (acc_to_traverse != bddfalse) - { - // Initial state. - { - tgba_succ_iterator* i = ecs_->aut->succ_iter(start); - i->first(); - todo.push(triplet(start, i, bddfalse)); - seen.insert(start); - } - - // The path being explored currently. - cycle_path path; - // The best path seen so far. - cycle_path best_path; - // The acceptance conditions traversed by BEST_PATH. - bdd best_acc = bddfalse; - - while (!todo.empty()) - { - tgba_succ_iterator* iter = todo.top().iter; - const state* s = todo.top().s; - - // Nothing more to explore, backtrack. - if (iter->done()) - { - todo.pop(); - delete iter; - seen.erase(s); - if (todo.size()) - { - assert(path.size()); - path.pop_back(); - } - continue; - } - - // We must not escape the current SCC. - const state* dest = iter->current_state(); - const state* h_dest = scc->has_state(dest); - if (!h_dest) - { - delete dest; - iter->next(); - continue; - } - - bdd acc = iter->current_acceptance_conditions() | todo.top().acc; - path.push_back(state_proposition(h_dest, - iter->current_condition())); - - // Advance iterator for next step. - iter->next(); - - if (seen.find(h_dest) == seen.end()) - { - // A new state: continue the DFS. - tgba_succ_iterator* di = ecs_->aut->succ_iter(h_dest); - di->first(); - todo.push(triplet(h_dest, di, acc)); - seen.insert(h_dest); - continue; - } - - // We have completed a full cycle. - - // If we already have a best path, let see if the current - // one is better. - if (best_path.size()) - { - // When comparing the merits of two paths, only the - // acceptance conditions we are trying the traverse - // are important. - bdd acc_restrict = acc & acc_to_traverse; - bdd best_acc_restrict = best_acc & acc_to_traverse; - - // If the best path and the current one traverse the - // same acceptance conditions, we keep the shorter - // path. Otherwise, we keep the path which has the - // more acceptance conditions. - if (best_acc_restrict == acc_restrict) - { - if (best_path.size() <= path.size()) - goto backtrack_path; - } - else - { - // `best_acc_restrict >> acc_restrict' is true - // when the set of acceptance conditions of - // best_acc_restrict is included in the set of - // acceptance conditions of acc_restrict. - // - // FIXME: It would be better to count the number - // of acceptance conditions. - if (bddtrue != (best_acc_restrict >> acc_restrict)) - goto backtrack_path; - } - } - - // The current path the best one. - best_path = path; - best_acc = acc; - - backtrack_path: - // Continue exploration from parent to find better paths. - // (Do not pop PATH if ITER is done, because that will be - // done at the top of the loop, among other things.) - if (!iter->done()) - path.pop_back(); - } - - // Append our best path to the period. - for (cycle_path::iterator it = best_path.begin(); - it != best_path.end(); ++it) - period.push_back(*it); - - // Prepare to find another path for the remaining acceptance - // conditions. - acc_to_traverse -= best_acc; - start = period.back().first; - } - - // Complete the path so that it goes back to its beginning, - // forming a cycle. - complete_cycle(scc, start, suffix.back()); - } - - std::ostream& - counter_example::print_result(std::ostream& os, const tgba* restrict) const - { - os << "Prefix:" << std::endl; - const bdd_dict* d = ecs_->aut->get_dict(); - for (state_sequence::const_iterator i_se = suffix.begin(); - i_se != suffix.end(); ++i_se) - { - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(*i_se, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(*i_se) << std::endl; - } - } - os << "Cycle:" <second) << std::endl; - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(it->first, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(it->first) << std::endl; - } - } - return os; - } - - - void - counter_example::print_stats(std::ostream& os) const - { - ecs_->print_stats(os); - os << suffix.size() << " states in suffix" << std::endl; - os << period.size() << " states in period" << std::endl; - } - -} diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh deleted file mode 100644 index 7ee3bbf28..000000000 --- a/src/tgbaalgos/emptinesscheck.hh +++ /dev/null @@ -1,294 +0,0 @@ -// Copyright (C) 2003, 2004 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. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#ifndef SPOT_EMPTINESS_CHECK_HH -# define SPOT_EMPTINESS_CHECK_HH - -#include "tgba/tgba.hh" -#include "misc/hash.hh" -#include -#include -#include -#include - -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; - - typedef std::stack stack_type; - stack_type s; - }; - - class numbered_state_heap_const_iterator - { - public: - virtual ~numbered_state_heap_const_iterator() {} - - virtual void first() = 0; - virtual void next() = 0; - virtual bool done() const = 0; - - virtual const state* get_state() const = 0; - virtual int get_index() const = 0; - }; - - class numbered_state_heap - { - public: - virtual ~numbered_state_heap() {} - //@{ - /// \brief Is state in the heap? - /// - /// Returns 0 if \a s is not in the heap. or a pointer to - /// its number if it is. - virtual const int* find(const state* s) const = 0; - virtual int* find(const state* s) = 0; - //@} - - virtual void insert(const state* s, int index) = 0; - virtual int size() const = 0; - - virtual numbered_state_heap_const_iterator* iterator() const = 0; - - /// \brief Return a state which is equal to \a s, but is in \c h, - /// and free \a s if it is different. - /// - /// Doing so simplify memory management, because we don't have to - /// track which state need to be kept or deallocated: all key in - /// \c h should last for the whole life of the emptiness_check. - virtual const state* filter(const state* s) const = 0; - }; - - class numbered_state_heap_hash_map : public numbered_state_heap - { - public: - virtual ~numbered_state_heap_hash_map(); - - virtual const int* find(const state* s) const; - virtual int* find(const state* s); - virtual void insert(const state* s, int index); - virtual int size() const; - - virtual numbered_state_heap_const_iterator* iterator() const; - - virtual const state* filter(const state* s) const; - - protected: - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - friend class numbered_state_heap_hash_map_const_iterator; - }; - - class emptiness_check_status - { - public: - emptiness_check_status(const tgba* aut); - ~emptiness_check_status(); - - const tgba* aut; - scc_stack root; - numbered_state_heap_hash_map h; ///< Map of visited states. - - /// Output statistics about this object. - void print_stats(std::ostream& os) const; - }; - - //@{ - /// \brief Check whether the language of an automate is empty. - /// - /// This is based on the following paper. - /// \verbatim - /// @InProceedings{couvreur.99.fm, - /// author = {Jean-Michel Couvreur}, - /// title = {On-the-fly Verification of Temporal Logic}, - /// pages = {253--271}, - /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, - /// booktitle = {Proceedings of the World Congress on Formal Methods in - /// the Development of Computing Systems (FM'99)}, - /// publisher = {Springer-Verlag}, - /// series = {Lecture Notes in Computer Science}, - /// volume = {1708}, - /// year = {1999}, - /// address = {Toulouse, France}, - /// month = {September}, - /// isbn = {3-540-66587-0} - /// } - /// \endverbatim - /// - /// check() returns true if the automaton's language is empty. When - /// it return false, a stack of SCC has been built and can - /// later be used by counter_example(). - /// - /// There are two variants of this algorithm: emptiness_check() and - /// emptiness_check_shy(). They differ in their memory usage, the - /// number for successors computed before they are used and the way - /// the depth first search is directed. - /// - /// emptiness_check() performs a straightforward depth first search. - /// The DFS stacks store tgba_succ_iterators, so that only the - /// iterators which really are explored are computed. - /// - /// emptiness_check_shy() try to explore successors which are - /// visited states first. this helps to merge SCCs and generally - /// helps to produce shorter counter-examples. However this - /// algorithm cannot stores unprocessed successors as - /// tgba_succ_iterators: it must compute all successors of a state - /// at once in order to decide which to explore first, and must keep - /// a list of all unexplored successors in its DFS stack. - class emptiness_check - { - public: - emptiness_check(const tgba* a); - virtual ~emptiness_check(); - - /// check whether the automaton's language is empty - virtual bool check(); - - const emptiness_check_status* result() const; - - protected: - emptiness_check_status* ecs_; - /// \brief Remove a strongly component from the hash. - /// - /// This function remove all accessible state from a given - /// state. In other words, it removes the strongly connected - /// component that contains this state. - void remove_component(const state* start_delete); - }; - - class emptiness_check_shy : public emptiness_check - { - public: - emptiness_check_shy(const tgba* a); - virtual ~emptiness_check_shy(); - - virtual bool check(); - }; - //@} - - - class explicit_connected_component: public scc_stack::connected_component - { - public: - virtual ~explicit_connected_component() {} - /// \brief Check if the SCC contains states \a s. - /// - /// Return the representative of \a s in the SCC, and delete \a - /// s if it is different (acting like - /// numbered_state_heap::filter), or 0 otherwise. - virtual const state* has_state(const state* s) const = 0; - - /// Insert a new state in the SCC. - virtual void insert(const state* s) = 0; - }; - - class connected_component_hash_set: public explicit_connected_component - { - public: - virtual ~connected_component_hash_set() {} - virtual const state* has_state(const state* s) const; - virtual void insert(const state* s); - protected: - typedef Sgi::hash_set set_type; - set_type states; - }; - - class explicit_connected_component_factory - { - public: - virtual ~explicit_connected_component_factory() {} - virtual explicit_connected_component* build() const = 0; - }; - - class connected_component_hash_set_factory : - public explicit_connected_component_factory - { - public: - virtual connected_component_hash_set* build() const; - - static const connected_component_hash_set_factory* instance(); - - protected: - virtual ~connected_component_hash_set_factory() {} - connected_component_hash_set_factory(); - }; - - class counter_example - { - public: - counter_example(const emptiness_check_status* ecs, - const explicit_connected_component_factory* - eccf = connected_component_hash_set_factory::instance()); - - typedef std::pair state_proposition; - typedef std::list state_sequence; - typedef std::list cycle_path; - state_sequence suffix; - cycle_path period; - - /// \brief Display the example computed by counter_example(). - /// - /// \param restrict optional automaton to project the example on. - std::ostream& print_result(std::ostream& os, - const tgba* restrict = 0) const; - - /// Output statistics about this object. - void print_stats(std::ostream& os) const; - - protected: - /// Called by counter_example to find a path which traverses all - /// acceptance conditions in the accepted SCC. - void accepting_path (const explicit_connected_component* scc, - const state* start, bdd acc_to_traverse); - - /// Complete a cycle that caraterise the period of the counter - /// example. Append a sequence to the path given by accepting_path. - void complete_cycle(const explicit_connected_component* scc, - const state* from, const state* to); - - private: - const emptiness_check_status* ecs_; - }; -} -#endif // SPOT_EMPTINESS_CHECK_HH diff --git a/src/tgbaalgos/gtec/.cvsignore b/src/tgbaalgos/gtec/.cvsignore new file mode 100644 index 000000000..799fc9785 --- /dev/null +++ b/src/tgbaalgos/gtec/.cvsignore @@ -0,0 +1,6 @@ +.deps +.libs +*.lo +*.la +Makefile +Makefile.in diff --git a/src/tgbaalgos/gtec/Makefile.am b/src/tgbaalgos/gtec/Makefile.am new file mode 100644 index 000000000..b8602669a --- /dev/null +++ b/src/tgbaalgos/gtec/Makefile.am @@ -0,0 +1,42 @@ +## Copyright (C) 2004 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. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/../.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +gtecdir = $(pkgincludedir)/tgbaalgos/gtec + +gtec_HEADERS = \ + ce.hh \ + explscc.hh \ + gtec.hh \ + nsheap.hh \ + sccstack.hh \ + status.hh + +noinst_LTLIBRARIES = libgtec.la +libgtec_la_SOURCES = \ + ce.cc \ + explscc.cc \ + gtec.cc \ + nsheap.cc \ + sccstack.cc \ + status.cc diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc new file mode 100644 index 000000000..b55d71029 --- /dev/null +++ b/src/tgbaalgos/gtec/ce.cc @@ -0,0 +1,443 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "ce.hh" +#include "tgba/bddprint.hh" +#include + +namespace spot +{ + namespace + { + typedef std::pair pair_state_iter; + } + + counter_example::counter_example(const emptiness_check_status* ecs, + const explicit_connected_component_factory* + eccf) + : ecs_(ecs) + { + assert(!ecs_->root.empty()); + assert(suffix.empty()); + + scc_stack::stack_type root = ecs_->root.s; + int comp_size = root.size(); + // Transform the stack of connected component into an array. + explicit_connected_component** scc = + new (explicit_connected_component*)[comp_size]; + for (int j = comp_size - 1; 0 <= j; --j) + { + scc[j] = eccf->build(); + scc[j]->index = root.top().index; + scc[j]->condition = root.top().condition; + root.pop(); + } + assert(root.empty()); + + // Build the set of states for all SCCs. + numbered_state_heap_const_iterator* i = ecs_->h.iterator(); + for (i->first(); !i->done(); i->next()) + { + int index = i->get_index(); + // Skip states from dead SCCs. + if (index < 0) + continue; + assert(index != 0); + + // Find the SCC this state belongs to. + int j; + for (j = 1; j < comp_size; ++j) + if (index < scc[j]->index) + break; + scc[j - 1]->insert(i->get_state()); + } + delete i; + + suffix.push_front(ecs_->h.filter(ecs_->aut->get_init_state())); + + // We build a path trough each SCC in the stack. For the + // first SCC, the starting state is the initial state of the + // automaton. The destination state is the closest state + // from the next SCC. This destination state becomes the + // starting state when building a path though the next SCC. + for (int k = 0; k < comp_size - 1; ++k) + { + // FIFO for the breadth-first search. + // (we are looking for the closest state in the next SCC.) + std::deque todo; + + // Record the father of each state, while performing the BFS. + typedef std::map father_map; + father_map father; + + // Initial state of the BFS. + const state* start = suffix.back(); + { + tgba_succ_iterator* i = ecs_->aut->succ_iter(start); + todo.push_back(pair_state_iter(start, i)); + } + + while (!todo.empty()) + { + const state* src = todo.front().first; + tgba_succ_iterator* i = todo.front().second; + todo.pop_front(); + + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + + // Are we leaving this SCC? + const state* h_dest = scc[k]->has_state(dest); + if (!h_dest) + { + // If we have found a state in the next SCC. + // Unwind the path and populate SUFFIX. + h_dest = scc[k+1]->has_state(dest); + if (h_dest) + { + state_sequence seq; + + seq.push_front(h_dest); + while (src->compare(start)) + { + seq.push_front(src); + src = father[src]; + } + // Append SEQ to SUFFIX. + suffix.splice(suffix.end(), seq); + // Exit this BFS for this SCC. + while (!todo.empty()) + { + delete todo.front().second; + todo.pop_front(); + } + break; + } + // Restrict the BFS to state inside the SCC. + continue; + } + + if (father.find(h_dest) == father.end()) + { + todo.push_back + (pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest))); + father[h_dest] = src; + } + } + delete i; + } + } + + accepting_path(scc[comp_size - 1], suffix.back(), + scc[comp_size - 1]->condition); + + + for (int j = comp_size - 1; 0 <= j; --j) + delete scc[j]; + delete[] scc; + } + + void + counter_example::complete_cycle(const explicit_connected_component* scc, + const state* from, + const state* to) + { + // If by change or period already ends on the state we have + // to reach back, we are done. + if (from == to + && ! period.empty()) + return; + + // Records backlinks to parent state during the BFS. + // (This also stores the propositions of this link.) + std::map father; + + // BFS queue. + std::deque todo; + + // Initial state. + { + tgba_succ_iterator* i = ecs_->aut->succ_iter(from); + todo.push_back(pair_state_iter(from, i)); + } + + while (!todo.empty()) + { + const state* src = todo.front().first; + tgba_succ_iterator* i = todo.front().second; + todo.pop_front(); + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + + // Do not escape this SCC or visit a state already visited. + const state* h_dest = scc->has_state(dest); + if (!h_dest) + { + delete dest; + continue; + } + if (father.find(h_dest) != father.end()) + continue; + + bdd cond = i->current_condition(); + + // If we have reached our destination, unwind the path + // and populate PERIOD. + if (h_dest == to) + { + cycle_path p; + p.push_front(state_proposition(h_dest, cond)); + while (src != from) + { + const state_proposition& psi = father[src]; + p.push_front(state_proposition(src, psi.second)); + src = psi.first; + } + period.splice(period.end(), p); + + // Exit the BFS, but release all iterators first. + while (!todo.empty()) + { + delete todo.front().second; + todo.pop_front(); + } + break; + } + + // Common case: record backlinks and continue BFS. + todo.push_back(pair_state_iter(h_dest, + ecs_->aut->succ_iter(h_dest))); + father[h_dest] = state_proposition(src, cond); + } + delete i; + } + } + + + namespace + { + struct triplet + { + const state* s; // Current state. + tgba_succ_iterator* iter; // Iterator to successor of the current state. + bdd acc; // All acceptance conditions traversed by + // the path so far. + + triplet (const state* s, tgba_succ_iterator* iter, bdd acc) + : s(s), iter(iter), acc(acc) + { + } + }; + + } + + void + counter_example::accepting_path(const explicit_connected_component* scc, + const state* start, bdd acc_to_traverse) + { + // State seen during the DFS. + typedef Sgi::hash_set set_type; + set_type seen; + // DFS stack. + std::stack todo; + + while (acc_to_traverse != bddfalse) + { + // Initial state. + { + tgba_succ_iterator* i = ecs_->aut->succ_iter(start); + i->first(); + todo.push(triplet(start, i, bddfalse)); + seen.insert(start); + } + + // The path being explored currently. + cycle_path path; + // The best path seen so far. + cycle_path best_path; + // The acceptance conditions traversed by BEST_PATH. + bdd best_acc = bddfalse; + + while (!todo.empty()) + { + tgba_succ_iterator* iter = todo.top().iter; + const state* s = todo.top().s; + + // Nothing more to explore, backtrack. + if (iter->done()) + { + todo.pop(); + delete iter; + seen.erase(s); + if (todo.size()) + { + assert(path.size()); + path.pop_back(); + } + continue; + } + + // We must not escape the current SCC. + const state* dest = iter->current_state(); + const state* h_dest = scc->has_state(dest); + if (!h_dest) + { + delete dest; + iter->next(); + continue; + } + + bdd acc = iter->current_acceptance_conditions() | todo.top().acc; + path.push_back(state_proposition(h_dest, + iter->current_condition())); + + // Advance iterator for next step. + iter->next(); + + if (seen.find(h_dest) == seen.end()) + { + // A new state: continue the DFS. + tgba_succ_iterator* di = ecs_->aut->succ_iter(h_dest); + di->first(); + todo.push(triplet(h_dest, di, acc)); + seen.insert(h_dest); + continue; + } + + // We have completed a full cycle. + + // If we already have a best path, let see if the current + // one is better. + if (best_path.size()) + { + // When comparing the merits of two paths, only the + // acceptance conditions we are trying the traverse + // are important. + bdd acc_restrict = acc & acc_to_traverse; + bdd best_acc_restrict = best_acc & acc_to_traverse; + + // If the best path and the current one traverse the + // same acceptance conditions, we keep the shorter + // path. Otherwise, we keep the path which has the + // more acceptance conditions. + if (best_acc_restrict == acc_restrict) + { + if (best_path.size() <= path.size()) + goto backtrack_path; + } + else + { + // `best_acc_restrict >> acc_restrict' is true + // when the set of acceptance conditions of + // best_acc_restrict is included in the set of + // acceptance conditions of acc_restrict. + // + // FIXME: It would be better to count the number + // of acceptance conditions. + if (bddtrue != (best_acc_restrict >> acc_restrict)) + goto backtrack_path; + } + } + + // The current path the best one. + best_path = path; + best_acc = acc; + + backtrack_path: + // Continue exploration from parent to find better paths. + // (Do not pop PATH if ITER is done, because that will be + // done at the top of the loop, among other things.) + if (!iter->done()) + path.pop_back(); + } + + // Append our best path to the period. + for (cycle_path::iterator it = best_path.begin(); + it != best_path.end(); ++it) + period.push_back(*it); + + // Prepare to find another path for the remaining acceptance + // conditions. + acc_to_traverse -= best_acc; + start = period.back().first; + } + + // Complete the path so that it goes back to its beginning, + // forming a cycle. + complete_cycle(scc, start, suffix.back()); + } + + std::ostream& + counter_example::print_result(std::ostream& os, const tgba* restrict) const + { + os << "Prefix:" << std::endl; + const bdd_dict* d = ecs_->aut->get_dict(); + for (state_sequence::const_iterator i_se = suffix.begin(); + i_se != suffix.end(); ++i_se) + { + os << " "; + if (restrict) + { + const state* s = ecs_->aut->project_state(*i_se, restrict); + assert(s); + os << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << ecs_->aut->format_state(*i_se) << std::endl; + } + } + os << "Cycle:" <second) << std::endl; + os << " "; + if (restrict) + { + const state* s = ecs_->aut->project_state(it->first, restrict); + assert(s); + os << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << ecs_->aut->format_state(it->first) << std::endl; + } + } + return os; + } + + + void + counter_example::print_stats(std::ostream& os) const + { + ecs_->print_stats(os); + os << suffix.size() << " states in suffix" << std::endl; + os << period.size() << " states in period" << std::endl; + } + +} diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh new file mode 100644 index 000000000..281e71725 --- /dev/null +++ b/src/tgbaalgos/gtec/ce.hh @@ -0,0 +1,68 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_CE_HH +# define SPOT_TGBAALGOS_GTEC_CE_HH + +#include "status.hh" +#include "explscc.hh" + +namespace spot +{ + class counter_example + { + public: + counter_example(const emptiness_check_status* ecs, + const explicit_connected_component_factory* + eccf = connected_component_hash_set_factory::instance()); + + typedef std::pair state_proposition; + typedef std::list state_sequence; + typedef std::list cycle_path; + state_sequence suffix; + cycle_path period; + + /// \brief Display the example computed by counter_example(). + /// + /// \param restrict optional automaton to project the example on. + std::ostream& print_result(std::ostream& os, + const tgba* restrict = 0) const; + + /// Output statistics about this object. + void print_stats(std::ostream& os) const; + + protected: + /// Called by counter_example to find a path which traverses all + /// acceptance conditions in the accepted SCC. + void accepting_path (const explicit_connected_component* scc, + const state* start, bdd acc_to_traverse); + + /// Complete a cycle that caraterise the period of the counter + /// example. Append a sequence to the path given by accepting_path. + void complete_cycle(const explicit_connected_component* scc, + const state* from, const state* to); + + private: + const emptiness_check_status* ecs_; + }; +} + +#endif // SPOT_TGBAALGOS_GTEC_CE_HH diff --git a/src/tgbaalgos/gtec/explscc.cc b/src/tgbaalgos/gtec/explscc.cc new file mode 100644 index 000000000..5e2826dfe --- /dev/null +++ b/src/tgbaalgos/gtec/explscc.cc @@ -0,0 +1,65 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "explscc.hh" + +namespace spot +{ + const state* + connected_component_hash_set::has_state(const state* s) const + { + set_type::const_iterator it = states.find(s); + if (it != states.end()) + { + if (s != *it) + delete s; + return *it; + } + else + return 0; + } + + void + connected_component_hash_set::insert(const state* s) + { + states.insert(s); + } + + ////////////////////////////////////////////////////////////////////// + + connected_component_hash_set_factory::connected_component_hash_set_factory() + : explicit_connected_component_factory() + { + } + + connected_component_hash_set* + connected_component_hash_set_factory::build() const + { + return new connected_component_hash_set(); + } + + const connected_component_hash_set_factory* + connected_component_hash_set_factory::instance() + { + static connected_component_hash_set_factory f; + return &f; + } +} diff --git a/src/tgbaalgos/gtec/explscc.hh b/src/tgbaalgos/gtec/explscc.hh new file mode 100644 index 000000000..b3cde4b3b --- /dev/null +++ b/src/tgbaalgos/gtec/explscc.hh @@ -0,0 +1,89 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_EXPLSCC_HH +# define SPOT_TGBAALGOS_GTEC_EXPLSCC_HH + +#include "misc/hash.hh" +#include "tgba/state.hh" +#include "sccstack.hh" + +namespace spot +{ + /// An SCC storing all its states explicitly. + class explicit_connected_component: public scc_stack::connected_component + { + public: + virtual ~explicit_connected_component() {} + /// \brief Check if the SCC contains states \a s. + /// + /// Return the representative of \a s in the SCC, and delete \a + /// s if it is different (acting like + /// numbered_state_heap::filter), or 0 otherwise. + virtual const state* has_state(const state* s) const = 0; + + /// Insert a new state in the SCC. + virtual void insert(const state* s) = 0; + }; + + /// A straightforward implementation of explicit_connected_component + /// using a hash. + class connected_component_hash_set: public explicit_connected_component + { + public: + virtual ~connected_component_hash_set() {} + virtual const state* has_state(const state* s) const; + virtual void insert(const state* s); + protected: + typedef Sgi::hash_set set_type; + set_type states; + }; + + /// Abstract factory for explicit_connected_component. + class explicit_connected_component_factory + { + public: + virtual ~explicit_connected_component_factory() {} + /// Create an explicit_connected_component. + virtual explicit_connected_component* build() const = 0; + }; + + /// \brief Factory for connected_component_hash_set. + /// + /// This class is a singleton. Retrieve the instance using instance(). + class connected_component_hash_set_factory : + public explicit_connected_component_factory + { + public: + virtual connected_component_hash_set* build() const; + + /// Get the unique instance of this class. + static const connected_component_hash_set_factory* instance(); + + protected: + virtual ~connected_component_hash_set_factory() {} + /// Construction is forbiden. + connected_component_hash_set_factory(); + }; +} + +#endif // SPOT_TGBAALGOS_GTEC_EXPLSCC_HH diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc new file mode 100644 index 000000000..f85145947 --- /dev/null +++ b/src/tgbaalgos/gtec/gtec.cc @@ -0,0 +1,414 @@ +// Copyright (C) 2003, 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "gtec.hh" + +namespace spot +{ + namespace + { + typedef std::pair pair_state_iter; + } + + emptiness_check::emptiness_check(const tgba* a) + { + ecs_ = new emptiness_check_status(a); + } + + emptiness_check::~emptiness_check() + { + delete ecs_; + } + + void + emptiness_check::remove_component(const state* from) + { + // Remove from H all states which are reachable from state FROM. + + // Stack of iterators towards states to remove. + std::stack to_remove; + + // Remove FROM itself, and prepare to remove its successors. + // (FROM should be in H, otherwise it means all reachable + // states from FROM have already been removed and there is no + // point in calling remove_component.) + int* hi = ecs_->h.find(from); + assert(hi); + assert(*hi != -1); + *hi = -1; + tgba_succ_iterator* i = ecs_->aut->succ_iter(from); + + for (;;) + { + // Remove each destination of this iterator. + for (i->first(); !i->done(); i->next()) + { + state* s = i->current_state(); + int *hi = ecs_->h.find(s); + assert(hi); + + if (*hi != -1) + { + *hi = -1; + to_remove.push(ecs_->aut->succ_iter(s)); + } + delete s; + } + delete i; + if (to_remove.empty()) + break; + i = to_remove.top(); + to_remove.pop(); + } + } + + bool + emptiness_check::check() + { + // We use five main data in this algorithm: + // * emptiness_check::root, a stack of strongly connected components (SCC), + // * emptiness_check::h, a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + // * num, the number of visited nodes. Used to set the order of each + // visited node, + int num = 1; + // * todo, the depth-first search stack. This holds pairs of the + // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator + // over the successors of STATE. In our use, ITERATOR should + // always be freed when TODO is popped, but STATE should not because + // it is also used as a key in H. + std::stack todo; + + // Setup depth-first search from the initial state. + { + state* init = ecs_->aut->get_init_state(); + ecs_->h.insert(init, 1); + ecs_->root.push(1); + arc.push(bddfalse); + tgba_succ_iterator* iter = ecs_->aut->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + } + + while (!todo.empty()) + { + assert(ecs_->root.size() == arc.size()); + + // We are looking at the next successor in SUCC. + tgba_succ_iterator* succ = todo.top().second; + + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. + const state* curr = todo.top().first; + + // Backtrack TODO. + todo.pop(); + + // When backtracking the root of an SCC, we must also + // remove that SCC from the ARC/ROOT stacks. We must + // discard from H all reachable states from this SCC. + int* i = ecs_->h.find(curr); + assert(i); + assert(!ecs_->root.empty()); + if (ecs_->root.top().index == *i) + { + assert(!arc.empty()); + arc.pop(); + ecs_->root.pop(); + remove_component(curr); + } + + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } + + // We have a successor to look at. Fetch the values + // (destination state, acceptance conditions of the arc) + // we are interested in... + const state* dest = succ->current_state(); + bdd acc = succ->current_acceptance_conditions(); + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. + + // Are we going to a new state? + int* i = ecs_->h.find(dest); + if (!i) + { + // Yes. Number it, stack it, and register its successors + // for later processing. + ecs_->h.insert(dest, ++num); + ecs_->root.push(num); + arc.push(acc); + tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + continue; + } + + // We know the state exists. Since a state can have several + // representations (i.e., objects), make sure we delete + // anything but the first one seen (the one used as key in H). + (void) ecs_->h.filter(dest); + + // If we have reached a dead component, ignore it. + 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; + while (threshold < ecs_->root.top().index) + { + assert(!ecs_->root.empty()); + assert(!arc.empty()); + acc |= ecs_->root.top().condition; + acc |= arc.top(); + 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; + + if (ecs_->root.top().condition + == ecs_->aut->all_acceptance_conditions()) + { + // We have found an accepting SCC. + // Release all iterators in TODO. + while (!todo.empty()) + { + delete todo.top().second; + todo.pop(); + } + return false; + } + } + // This automaton recognizes no word. + return true; + } + + const emptiness_check_status* + emptiness_check::result() const + { + return ecs_; + } + + ////////////////////////////////////////////////////////////////////// + + emptiness_check_shy::emptiness_check_shy(const tgba* a) + : emptiness_check(a) + { + } + + emptiness_check_shy::~emptiness_check_shy() + { + } + + struct successor { + bdd acc; + const spot::state* s; + successor(bdd acc, const spot::state* s): acc(acc), s(s) {} + }; + + bool + emptiness_check_shy::check() + { + // We use five main data in this algorithm: + // * emptiness_check::root, a stack of strongly connected components (SCC), + // * emptiness_check::h, a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + // * num, the number of visited nodes. Used to set the order of each + // visited node, + int num = 1; + // * todo, the depth-first search stack. This holds pairs of the + // form (STATE, SUCCESSORS) where SUCCESSORS is a list of + // (ACCEPTANCE_CONDITIONS, STATE) pairs. + typedef std::list succ_queue; + typedef std::pair pair_state_successors; + std::stack todo; + + // Setup depth-first search from the initial state. + todo.push(pair_state_successors(0, succ_queue())); + todo.top().second.push_front(successor(bddtrue, + ecs_->aut->get_init_state())); + + for (;;) + { + assert(ecs_->root.size() == arc.size()); + + // Get the successors of the current state. + succ_queue& queue = todo.top().second; + + // First, we process all successors that we have already seen. + // This is an idea from Soheib Baarir. It helps to merge SCCs + // and get shorter traces faster. + succ_queue::iterator q = queue.begin(); + while (q != queue.end()) + { + int* i = ecs_->h.find(q->s); + if (!i) + { + // Skip unknown states. + ++q; + continue; + } + + // Skip states from dead SCCs. + if (*i != -1) + { + // 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; + bdd acc = q->acc; + while (threshold < ecs_->root.top().index) + { + assert(!ecs_->root.empty()); + assert(!arc.empty()); + acc |= ecs_->root.top().condition; + acc |= arc.top(); + 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; + + if (ecs_->root.top().condition + == ecs_->aut->all_acceptance_conditions()) + { + // We have found an accepting SCC. Clean up TODO. + // We must delete all states of apparing in TODO + // unless they are used as keys in H. + while (!todo.empty()) + { + succ_queue& queue = todo.top().second; + for (succ_queue::iterator q = queue.begin(); + q != queue.end(); ++q) + { + int* i = ecs_->h.find(q->s); + if (!i) + delete q->s; + else + // Delete the state if it is a clone + // of a state in the heap. + (void) ecs_->h.filter(q->s); + } + todo.pop(); + } + return false; + } + } + // We know the state exists. Since a state can have several + // representations (i.e., objects), make sure we delete + // anything but the first one seen (the one used as key in H). + (void) ecs_->h.filter(q->s); + // Remove that state from the queue, so we do not + // recurse into it. + succ_queue::iterator old = q++; + queue.erase(old); + } + + // If there is no more successor, backtrack. + if (queue.empty()) + { + // We have explored all successors of state CURR. + const state* curr = todo.top().first; + // Backtrack TODO. + todo.pop(); + if (todo.empty()) + // This automaton recognizes no word. + return true; + + // When backtracking the root of an SCC, we must also + // remove that SCC from the ARC/ROOT stacks. We must + // discard from H all reachable states from this SCC. + int* i = ecs_->h.find(curr); + assert(i); + assert(!ecs_->root.empty()); + if (ecs_->root.top().index == *i) + { + assert(!arc.empty()); + arc.pop(); + ecs_->root.pop(); + remove_component(curr); + } + continue; + } + + // Recurse. (Finally!) + + // Pick one successor off the list, and schedule its + // successors first on TODO. Update the various hashes and + // stacks. + successor succ = queue.front(); + queue.pop_front(); + ecs_->h.insert(succ.s, ++num); + ecs_->root.push(num); + arc.push(succ.acc); + todo.push(pair_state_successors(succ.s, succ_queue())); + succ_queue& new_queue = todo.top().second; + tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); + for (iter->first(); ! iter->done(); iter->next()) + new_queue.push_back(successor(iter->current_acceptance_conditions(), + iter->current_state())); + delete iter; + } + } +} diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh new file mode 100644 index 000000000..01589d537 --- /dev/null +++ b/src/tgbaalgos/gtec/gtec.hh @@ -0,0 +1,114 @@ +// Copyright (C) 2003, 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_GTEC_HH +# define SPOT_TGBAALGOS_GTEC_GTEC_HH + +#include "status.hh" + +namespace spot +{ + /// \brief Check whether the language of an automate is empty. + /// + /// This is based on the following paper. + /// \verbatim + /// @InProceedings{couvreur.99.fm, + /// author = {Jean-Michel Couvreur}, + /// title = {On-the-fly Verification of Temporal Logic}, + /// pages = {253--271}, + /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, + /// booktitle = {Proceedings of the World Congress on Formal Methods in + /// the Development of Computing Systems (FM'99)}, + /// publisher = {Springer-Verlag}, + /// series = {Lecture Notes in Computer Science}, + /// volume = {1708}, + /// year = {1999}, + /// address = {Toulouse, France}, + /// month = {September}, + /// isbn = {3-540-66587-0} + /// } + /// \endverbatim + /// + /// check() returns true if the automaton's language is empty. When + /// it return false, a stack of SCC has been built is available + /// using result() (spot::counter_example needs it). + /// + /// There are two variants of this algorithm: spot::emptiness_check and + /// spot::emptiness_check_shy. They differ in their memory usage, the + /// number for successors computed before they are used and the way + /// the depth first search is directed. + /// + /// spot::emptiness_check performs a straightforward depth first search. + /// The DFS stacks store tgba_succ_iterators, so that only the + /// iterators which really are explored are computed. + /// + /// spot::emptiness_check_shy try to explore successors which are + /// visited states first. this helps to merge SCCs and generally + /// helps to produce shorter counter-examples. However this + /// algorithm cannot stores unprocessed successors as + /// tgba_succ_iterators: it must compute all successors of a state + /// at once in order to decide which to explore first, and must keep + /// a list of all unexplored successors in its DFS stack. + class emptiness_check + { + public: + emptiness_check(const tgba* a); + virtual ~emptiness_check(); + + /// Check whether the automaton's language is empty. + virtual bool check(); + + /// \brief Return the status of the emptiness-check. + /// + /// When check() succeed, the status should be passed along + /// to spot::counter_example. + /// + /// This status should not be deleted, it is a pointer + /// to a member of this class that will be deleted when + /// the emptiness_check object is deleted. + const emptiness_check_status* result() const; + + protected: + emptiness_check_status* ecs_; + /// \brief Remove a strongly component from the hash. + /// + /// This function remove all accessible state from a given + /// state. In other words, it removes the strongly connected + /// component that contains this state. + void remove_component(const state* start_delete); + }; + + /// \brief A version of spot::emptiness_check try to visit known + /// states first. + /// + /// See the documentation for spot::emptiness_check + class emptiness_check_shy : public emptiness_check + { + public: + emptiness_check_shy(const tgba* a); + virtual ~emptiness_check_shy(); + + virtual bool check(); + }; + +} + +#endif // SPOT_TGBAALGOS_GTEC_GTEC_HH diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc new file mode 100644 index 000000000..0e5c1e062 --- /dev/null +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -0,0 +1,133 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "nsheap.hh" + +namespace spot +{ + class numbered_state_heap_hash_map_const_iterator : + public numbered_state_heap_const_iterator + { + public: + numbered_state_heap_hash_map_const_iterator + (const numbered_state_heap_hash_map::hash_type& h) + : numbered_state_heap_const_iterator(), h(h) + { + } + + ~numbered_state_heap_hash_map_const_iterator() + { + } + + virtual void + first() + { + i = h.begin(); + } + + virtual void + next() + { + ++i; + } + + virtual bool + done() const + { + return i == h.end(); + } + + virtual const state* + get_state() const + { + return i->first; + } + + virtual int + get_index() const + { + return i->second; + } + + private: + numbered_state_heap_hash_map::hash_type::const_iterator i; + const numbered_state_heap_hash_map::hash_type& h; + }; + + numbered_state_heap_hash_map::~numbered_state_heap_hash_map() + { + // Free keys in H. + hash_type::iterator i = h.begin(); + while (i != h.end()) + { + // Advance the iterator before deleting the key. + const state* s = i->first; + ++i; + delete s; + } + } + + const int* + numbered_state_heap_hash_map::find(const state* s) const + { + hash_type::const_iterator i = h.find(s); + if (i == h.end()) + return 0; + return &i->second; + } + + int* + numbered_state_heap_hash_map::find(const state* s) + { + hash_type::iterator i = h.find(s); + if (i == h.end()) + return 0; + return &i->second; + } + + void + numbered_state_heap_hash_map::insert(const state* s, int index) + { + h[s] = index; + } + + int + numbered_state_heap_hash_map::size() const + { + return h.size(); + } + + numbered_state_heap_const_iterator* + numbered_state_heap_hash_map::iterator() const + { + return new numbered_state_heap_hash_map_const_iterator(h); + } + + const state* + numbered_state_heap_hash_map::filter(const state* s) const + { + hash_type::const_iterator i = h.find(s); + assert(i != h.end()); + if (s != i->first) + delete s; + return i->first; + } +} diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh new file mode 100644 index 000000000..408074da5 --- /dev/null +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -0,0 +1,108 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_NSHEAP_HH +# define SPOT_TGBAALGOS_GTEC_NSHEAP_HH + +#include "tgba/state.hh" +#include "misc/hash.hh" + +namespace spot +{ + /// Iterator on numbered_state_heap objects. + class numbered_state_heap_const_iterator + { + public: + virtual ~numbered_state_heap_const_iterator() {} + + //@{ + /// Iteration + virtual void first() = 0; + virtual void next() = 0; + virtual bool done() const = 0; + //@} + + //@{ + /// Inspection + virtual const state* get_state() const = 0; + virtual int get_index() const = 0; + //@} + }; + + /// Keep track of a large quantity of indexed states. + class numbered_state_heap + { + public: + virtual ~numbered_state_heap() {} + //@{ + /// \brief Is state in the heap? + /// + /// Returns 0 if \a s is not in the heap. or a pointer to + /// its number if it is. + virtual const int* find(const state* s) const = 0; + virtual int* find(const state* s) = 0; + //@} + + /// Add a new state \a s with index \a index + virtual void insert(const state* s, int index) = 0; + + /// The number of stored states. + virtual int size() const = 0; + + /// Return an iterator on the states/indexes pairs. + virtual numbered_state_heap_const_iterator* iterator() const = 0; + + /// \brief Filter state clones. + /// + /// Return a state which is equal to \a s, but is an actual key in + /// the heap, and free \a s if it is a clone of that state. + /// + /// Doing so simplify memory management, because we don't have to + /// track which state need to be kept or deallocated: all key in + /// the heap should last for the whole life of the emptiness-check. + virtual const state* filter(const state* s) const = 0; + }; + + /// A straightforward implementation of numbered_state_heap with a hash map. + class numbered_state_heap_hash_map : public numbered_state_heap + { + public: + virtual ~numbered_state_heap_hash_map(); + + virtual const int* find(const state* s) const; + virtual int* find(const state* s); + virtual void insert(const state* s, int index); + virtual int size() const; + + virtual numbered_state_heap_const_iterator* iterator() const; + + virtual const state* filter(const state* s) const; + + protected: + typedef Sgi::hash_map hash_type; + hash_type h; ///< Map of visited states. + + friend class numbered_state_heap_hash_map_const_iterator; + }; +} + +#endif // SPOT_TGBAALGOS_GTEC_NSHEAP_HH diff --git a/src/tgbaalgos/gtec/sccstack.cc b/src/tgbaalgos/gtec/sccstack.cc new file mode 100644 index 000000000..6a26d8a6e --- /dev/null +++ b/src/tgbaalgos/gtec/sccstack.cc @@ -0,0 +1,61 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "sccstack.hh" + +namespace spot +{ + 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(); + } +} diff --git a/src/tgbaalgos/gtec/sccstack.hh b/src/tgbaalgos/gtec/sccstack.hh new file mode 100644 index 000000000..1d8708365 --- /dev/null +++ b/src/tgbaalgos/gtec/sccstack.hh @@ -0,0 +1,67 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_SCCSTACK_HH +# define SPOT_TGBAALGOS_GTEC_SCCSTACK_HH + +#include +#include + +namespace spot +{ + // A stack of Strongly-Connected Components, as needed by the + // Tarjan-Couvreur algorithm. + class scc_stack + { + public: + struct connected_component + { + public: + connected_component(int index = -1); + + /// Index of the SCC. + int index; + /// The bdd condition is the union of all acceptance conditions of + /// transitions which connect the states of the connected component. + bdd condition; + }; + + /// Stack a new SCC with index \a index. + void push(int index); + + /// Access the top SCC. + connected_component& top(); + + /// Pop the top SCC. + void pop(); + + /// How many SCC are in stack. + size_t size() const; + + /// Is the stack empty? + bool empty() const; + + typedef std::stack stack_type; + stack_type s; + }; +} + +#endif // SPOT_TGBAALGOS_GTEC_SCCSTACK_HH diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc new file mode 100644 index 000000000..49783139c --- /dev/null +++ b/src/tgbaalgos/gtec/status.cc @@ -0,0 +1,43 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "status.hh" + +namespace spot +{ + emptiness_check_status::emptiness_check_status(const tgba* aut) + : aut(aut) + { + } + + emptiness_check_status::~emptiness_check_status() + { + } + + void + emptiness_check_status::print_stats(std::ostream& os) const + { + os << h.size() << " unique states visited" << std::endl; + os << root.size() + << " strongly connected components in search stack" + << std::endl; + } +} diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh new file mode 100644 index 000000000..9b0f79256 --- /dev/null +++ b/src/tgbaalgos/gtec/status.hh @@ -0,0 +1,53 @@ +// Copyright (C) 2004 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. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_GTEC_STATUS_HH +# define SPOT_TGBAALGOS_GTEC_STATUS_HH + +#include "sccstack.hh" +#include "nsheap.hh" +#include "tgba/tgba.hh" +#include + +namespace spot +{ + /// \brief The status of the emptiness-check on success. + /// + /// This contains everything needed to construct a counter-example: + /// the automata, the stack of SCCs traversed by the counter-example, + /// and the heap of visited states with their indexes. + class emptiness_check_status + { + public: + emptiness_check_status(const tgba* aut); + ~emptiness_check_status(); + + const tgba* aut; + scc_stack root; + numbered_state_heap_hash_map h; ///< Map of visited states. + + /// Output statistics about this object. + void print_stats(std::ostream& os) const; + }; + +} + +#endif // SPOT_TGBAALGOS_GTEC_STATUS_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index f3eab4d64..8c28e0bb3 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -33,7 +33,8 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgbaalgos/magic.hh" -#include "tgbaalgos/emptinesscheck.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/gtec/ce.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh"