diff --git a/ChangeLog b/ChangeLog index 70d4faa10..fe725e466 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2004-10-15 Alexandre Duret-Lutz + + Back out all Thomas's changes on emptiness checks since + 2004-08-23. Some of these will need to be reintegrated more + slowly and cleanly. + + * src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc, + src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am, + src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert. + * src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh, + src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh, + src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh, + src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh, + src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh: + Delete. + 2004-10-14 Alexandre Duret-Lutz * src/ltltest/reduc.test: Do source ./defs. Revert mistaken diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 49b1b0ff4..3ddabb01d 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -27,43 +27,33 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ - colordfs.hh \ dotty.hh \ dupexp.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ - minimalce.hh \ - nesteddfs.hh \ - nesteddfsgen.hh \ neverclaim.hh \ powerset.hh \ reachiter.hh \ save.hh \ stats.hh \ - reductgba_sim.hh \ - tarjan_on_fly.hh + reductgba_sim.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ - colordfs.cc \ dotty.cc \ dupexp.cc \ lbtt.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ - minimalce.cc \ - nesteddfs.cc \ - nesteddfsgen.cc \ neverclaim.cc \ powerset.cc \ reachiter.cc \ save.cc \ stats.cc \ reductgba_sim.cc \ - reductgba_sim_del.cc \ - tarjan_on_fly.cc + reductgba_sim_del.cc libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/colordfs.cc b/src/tgbaalgos/colordfs.cc deleted file mode 100644 index e953640c5..000000000 --- a/src/tgbaalgos/colordfs.cc +++ /dev/null @@ -1,435 +0,0 @@ -// 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 -#include -#include "colordfs.hh" -#include "tgba/bddprint.hh" - -namespace spot -{ - - colordfs_search::colordfs_search(const tgba_tba_proxy* a) - : a(a), x(0), counter_(0) - { - Maxdepth = -1; - } - - colordfs_search::~colordfs_search() - { - hash_type::const_iterator s = h.begin(); - while (s != h.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - delete ptr; - } - if (x) - delete x; - // Release all iterators on the stack. - while (!stack.empty()) - { - delete stack.front().second; - stack.pop_front(); - } - } - - bool - colordfs_search::push(const state* s, color c) - { - tgba_succ_iterator* i = a->succ_iter(s); - i->first(); - - /* - hash_type::iterator hi = h.find(s); - if (hi != h.end()) - if (hi->second.depth <= (int)stack.size()) - //return false; // FIXME - return true; - */ - - color_state cs = { c, true , stack.size() }; // FIXME - h[s] = cs; - - stack.push_front(state_iter_pair(s, i)); - - // We build the counter example - bdd b = bddfalse; - if (!i->done()) // if the state is dead. - b = i->current_condition(); - counter_->prefix.push_back(ce::state_ce(s->clone(), b)); - - return true; - } - - void - colordfs_search::pop() - { - const state* s = stack.begin()->first; - tgba_succ_iterator* i = stack.begin()->second; - delete i; - - //std::cout << "pop : " << a->format_state(s) << std::endl; - - hash_type::iterator hi = h.find(s); - assert(hi != h.end()); - hi->second.is_in_cp = false; - stack.pop_front(); - //delete s; - - // We build the counter example - delete counter_->prefix.back().first; - counter_->prefix.pop_back(); - } - - bool - colordfs_search::all_succ_black(const state* s) - { - bool return_value = true; - hash_type::iterator hi; - - const state* s2; - tgba_succ_iterator* i = a->succ_iter(s); - int n = 0; - for (i->first(); !i->done(); i->next(), n++) - { - s2 = i->current_state(); - hi = h.find(s2); - if (hi != h.end()) - return_value &= (hi->second.c == black); - else - return_value = false; - delete s2; - } - delete i; - - hi = h.find(s); - assert(hi != h.end()); - if (return_value) - hi->second.c = black; - - return return_value; - } - - ce::counter_example* - colordfs_search::check() - { - clock(); - counter_ = new ce::counter_example(a); - const state *s = a->get_init_state(); - if (dfs_blue_min(s)) - counter_->build_cycle(x); - else - { - delete counter_; - counter_ = 0; - } - tps_ = clock(); - - return counter_; - } - - bool - colordfs_search::dfs_blue(const state* s, bdd) - { - std::cout << "dfs_blue : " << std::endl; - - if (stack.empty()) - // It's a new search. - push(a->get_init_state(), blue); - else - tstack.pop_front(); - - while (!stack.empty()) - { - recurse: - tgba_succ_iterator *i = stack.front().second; - hash_type::iterator hi; - - //std::cout << a->format_state(p.first) << std::endl; - while (!i->done()) - { - const state* s2 = i->current_state(); - hi = h.find(s2); - if (a->state_is_accepting(s2) && - (hi != h.end() && hi->second.is_in_cp)) - { - //ce::state_ce ce; - //ce = ce::state_ce(s2, i->current_condition()); - x = const_cast(s2); - //push(s2, blue); // - //delete i; - return true;// a counter example is found !! - } - else if (hi == h.end() || hi->second.c == white) - { - push(s2, blue); - goto recurse; - } - else - delete s2; - i->next(); - } - - s = stack.front().first; - pop(); - - if (!all_succ_black(s) && - a->state_is_accepting(s)) - { - if (dfs_red(s)) - return true; - - hash_type::iterator hi = h.find(s); - assert(hi == h.end()); - hi->second.c = black; - } - - delete s; // - } - - return false; - } - - bool - colordfs_search::dfs_red(const state* s) - { - std::cout << "dfs_red : " << a->format_state(s) << std::endl; - if (!push(s, red)) - return false; - - hash_type::iterator hi; - tgba_succ_iterator* i = a->succ_iter(s); - int n = 0; - for (i->first(); !i->done(); i->next(), n++) - { - const state* s2 = i->current_state(); - hi = h.find(s2); - if (hi != h.end() && hi->second.is_in_cp && - (a->state_is_accepting(s2) || - (hi->second.c == blue))) - { - //ce::state_ce ce; - //ce = ce::state_ce(s2->clone(), i->current_condition()); - x = const_cast(s2); - delete i; - return true;// a counter example is found !! - } - if (hi != h.end() && hi->second.c == blue) - { - delete s2; // FIXME - if (dfs_red(hi->first)) - { - delete i; - return true; - } - } - else - delete s2; - } - delete i; - - hi = h.find(s); - assert(hi == h.end()); - hi->second.c = black; - //std::cout << "dfs_red : pop" << std::endl; - pop(); - - return false; - } - - /////////////////////////////////////////////////////////////////////// - // for minimisation - - bool - colordfs_search::dfs_blue_min(const state* s, bdd) - { - //std::cout << "dfs_blue : " << a->format_state(s) << std::endl; - if (!push(s, blue)) - return false; - - hash_type::iterator hi = h.find(s); - if (hi != h.end()) - { - if (((int)stack.size() + 1) < hi->second.depth) - hi->second.depth = stack.size(); // for minimize - } - else - { - assert(0); - } - - if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth)) - { - tgba_succ_iterator* i = a->succ_iter(s); - int n = 0; - for (i->first(); !i->done(); i->next(), n++) - { - const state* s2 = i->current_state(); - //std::cout << "s2 : " << a->format_state(s2) << std::endl; - hi = h.find(s2); - - if (a->state_is_accepting(s2) && - (hi != h.end() && hi->second.is_in_cp)) - { - Maxdepth = stack.size(); - ce::state_ce ce; - ce = ce::state_ce(s2, i->current_condition()); - x = const_cast(s2); - delete i; - return true;// a counter example is found !! - } - else if (hi == h.end() || hi->second.c == white) - { - int res = dfs_blue_min(s2, i->current_acceptance_conditions()); - if (res == 1) - { - delete i; - return true; - } - } - else - delete s2; // FIXME - } - delete i; - - - pop(); - - if (!all_succ_black(s) && - a->state_is_accepting(s)) - { - if (dfs_red_min(s)) - return 1; - dfs_black(s); - } - } - - return false; - } - - bool - colordfs_search::dfs_red_min(const state* s) - { - //std::cout << "dfs_red : " << a->format_state(s) << std::endl; - if (!push(s, red)) - return false; - - hash_type::iterator hi = h.find(s); - if (hi != h.end()) - { - if (((int)stack.size() + 1) < hi->second.depth) - hi->second.depth = stack.size(); // for minimize - } - else - assert(0); - - if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth)) - { - tgba_succ_iterator* i = a->succ_iter(s); - int n = 0; - for (i->first(); !i->done(); i->next(), n++) - { - const state* s2 = i->current_state(); - hi = h.find(s2); - if (hi != h.end() && hi->second.is_in_cp && - (a->state_is_accepting(s2) || - (hi->second.c == blue))) - { - Maxdepth = stack.size(); - ce::state_ce ce; - ce = ce::state_ce(s2->clone(), i->current_condition()); - x = const_cast(s2); - delete i; - return true;// a counter example is found !! - } - if (hi != h.end() && - (hi->second.c == blue)) - // || ((int)stack.size() + 1) < hi->second.depth)) - { - delete s2; // FIXME - if (dfs_red_min(hi->first)) - { - delete i; - return true; - } - } - else - delete s2; - } - delete i; - - //std::cout << "dfs_red : pop" << std::endl; - pop(); - } - return false; - } - - - void - colordfs_search::dfs_black(const state* s) - { - //std::cout << "dfs_black" << a->format_state(s) << std::endl; - hash_type::iterator hi = h.find(s); - if (hi == h.end()) // impossible - { - color_state cs = { black, false, stack.size() }; - h[s] = cs; - } - else - hi->second.c = black; - - tgba_succ_iterator* i = a->succ_iter(s); - for (i->first(); !i->done(); i->next()) - { - const state* s2 = i->current_state(); - hi = h.find(s2); - if (hi == h.end()) - { - color_state cs = { black, false, stack.size() }; - h[s2] = cs; - dfs_black(s2); - } - else - { - delete s2; - if (hi->second.c != black) - dfs_black(hi->first); - } - } - delete i; - - } - - std::ostream& - colordfs_search::print_stat(std::ostream& os) const - { - int ce_size = 0; - if (counter_) - ce_size = counter_->size(); - os << "Size of Counter Example : " << ce_size << std::endl - << "States explored : " << h.size() << std::endl - << "Computed time : " << tps_ << " microseconds" << std::endl; - return os; - } - -} diff --git a/src/tgbaalgos/colordfs.hh b/src/tgbaalgos/colordfs.hh deleted file mode 100644 index fde1f81b1..000000000 --- a/src/tgbaalgos/colordfs.hh +++ /dev/null @@ -1,124 +0,0 @@ -// 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_COLORDFS_HH -# define SPOT_TGBAALGOS_COLORDFS_HH - -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" -#include "tgbaalgos/minimalce.hh" - -namespace spot -{ - class colordfs_search: public emptiness_search - { - public: - /// Initialize the Colordfs Search algorithm on the automaton \a a. - colordfs_search(const tgba_tba_proxy *a); - - virtual ~colordfs_search(); - - /// \brief Perform a Color DFS Search. - /// - /// \return a new accepting path if there exists one, NULL otherwise. - /// - /// check() can be called several times until it return false, - /// to enumerate all accepting paths. - virtual ce::counter_example* check(); - - /// \brief Print Stat. - std::ostream& print_stat(std::ostream& os) const; - - private: - - // The names "stack", "h", and "x", are those used in the paper. - - /// \brief Records the color of a state. - enum color - { - white = 0, - blue = 1, - red = 2, - black = 3 - }; - - struct color_state - { - color c; - bool is_in_cp; - int depth; - }; - - typedef std::pair state_iter_pair; - typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - typedef std::list tstack_type; - /// \brief Stack of transitions. - /// - /// This is an addition to the data from the paper. - tstack_type tstack; - - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - /// The three dfs as explain in - /// @InProceedings(GaMoZe04spin, - /// Author = "Gastin, P. and Moro, P. and Zeitoun, M.", - /// Title = "Minimization of counterexamples in {SPIN}", - /// BookTitle = "Proceedings of the 11th SPIN Workshop (SPIN'04)", - /// Editor = "Graf, S. and Mounier, L.", - /// Publisher = SPRINGER, - /// Series = LNCS, - /// Number = 2989, - /// Year = 2004, - /// Pages = "92-108") - bool dfs_blue(const state* s, bdd acc = bddfalse); - bool dfs_red(const state* s); - bool dfs_blue_min(const state* s, bdd acc = bddfalse); - bool dfs_red_min(const state* s); - void dfs_black(const state* s); - - /// Append a new state to the current path. - bool push(const state* s, color c); - /// Remove a state to the current path. - void pop(); - /// Check if all successors of \a s are black and color - /// \a s in black if true. - bool all_succ_black(const state* s); - - const tgba_tba_proxy* a; ///< The automata to check. - /// The state for which we are currently seeking an SCC. - const state* x; - int Maxdepth; ///< The size of the current counter example. - - ce::counter_example* counter_; - clock_t tps_; - }; - - -} - -#endif // SPOT_TGBAALGOS_COLORDFS_HH diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 1d54dbe92..dac2f2415 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -35,11 +35,6 @@ namespace spot eccf) : ecs_(ecs) { - - std::cout << "counter_example" << std::endl; - - //counter_ = new ce::counter_example(ecs->aut); - assert(!ecs_->root.empty()); assert(suffix.empty()); @@ -81,10 +76,6 @@ namespace spot assert(spi.first); suffix.push_front(spi.first); - ///// - // counter_->prefix.push_front(ce::state_ce(spi.first->clone(), bddfalse)); - //// - // 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 @@ -122,36 +113,21 @@ namespace spot const state* h_dest = scc[k]->has_state(dest); if (!h_dest) { - // If we have found a state in greater SCC which. + // 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; - /// - // ce::l_state_ce seq_count; - /// - seq.push_front(h_dest); while (src->compare(start)) { - /// - // seq_count.push_front(ce::state_ce(src->clone(), - // bddfalse)); - /// - seq.push_front(src); src = father[src]; } // Append SEQ to SUFFIX. suffix.splice(suffix.end(), seq); - - /// - // counter_->prefix.splice(counter_->prefix.end(), - // seq_count); - /// - // Exit this BFS for this SCC. while (!todo.empty()) { @@ -190,8 +166,6 @@ namespace spot const state* from, const state* to) { - //std::cout << "complete_cycle" << std::endl; - // If by change or period already ends on the state we have // to reach back, we are done. if (from == to @@ -237,28 +211,14 @@ namespace spot if (h_dest == to) { cycle_path p; - - /// - // ce::l_state_ce p_counter; - // p_counter.push_front(ce::state_ce(h_dest->clone(), cond)); - /// - p.push_front(state_proposition(h_dest, cond)); while (src != from) { const state_proposition& psi = father[src]; - /// - // p_counter.push_front(ce::state_ce(src->clone(), - // psi.second)); - /// p.push_front(state_proposition(src, psi.second)); src = psi.first; } period.splice(period.end(), p); - /// - // counter_->cycle.splice(counter_->cycle.end(), - // p_counter); - /// // Exit the BFS, but release all iterators first. while (!todo.empty()) @@ -296,9 +256,6 @@ namespace spot } - //////////////////////////////////////////////////////////////////////// - /* - void counter_example::accepting_path(const explicit_connected_component* scc, const state* start, bdd acc_to_traverse) @@ -338,9 +295,9 @@ namespace spot todo.pop(); delete iter; seen.erase(s); - if (!todo.empty()) + if (todo.size()) { - assert(!path.empty()); + assert(path.size()); path.pop_back(); } continue; @@ -377,7 +334,7 @@ namespace spot // If we already have a best path, let see if the current // one is better. - if (!best_path.empty()) + if (best_path.size()) { // When comparing the merits of two paths, only the // acceptance conditions we are trying the traverse @@ -423,12 +380,7 @@ namespace spot // Append our best path to the period. for (cycle_path::iterator it = best_path.begin(); it != best_path.end(); ++it) - { - period.push_back(*it); - ce::state_ce ce(it->first, it->second); - counter_->cycle.push_back(ce); - counter_->cycle.push_back(*it); - } + period.push_back(*it); // Prepare to find another path for the remaining acceptance // conditions. @@ -441,161 +393,6 @@ namespace spot complete_cycle(scc, start, suffix.back()); } - */ - //////////////////////////////////////////////////////////////////////// - - void - counter_example::accepting_path(const explicit_connected_component* scc, - const state* start, bdd acc_to_traverse) - { - //std::cout << "accepting_path" << std::endl; - - // State seen during the DFS. - typedef Sgi::hash_set set_type; - set_type seen; - // DFS stack. - std::stack todo; - - while (acc_to_traverse != bddfalse) - { - //std::cout << "accepting_path : while (acc_to_traverse != bddfalse)" - // << std::endl; - - // 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()) - { - // std::cout << "accepting_path : while (!todo.empty())" - // << std::endl; - - 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.empty()) - { - assert(!path.empty()); - 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.empty()) - { - // 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); - //ce::state_ce ce(it->first->clone(), it->second); - //counter_->cycle.push_back(ce); - //counter_->cycle.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 { @@ -647,10 +444,4 @@ namespace spot os << period.size() << " states in period" << std::endl; } - ce::counter_example* - counter_example::get_counter_example() const - { - return counter_; - } - } diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index a5816bf94..f541e3522 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -25,8 +25,6 @@ #include "status.hh" #include "explscc.hh" -#include "tgbaalgos/minimalce.hh" - namespace spot { /// Compute a counter example from a spot::emptiness_check_status @@ -53,8 +51,6 @@ namespace spot /// Output statistics about this object. void print_stats(std::ostream& os) const; - ce::counter_example* get_counter_example() const; - protected: /// Called by counter_example to find a path which traverses all /// acceptance conditions in the accepted SCC. @@ -68,7 +64,6 @@ namespace spot private: const emptiness_check_status* ecs_; - ce::counter_example* counter_; }; } diff --git a/src/tgbaalgos/minimalce.cc b/src/tgbaalgos/minimalce.cc deleted file mode 100644 index 06e781711..000000000 --- a/src/tgbaalgos/minimalce.cc +++ /dev/null @@ -1,1006 +0,0 @@ -// 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 "tgbaalgos/minimalce.hh" -#include "tgba/tgbaexplicit.hh" - -namespace spot -{ - - /////////////////////////////////////////////////////////////////////////// - // Class counter example. - - namespace ce - { - - counter_example::counter_example(const tgba* a) - : automata_(a) - { - } - - counter_example::~counter_example() - { - for (l_state_ce::const_iterator i = prefix.begin(); - i != prefix.end(); ++i) - { - delete i->first; - } - for (l_state_ce::const_iterator i = cycle.begin(); - i != cycle.end(); ++i) - { - delete i->first; - } - } - - void - counter_example::build_cycle(const state* x) - { - if (!x) - return; - bool in_cycle = false; - for (l_state_ce::iterator i = prefix.begin(); - i != prefix.end();) - { - if (i->first->compare(x) == 0) - in_cycle = true; - if (in_cycle) - { - cycle.push_back(*i); - i = prefix.erase(i); - } - else - ++i; - } - } - - int - counter_example::size() - { - return prefix.size() + cycle.size(); - } - - std::ostream& - counter_example::print(std::ostream& os) const - { - os << "Prefix:" << std::endl; - const bdd_dict* d = automata_->get_dict(); - for (l_state_ce::const_iterator i = prefix.begin(); - i != prefix.end(); ++i) - { - os << " " << automata_->format_state(i->first) << std::endl; - os << " | " << bdd_format_set(d, i->second) << std::endl; - } - os <<"Cycle:" <format_state(i->first) << std::endl; - os << " | " << bdd_format_set(d, i->second) << std::endl; - } - return os; - } - - bdd_dict* - counter_example::get_dict() const - { - return automata_->get_dict(); - } - - void - counter_example::project_ce(const tgba* aut, std::ostream& os) - { - os << "prefix :" << std::endl; - for (ce::l_state_ce::const_iterator i = prefix.begin(); - i != prefix.end(); ++i) - { - const state* s = aut->project_state(i->first, aut); - assert(s); - os << aut->format_state(s) << std::endl; - delete s; - } - - os << "cycle :" << std::endl; - for (ce::l_state_ce::const_iterator i = cycle.begin(); - i != cycle.end(); ++i) - { - const state* s = aut->project_state(i->first, aut); - assert(s); - os << aut->format_state(s) << std::endl; - delete s; - } - - } - - tgba* - counter_example::ce2tgba() - { - - tgba_explicit* aut = new tgba_explicit(automata_->get_dict()); - - std::string strs, strd; - tgba_explicit::transition* t; - ce::l_state_ce::const_iterator is = prefix.begin(); - ce::l_state_ce::const_iterator id = is; - //ce::l_state_ce::const_iterator is_c; - //ce::l_state_ce::const_iterator id_c; - if (is != prefix.end()) - { - strs = automata_->format_state(is->first); - aut->set_init_state(strs); - ++id; - - for (; id != prefix.end(); ++is, ++id) - { - strs = automata_->format_state(is->first); - strd = automata_->format_state(id->first); - t = aut->create_transition(strs, strd); - aut->add_conditions(t, is->second); - } - - id = cycle.begin(); - } - else - { - id = cycle.begin(); - is = id; - ++id; - } - - for (; id != cycle.end();) - { - strs = automata_->format_state(is->first); - strd = automata_->format_state(id->first); - t = aut->create_transition(strs, strd); - aut->add_conditions(t, is->second); - is = id; - ++id; - } - - assert(!cycle.empty()); - is = cycle.end(); - --is; - id = cycle.begin(); - strs = automata_->format_state(is->first); - strd = automata_->format_state(id->first); - t = aut->create_transition(strs, strd); - aut->add_conditions(t, is->second); - - aut->merge_transitions(); - - return aut; - } - - } - - ///////////////////////////////////////////////////////////////////////////// - // The base interface for build a emptiness search algorithm - emptiness_search::emptiness_search() - { - } - - emptiness_search::~emptiness_search() - { - } - - /* - std::ostream& - nesteddfs_search::print_stat(std::ostream& os) const - { - int ce_size = 0; - if (counter_) - ce_size = counter_->size(); - os << "Size of Counter Example : " << ce_size << std::endl - os << "States explored : " << size_ << std::endl - << "Computed time : " << tps_ << " microseconds" << std::endl; - return os; - } - */ - - std::ostream& - emptiness_search::print_stat(std::ostream& os) const - { - return os; - } - - ///////////////////////////////////////////////////////////////////////////// - // minimal_search - - /////////////////////////////////////////////////////////////////// - /////////////////////////////////////////////////////////////////// - - minimalce_search::minimalce_search(const tgba_tba_proxy* a, - int opt) - : a(a), x(0), - x_bis(0), - accepted_path_(false) - { - counter_ = 0; - nested_ = my_nested_ = false; - if (opt == nested) - nested_ = true; - if (opt == my_nested) - my_nested_ = true; - Maxsize = 0; - } - - minimalce_search::~minimalce_search() - { - hash_type::const_iterator s = h.begin(); - while (s != h.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - delete ptr; - } - if (x) - delete x; - // Release all iterators on the stack. - while (!stack.empty()) - { - delete stack.front().second; - stack.pop_front(); - } - for (std::list::iterator i = l_ce.begin(); - i != l_ce.end(); ++i) - { - delete *i; - } - } - - - bool - minimalce_search::push(const state* s, bool m) - { - if ((Maxsize != 0) && // for minimize - (stack.size() + 1 > Maxsize)) - return false; - - tgba_succ_iterator* i = a->succ_iter(s); - i->first(); - - hash_type::iterator hi = h.find(s); - if (hi == h.end()) - { - magic d = { !m, m, true, stack.size() + 1}; - //magic d = { !m, m, true }; - h[s] = d; - } - else - { - hi->second.seen_without |= !m; - hi->second.seen_with |= m; - hi->second.seen_path = true; // for nested search - - if ((stack.size() + 1) < hi->second.depth) // for minimize - hi->second.depth = stack.size() + 1; - - if (hi->first != s) - delete s; - s = hi->first; - } - - magic_state ms = { s, m }; - stack.push_front(state_iter_pair(ms, i)); - - return true; - } - - bool - minimalce_search::has(const state* s, bool m) const - { - hash_type::const_iterator i = h.find(s); - if (i == h.end()) - return false; - if (!m && i->second.seen_without) - return true; - if (m && i->second.seen_with) - return true; - return false; - } - - bool - minimalce_search::exist_path(const state* s) const - { - hash_type::const_iterator hi = h.find(s); - if (hi == h.end()) - return false; - if (hi->second.seen_with) - return false; - return hi->second.seen_path && hi->second.seen_without; - } - - int - minimalce_search::depth_path(const state* s) const - { - int depth = 0; - stack_type::const_reverse_iterator i; - for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth) - if (s->compare(i->first.s) == 0) - break; - - if (i != stack.rend()) - return depth; - else - return stack.size() + 1; - } - - ce::counter_example* - minimalce_search::check() - { - if (my_nested_) - { - accepted_path_ = false; - accepted_depth_ = 0; - } - - if (stack.empty()) - // It's a new search. - push(a->get_init_state(), false); - else - // Remove the transition to the cycle root. - tstack.pop_front(); - - assert(stack.size() == 1 + tstack.size()); - - while (!stack.empty()) - { - recurse: - //std::cout << "recurse : "<< stack.size() << std::endl; - minimalce_search::state_iter_pair& p = stack.front(); - tgba_succ_iterator* i = p.second; - const bool magic = p.first.m; - - while (!i->done()) - { - const state* s_prime = i->current_state(); - //std::cout << a->format_state(s_prime) << std::endl; - bdd c = i->current_condition(); - i->next(); - - if ((magic && 0 == s_prime->compare(x)) || - (magic && (nested_ || my_nested_) && exist_path(s_prime)) || - (!magic && my_nested_ && accepted_path_ && - exist_path(s_prime) && depth_path(s_prime) <= accepted_path_)) - { - if (nested_ || my_nested) - { - if (x) - delete x; - x = s_prime->clone(); - } - delete s_prime; - tstack.push_front(c); - assert(stack.size() == tstack.size()); - - build_counter(); - Maxsize = stack.size(); - counter_->build_cycle(x); - return counter_; - } - if (!has(s_prime, magic)) - { - if (my_nested_ && a->state_is_accepting(s_prime)) - { - accepted_path_ = true; - accepted_depth_ = stack.size(); - } - if (push(s_prime, magic)) - { - tstack.push_front(c); - goto recurse; - } - // for minimize - } - delete s_prime; - } - - const state* s = p.first.s; - delete i; - if (nested_ || my_nested_) - { - hash_type::iterator hi = h.find(((stack.front()).first).s); - assert (hi != h.end()); - hi->second.seen_path = false; - } - stack.pop_front(); - - if (!magic && a->state_is_accepting(s)) - { - if (!has(s, true)) - { - if (x) - delete x; - x = s->clone(); - push(s, true); - continue; - } - } - if (!stack.empty()) - tstack.pop_front(); - } - - std::cout << "END CHECK" << std::endl; - - assert(tstack.empty()); - - return 0; - } - - std::ostream& - minimalce_search::print_result(std::ostream& os, const tgba* restrict) const - { - stack_type::const_reverse_iterator i; - tstack_type::const_reverse_iterator ti; - os << "Prefix:" << std::endl; - const bdd_dict* d = a->get_dict(); - for (i = stack.rbegin(), ti = tstack.rbegin(); - i != stack.rend(); ++i, ++ti) - { - if (i->first.s->compare(x) == 0) - os <<"Cycle:" <first.s; - if (restrict) - { - s = a->project_state(s, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << " " << a->format_state(s) << std::endl; - } - os << " | " << bdd_format_set(d, *ti) << std::endl; - } - - if (restrict) - { - const state* s = a->project_state(x, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - - } - else - { - os << " " << a->format_state(x) << std::endl; - } - return os; - } - - std::ostream& - minimalce_search::print_stat(std::ostream& os) const - { - int ce_size = 0; - if (counter_) - ce_size = counter_->size(); - os << "Size of Counter Example : " << ce_size << std::endl - << "States explored : " << h.size() << std::endl; - return os; - } - - void - minimalce_search::build_counter() - { - if (counter_) - l_ce.push_front(counter_); - assert(stack.size() == tstack.size()); - counter_ = new ce::counter_example(a); - stack_type::reverse_iterator i; - tstack_type::reverse_iterator ti; - for (i = stack.rbegin(), ti = tstack.rbegin(); - i != stack.rend(); ++i, ++ti) - { - if (i->first.s->compare(x) == 0) - break; - ce::state_ce ce; - ce = ce::state_ce(i->first.s->clone(), *ti); - counter_->prefix.push_back(ce); - } - for (; i != stack.rend(); ++i, ++ti) - { - ce::state_ce ce; - ce = ce::state_ce(i->first.s->clone(), *ti); - counter_->cycle.push_back(ce); - } - //counter_->build_cycle(x); - } - - /////////////////////////////////////////////////////////////////// - /////////////////////////////////////////////////////////////////// - /* - minimalce_search::minimalce_search(const tgba_tba_proxy *a, - bool mode) - : a(a), min_ce(0), - x(0), - x_bis(0), - accepted_path_(false) - { - Maxsize = 0; - nested_ = my_nested_ = false; - mode_ = mode; - } - - minimalce_search::~minimalce_search() - { - hash_type::const_iterator s = h_lenght.begin(); - while (s != h_lenght.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - delete ptr; - } - - for (std::list::iterator i = l_ce.begin(); - i != l_ce.end();) - { - //std::cout << "delete a counter" << std::endl; - - //if (*i == min_ce) - //{ - //++i; - //continue; - //} - - ce::counter_example* ce = *i; - ++i; - delete ce; - } - - //std::cout << "END ~minimalce_search()" << std::endl; - } - - ce::counter_example* - minimalce_search::check() - { - clock(); - nb_found = 0; - - if ((!min_ce && mode_) || - !mode_) - min_ce = new ce::counter_example(a); - - if (mode_) - { - min_ce = find(); - tps_ = clock(); - return min_ce; - } - - std::ostringstream os; - const state* s = a->get_init_state(); - recurse_find(s, os); - //std::cout << "nb_found : " << nb_found << std::endl; - - if (min_ce->empty()) - { - delete min_ce; - min_ce = 0; - } - - tps_ = clock(); - return min_ce; - } - - ce::counter_example* - minimalce_search::check(ce::counter_example* ce) - { - min_ce = ce; - - std::ostringstream os; - const state* s = a->get_init_state(); - recurse_find(s, os); - //std::cout << "nb_found : " << nb_found << std::endl; - tps_ = clock(); - return min_ce; - } - - ce::counter_example* - minimalce_search::find() - { - /// FIXME - std::ostringstream os; - - int mode = normal; - int depth_mode = 0; - int depth_mode_memory = -1; - const state* s = 0; - hash_type::iterator i; - tgba_succ_iterator* iter = 0; - - if (h_lenght.empty()) - { - // it's a new search - //std::cout << "it's a new search" << std::endl; - s = a->get_init_state(); - i = h_lenght.find(s); - if (i != h_lenght.end()) - { - delete s; - s = i->first; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - else - h_lenght[s] = stack.size(); - iter = a->succ_iter(s); - iter->first(); - stack.push_front(state_pair(s, iter)); - ++depth_mode; - } - else - s = stack.front().first; - - while (!stack.empty()) - { - recurse: - //std::cout << "recurse: " << a->format_state(s) << std::endl; - - // if (iter) - // delete iter; - - iter = stack.front().second; - while (!iter->done()) - { - //std::cout << "iter" << std::endl; - - //stack_type::iterator j = stack.begin(); - //j->second = iter->current_condition(); - - const state* succ = iter->current_state(); - - if (min_ce->empty() || - ((int)stack.size() + 1 <= min_ce->size())) - { - int depth = in_stack(succ, os); - if (depth != -1) - { - if (closes_accepting(succ, depth, os)) - { - // New counter example is found !! - //std::cout << "CE found !!" << std::endl; - save_counter(succ, os); - - i = h_lenght.find(succ); - if (i == h_lenght.end()) - h_lenght[succ] = stack.size() + 1; - else - { - delete succ; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - - iter->next(); - return min_ce; - } - else - delete succ; - } - - else if ((mode == careful) || - a->state_is_accepting(succ)) - { - s = succ; - iter->next(); - - if (mode != careful) - depth_mode_memory = depth_mode; - mode = careful; - hash_type::iterator i = h_lenght.find(s); - if (i != h_lenght.end()) - { - delete s; - s = i->first; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - else - h_lenght[s] = stack.size(); - - iter = a->succ_iter(s); - iter->first(); - stack.push_front(state_pair(s, iter)); - ++depth_mode; - goto recurse; - } - - else if (h_lenght.find(succ) == h_lenght.end()) - { - s = succ; - iter->next(); - - hash_type::iterator i = h_lenght.find(s); - if (i != h_lenght.end()) - { - delete s; - s = i->first; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - else - h_lenght[s] = stack.size(); - - iter = a->succ_iter(s); - iter->first(); - stack.push_front(state_pair(s, iter)); - ++depth_mode; - goto recurse; - } - - else if ((h_lenght[succ] > (int)stack.size() + 1) && - !min_ce->empty()) - { - s = succ; - iter->next(); - - if (mode != careful) - depth_mode_memory = depth_mode; - mode = careful; - hash_type::iterator i = h_lenght.find(s); - if (i != h_lenght.end()) - { - delete s; - s = i->first; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - else - h_lenght[s] = stack.size(); - - iter = a->succ_iter(s); - iter->first(); - stack.push_front(state_pair(s, iter)); - ++depth_mode; - goto recurse; - } - else - delete succ; - } - else - delete succ; - - iter->next(); - } - - delete iter; - - --depth_mode; - if (depth_mode_memory == depth_mode) - { - depth_mode_memory = -1; - mode = normal; - } - - stack.pop_front(); - s = stack.front().first; - } - - return 0; - } - - void - minimalce_search::recurse_find(const state* s, - std::ostringstream& os, - int mode) - { - - // std::cout << os.str() << "recurse find : " - // << a->format_state(s) << std::endl; - - hash_type::iterator i = h_lenght.find(s); - if (i != h_lenght.end()) - { - delete s; - s = i->first; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - else - h_lenght[s] = stack.size() + 1; - - //stack.push_front(state_pair(s, bddfalse)); - - tgba_succ_iterator* iter = a->succ_iter(s); - stack.push_front(state_pair(s, iter)); - iter->first(); - while (!iter->done()) - { - //stack_type::iterator j = stack.begin(); - //j->second = iter->current_condition(); - - const state* succ = iter->current_state(); - - if (min_ce->empty() || - ((int)stack.size() + 1 <= min_ce->size())) - { - int depth = in_stack(succ, os); - if (depth != -1) - { - if (closes_accepting(succ, depth, os)) - { - // New counter example is found !! - save_counter(succ, os); - - i = h_lenght.find(succ); - if (i == h_lenght.end()) - h_lenght[succ] = stack.size() + 1; - else - { - delete succ; - if (((int)stack.size() + 1) < i->second) - i->second = stack.size() + 1; - } - - } - else - delete succ; - } - else if ((mode == careful) || - a->state_is_accepting(succ)) - { - //std::cout << "recurse 1 : " << stack.size() << " "; - mode = careful; - os << " "; - recurse_find(succ, os, mode); - } - else if (h_lenght.find(succ) == h_lenght.end()) - { - //std::cout << "recurse 2 : " << stack.size() << " "; - os << " "; - recurse_find(succ, os, mode); - } - else if ((h_lenght[succ] > (int)stack.size() + 1) && - !min_ce->empty()) - { - //std::cout << "recurse 3 : " << stack.size() << " "; - mode = careful; - os << " "; - recurse_find(succ, os, mode); - } - else - delete succ; - } - else //if (h_lenght.find(succ) == h_lenght.end()) - delete succ; - - iter->next(); - } - - delete iter; - - //std::cout << os.str() << "stack.pop_front()" << std::endl; - stack.pop_front(); - - } - - bool - minimalce_search::closes_accepting(const state*, - int depth, - std::ostringstream&) const - { - //std::cout << os.str() << "close accepting : " << a->format_state(s); - - int last_depth = -1; - int depth_cp = stack.size(); - - for (stack_type::const_iterator i = stack.begin(); - i != stack.end(); ++i, --depth_cp) - if (a->state_is_accepting(i->first)) - //if (a->state_is_accepting(*i)) - { - last_depth = depth_cp - 1; - //last_depth = h_lenght[*i]; - break; - } - - return depth <= last_depth; - } - - int - minimalce_search::in_stack(const state* s, std::ostringstream&) const - { - //std::cout << os.str() << "in stack : " << a->format_state(s); - - int depth = stack.size(); - - bool return_value = false; - for (stack_type::const_iterator i = stack.begin(); - i != stack.end() && !return_value; ++i, --depth) - { - if (s->compare(i->first) == 0) - //if (s->compare(*i) == 0) - return_value = true; - } - - if (!return_value) - depth = -1; - - return depth; - } - - void - minimalce_search::save_counter(const state* s, std::ostringstream&) - { - //std::cout << os.str() << "save counter" << std::endl; - - ++nb_found; - if (min_ce->empty()) - delete min_ce; - - min_ce = new ce::counter_example(a); - ce::state_ce ce; - for (stack_type::iterator i = stack.begin(); - i != stack.end(); ++i) - { - //ce = ce::state_ce(i->first->clone(), i->second->current_condition()); - ce = ce::state_ce(i->first->clone(), bddfalse); - min_ce->prefix.push_front(ce); - } - - stack_type::iterator i = stack.begin(); - if (i == stack.end()) // empty counter example. - return; - - //const state* s = *i; - min_ce->build_cycle(s); - l_ce.push_front(min_ce); - } - - std::ostream& - minimalce_search::print_stat(std::ostream& os) const - { - int ce_size = 0; - if (min_ce) - ce_size = min_ce->size(); - os << "Size of Counter Example : " << ce_size << std::endl - << "States explored : " << h_lenght.size() << std::endl - << "Computed time : " << tps_ << " microseconds" << std::endl; - return os; - } - - ce::counter_example* - minimalce_search::get_minimal_cyle() const - { - ce::counter_example* min_cycle = min_ce; - for (std::list::const_iterator i = l_ce.begin(); - i != l_ce.end();) - if ((*i)->cycle.size() < min_cycle->cycle.size()) - min_cycle = *i; - return min_cycle; - } - - ce::counter_example* - minimalce_search::get_minimal_prefix() const - { - ce::counter_example* min_prefix = min_ce; - for (std::list::const_iterator i = l_ce.begin(); - i != l_ce.end();) - if ((*i)->prefix.size() < min_prefix->prefix.size()) - min_prefix = *i; - return min_prefix; - } - */ - -} diff --git a/src/tgbaalgos/minimalce.hh b/src/tgbaalgos/minimalce.hh deleted file mode 100644 index 6ab110a17..000000000 --- a/src/tgbaalgos/minimalce.hh +++ /dev/null @@ -1,237 +0,0 @@ -// 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_MINIMALCE_HH -# define SPOT_TGBAALGOS_MINIMALCE_HH - -#include "misc/hash.hh" -#include -#include -#include -#include -#include "tgba/tgbatba.hh" -#include "tgba/bddprint.hh" -//#include "tgbaalgos/gtec/ce.hh" - -#include - -namespace spot -{ - - enum search_opt - { - magic = 0, - nested = 1, - my_nested = 2 - }; - - namespace ce - { - - typedef std::pair state_ce; - typedef std::list l_state_ce; - - /////////////////////////////////////////////////////////////////////////// - // Class counter example. - - class counter_example - { - public : - counter_example(const tgba* a); - ~counter_example(); - - void build_cycle(const state* x); - int size(); - std::ostream& print(std::ostream& os) const; - bdd_dict* get_dict() const; - - /// \brief Project a counter example on a tgba. - void project_ce(const tgba* aut, std::ostream& os = std::cout); - /// \brief Build a tgba from a counter example. - tgba* ce2tgba(); - - l_state_ce prefix; - l_state_ce cycle; - const tgba* automata_; - - }; - - } - - ///////////////////////////////////////////////////////////////////////////// - // The base interface to build an emptiness check algorithm - class emptiness_search - { - protected: - emptiness_search(); - - public: - virtual ~emptiness_search(); - virtual ce::counter_example* check() = 0; - /// \brief Print Stat. - virtual std::ostream& print_stat(std::ostream& os) const; - }; - - ///////////////////////////////////////////////////////////////////////////// - // Perform a minimal search - - class minimalce_search: public emptiness_search - { - public: - //minimalce_search(const tgba_tba_proxy *a, bool mode = false); - minimalce_search(const tgba_tba_proxy *a, int opt = nested); - - virtual ~minimalce_search(); - - /// \brief Find the shortest counter example. - virtual ce::counter_example* check(); - - /// \brief Find a counter example shorter than \a min_ce. - //ce::counter_example* check(ce::counter_example* min_ce); - - //ce::counter_example* find(); - - /// \brief Print Stat. - std::ostream& print_stat(std::ostream& os) const; - std::ostream& print_result(std::ostream& os, - const tgba* restrict = 0) const; - - //ce::counter_example* get_minimal_cyle() const; - //ce::counter_example* get_minimal_prefix() const; - - private: - - /// \brief Minimisation is implemented on the magic search algorithm. - struct magic - { - bool seen_without : 1; - bool seen_with : 1; - bool seen_path : 1; - unsigned int depth; - }; - - struct magic_state - { - const state* s; - bool m; - }; - - enum search_mode - { - normal = 0, - careful = 1 - }; - //int mode; - - - typedef std::pair state_iter_pair; - typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - typedef std::list tstack_type; - /// \brief Stack of transitions. - /// - /// This is an addition to the data from the paper. - tstack_type tstack; - - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - /// Append a new state to the current path. - bool push(const state* s, bool m); - /// Check whether we already visited \a s with the Magic bit set to \a m. - bool has(const state* s, bool m) const; - /// Check if \a s is in the path. - bool exist_path(const state* s) const; - /// Return the depth of the state \a s in stack. - int depth_path(const state* s) const; - - void build_counter(); - - const tgba_tba_proxy* a; ///< The automata to check. - /// The state for which we are currently seeking an SCC. - const state* x; - /// \brief Active the nested search which produce a - /// smaller counter example. - bool nested_; - /// \brief Active the nested bis search which produce a - /// smaller counter example. - const state* x_bis; - bool my_nested_; - bool accepted_path_; - int accepted_depth_; - - unsigned int Maxsize; - - ce::counter_example* counter_; - std::list l_ce; - - /////////////////////////////////////////////////////////////////// - /* - //typedef std::pair state_iter_pair; - typedef Sgi::hash_map hash_type; - hash_type h_lenght; ///< Map of visited states. - - typedef std::pair state_pair; - //typedef std::pair state_pair; - typedef std::list stack_type; - //typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - const tgba_tba_proxy* a; ///< The automata to check. - /// The state for which we are currently seeking an SCC. - //const state* x; - ce::counter_example* min_ce; - std::list l_ce; - int nb_found; - bool mode_; - clock_t tps_; - - /// \brief Perform the minimal search as explain in - /// @InProceedings(GaMoZe04spin, - /// Author = "Gastin, P. and Moro, P. and Zeitoun, M.", - /// Title = "Minimization of counterexamples in {SPIN}", - /// BookTitle = "Proceedings of the 11th SPIN Workshop (SPIN'04)", - /// Editor = "Graf, S. and Mounier, L.", - /// Publisher = SPRINGER, - /// Series = LNCS, - /// Number = 2989, - /// Year = 2004, - /// Pages = "92-108") - void recurse_find(const state* it, - std::ostringstream& os, - int mode = normal); - bool closes_accepting(const state* s, - int detph, - std::ostringstream& os) const; - int in_stack(const state* s, std::ostringstream& os) const; - - /// Save the current path in stack as a counter example. - /// this counter example is the minimal that we have found yet. - void save_counter(const state* s, std::ostringstream& os); - */ - }; - -} - -#endif // SPOT_TGBAALGOS_MINIMALCE_HH diff --git a/src/tgbaalgos/nesteddfs.cc b/src/tgbaalgos/nesteddfs.cc deleted file mode 100644 index b13d378b9..000000000 --- a/src/tgbaalgos/nesteddfs.cc +++ /dev/null @@ -1,322 +0,0 @@ -// 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 -#include -#include "nesteddfs.hh" -#include "tgba/bddprint.hh" - -namespace spot -{ - nesteddfs_search::nesteddfs_search(const tgba_tba_proxy* a, - int opt) - : a(a), x(0), - x_bis(0), - accepted_path_(false) - { - nested_ = my_nested_ = false; - if (opt == nested) - nested_ = true; - if (opt == my_nested) - my_nested_ = true; - Maxsize = 0; - } - - nesteddfs_search::~nesteddfs_search() - { - hash_type::const_iterator s = h.begin(); - while (s != h.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - delete ptr; - } - if (x) - delete x; - // Release all iterators on the stack. - while (!stack.empty()) - { - delete stack.front().second; - stack.pop_front(); - } - } - - bool - nesteddfs_search::push(const state* s, bool m) - { - /* - if ((Maxsize != 0) && // for minimize - (stack.size() + 1 > Maxsize)) - return false; - */ - - tgba_succ_iterator* i = a->succ_iter(s); - i->first(); - - hash_type::iterator hi = h.find(s); - if (hi == h.end()) - { - //magic d = { !m, m, true, stack.size() + 1}; - magic d = { !m, m, true }; - h[s] = d; - } - else - { - hi->second.seen_without |= !m; - hi->second.seen_with |= m; - hi->second.seen_path = true; // for nested search - /* - if ((stack.size() + 1) < hi->second.depth) // for minimize - hi->second.depth = stack.size() + 1; - */ - if (hi->first != s) - delete s; - s = hi->first; - } - - magic_state ms = { s, m }; - stack.push_front(state_iter_pair(ms, i)); - - return true; - } - - bool - nesteddfs_search::has(const state* s, bool m) const - { - hash_type::const_iterator i = h.find(s); - if (i == h.end()) - return false; - if (!m && i->second.seen_without) - return true; - if (m && i->second.seen_with) - return true; - return false; - } - - bool - nesteddfs_search::exist_path(const state* s) const - { - hash_type::const_iterator hi = h.find(s); - if (hi == h.end()) - return false; - if (hi->second.seen_with) - return false; - return hi->second.seen_path && hi->second.seen_without; - } - - int - nesteddfs_search::depth_path(const state* s) const - { - int depth = 0; - stack_type::const_reverse_iterator i; - for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth) - if (s->compare(i->first.s) == 0) - break; - - if (i != stack.rend()) - return depth; - else - return stack.size() + 1; - } - - ce::counter_example* - nesteddfs_search::check() - { - if (my_nested_) - { - accepted_path_ = false; - accepted_depth_ = 0; - } - - if (stack.empty()) - // It's a new search. - push(a->get_init_state(), false); - else - // Remove the transition to the cycle root. - tstack.pop_front(); - - assert(stack.size() == 1 + tstack.size()); - - while (!stack.empty()) - { - recurse: - //std::cout << "recurse : "<< stack.size() << std::endl; - nesteddfs_search::state_iter_pair& p = stack.front(); - tgba_succ_iterator* i = p.second; - const bool magic = p.first.m; - - while (!i->done()) - { - const state* s_prime = i->current_state(); - //std::cout << a->format_state(s_prime) << std::endl; - bdd c = i->current_condition(); - i->next(); - - if ((magic && 0 == s_prime->compare(x)) || - (magic && (nested_ || my_nested_) && exist_path(s_prime)) || - (!magic && my_nested_ && accepted_path_ && - exist_path(s_prime) && depth_path(s_prime) <= accepted_path_)) - { - if (nested_ || my_nested) - { - if (x) - delete x; - x = s_prime->clone(); - } - delete s_prime; - tstack.push_front(c); - assert(stack.size() == tstack.size()); - - build_counter(); - //Maxsize = stack.size(); - //counter_->build_cycle(x); - return counter_; - } - if (!has(s_prime, magic)) - { - if (my_nested_ && a->state_is_accepting(s_prime)) - { - accepted_path_ = true; - accepted_depth_ = stack.size(); - } - if (push(s_prime, magic)) - { - tstack.push_front(c); - goto recurse; - } - // for minimize - } - delete s_prime; - } - - const state* s = p.first.s; - delete i; - if (nested_ || my_nested_) - { - hash_type::iterator hi = h.find(((stack.front()).first).s); - assert (hi != h.end()); - hi->second.seen_path = false; - } - stack.pop_front(); - - if (!magic && a->state_is_accepting(s)) - { - if (!has(s, true)) - { - if (x) - delete x; - x = s->clone(); - push(s, true); - continue; - } - } - if (!stack.empty()) - tstack.pop_front(); - } - - std::cout << "END CHECK" << std::endl; - - assert(tstack.empty()); - - return 0; - } - - std::ostream& - nesteddfs_search::print_result(std::ostream& os, const tgba* restrict) const - { - stack_type::const_reverse_iterator i; - tstack_type::const_reverse_iterator ti; - os << "Prefix:" << std::endl; - const bdd_dict* d = a->get_dict(); - for (i = stack.rbegin(), ti = tstack.rbegin(); - i != stack.rend(); ++i, ++ti) - { - if (i->first.s->compare(x) == 0) - os <<"Cycle:" <first.s; - if (restrict) - { - s = a->project_state(s, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << " " << a->format_state(s) << std::endl; - } - os << " | " << bdd_format_set(d, *ti) << std::endl; - } - - if (restrict) - { - const state* s = a->project_state(x, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - - } - else - { - os << " " << a->format_state(x) << std::endl; - } - return os; - } - - std::ostream& - nesteddfs_search::print_stat(std::ostream& os) const - { - int ce_size = 0; - if (counter_) - ce_size = counter_->size(); - os << "Size of Counter Example : " << ce_size << std::endl - << "States explored : " << h.size() << std::endl; - return os; - } - - void - nesteddfs_search::build_counter() - { - assert(stack.size() == tstack.size()); - counter_ = new ce::counter_example(a); - stack_type::reverse_iterator i; - tstack_type::reverse_iterator ti; - for (i = stack.rbegin(), ti = tstack.rbegin(); - i != stack.rend(); ++i, ++ti) - { - if (i->first.s->compare(x) == 0) - break; - ce::state_ce ce; - ce = ce::state_ce(i->first.s->clone(), *ti); - counter_->prefix.push_back(ce); - } - for (; i != stack.rend(); ++i, ++ti) - { - ce::state_ce ce; - ce = ce::state_ce(i->first.s->clone(), *ti); - counter_->cycle.push_back(ce); - } - //counter_->build_cycle(x); - } - -} diff --git a/src/tgbaalgos/nesteddfs.hh b/src/tgbaalgos/nesteddfs.hh deleted file mode 100644 index 4e5f4a4a2..000000000 --- a/src/tgbaalgos/nesteddfs.hh +++ /dev/null @@ -1,142 +0,0 @@ -// 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_NESTEDDFS_HH -# define SPOT_TGBAALGOS_NESTEDDFS_HH - -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" -#include "tgbaalgos/minimalce.hh" - -namespace spot -{ - - /* - enum search_opt - { - magic = 0, - nested = 1, - my_nested = 2 - }; - */ - - class nesteddfs_search: public emptiness_search - { - - public: - - /// Initialize the Nesteddfs Search algorithm on the automaton \a a. - nesteddfs_search(const tgba_tba_proxy *a, int opt = nested); - - virtual ~nesteddfs_search(); - - /// \brief Perform a Magic or a Nested DFS Search. - /// - /// \return true iff the algorithm has found a new accepting - /// path. - /// - /// check() can be called several times until it return false, - /// to enumerate all accepting paths. - virtual ce::counter_example* check(); - - /// \brief Print the last accepting path found. - /// - /// Restrict printed states to \a the state space of restrict if - /// supplied. - std::ostream& print_result(std::ostream& os, - const tgba* restrict = 0) const; - - /// \brief Print Stat. - std::ostream& print_stat(std::ostream& os) const; - - private: - - // The names "stack", "h", and "x", are those used in the paper. - - /// \brief Records whether a state has be seen with the magic bit - /// on or off. - struct magic - { - bool seen_without : 1; - bool seen_with : 1; - bool seen_path : 1; - //unsigned int depth; - }; - - /// \brief A state for the spot::magic_search algorithm. - struct magic_state - { - const state* s; - bool m; ///< The state of the magic demon. - // int depth; - }; - - typedef std::pair state_iter_pair; - typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - typedef std::list tstack_type; - /// \brief Stack of transitions. - /// - /// This is an addition to the data from the paper. - tstack_type tstack; - - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - /// Append a new state to the current path. - bool push(const state* s, bool m); - /// Check whether we already visited \a s with the Magic bit set to \a m. - bool has(const state* s, bool m) const; - /// Check if \a s is in the path. - bool exist_path(const state* s) const; - /// Return the depth of the state \a s in stack. - int depth_path(const state* s) const; - - void build_counter(); - - const tgba_tba_proxy* a; ///< The automata to check. - /// The state for which we are currently seeking an SCC. - const state* x; - /// \brief Active the nested search which produce a - /// smaller counter example. - bool nested_; - /// \brief Active the nested bis search which produce a - /// smaller counter example. - const state* x_bis; - bool my_nested_; - bool accepted_path_; - int accepted_depth_; - - unsigned int Maxsize; - - ce::counter_example* counter_; - - }; - - -} - -#endif // SPOT_TGBAALGOS_NESTEDDFS_HH diff --git a/src/tgbaalgos/nesteddfsgen.cc b/src/tgbaalgos/nesteddfsgen.cc deleted file mode 100644 index b343b5f20..000000000 --- a/src/tgbaalgos/nesteddfsgen.cc +++ /dev/null @@ -1,333 +0,0 @@ -// 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 "tgbaalgos/nesteddfsgen.hh" - -namespace spot -{ - - nesteddfsgen_search::nesteddfsgen_search(const tgba *a) - : a(a) - { - } - - nesteddfsgen_search::~nesteddfsgen_search() - { - for (stack_type::iterator i = stack.begin(); - i != stack.end(); ++i) - { - //delete i->first; - delete i->second; - } - for (hash_type::iterator i = h.begin(); - i != h.end();) - { - const state *s = i->first; - ++i; - delete s; - } - } - - void - nesteddfsgen_search::free_states() - { - for (std::list::iterator i = states->begin(); - i != states->end(); ++i) - { - delete *i; - } - delete states; - } - - //ce::counter_example* - /* - bool - nesteddfsgen_search::check() - { - hash_type::iterator hi, hi_next; - tgba_succ_iterator *iter, *iter_temp; - const state *init, *s, *s_next, *succ; - bdd cond1, cond2; - - init = a->get_init_state(); - iter_temp = a->succ_iter(init); - iter_temp->first(); - stack.push_front(state_iter_pair(init, iter_temp)); - - while (!stack.empty()) - { - s = stack.front().first; - iter = stack.front().second; - - while (!iter->done()) - { - succ = iter->current_state(); // - hi = h.find(succ); - if (hi != h.end() && - (hi->second.in_stack || - hi->second.processed)) - { - delete succ; - iter->next(); - continue; - } - iter_temp = a->succ_iter(succ); - iter_temp->first(); - stack.push_front(state_iter_pair(succ, iter_temp)); - if (hi != h.end()) - hi->second.in_stack = 1; - else - { - state_info si = { 1, 0, bddfalse }; - h[s] = si; - } - s = succ; - iter->next(); - iter = iter_temp; - } - - //delete iter; - iter = a->succ_iter(s); - hi = h.find(s); - - for (iter->first(); !iter->done(); iter->next()) - { - s_next = iter->current_state(); // - hi_next = h.find(s_next); - if (hi != h.end()) - cond1 = hi->second.cond; - else - cond1 = bddfalse; - if (hi_next != h.end()) - cond2 = hi_next->second.cond; - else - cond2 = bddfalse; - if ((!(iter->current_acceptance_conditions() | cond1) | - cond2) != bddtrue) - markConditions(s_next, - iter->current_acceptance_conditions() - | cond1); - //else - //delete s_next; - } - delete iter; - - if (hi != h.end() && - hi->second.cond == a->all_acceptance_conditions()) - { - std::cout << "Counter example found" << std::endl; - return 1; - } - - //free_states(); - - if (hi == h.end()) - { - state_info si = { 0, 1, bddfalse }; - h[s] = si; - } - else - { - hi->second.processed = 1; - //delete s; - } - - hi = h.find(stack.front().first); - if (hi == h.end()) - delete stack.front().first; - delete stack.front().second; - //iter = stack.front().second; - //delete iter; - stack.pop_front(); - - } - - std::cout << "Automate is inf-empty" << std::endl; - return 0; - } - */ - - bool - nesteddfsgen_search::check() - { - hash_type::iterator hi, hi_next; - tgba_succ_iterator *iter, *iter_temp; - const state *init, *s, *s_next, *succ; - bdd cond1, cond2; - - init = a->get_init_state(); - iter_temp = a->succ_iter(init); - iter_temp->first(); - stack.push_front(state_iter_pair(init, iter_temp)); - state_info si = { 1, 0, bddfalse }; - h[init] = si; - - while (!stack.empty()) - { - recurse: - s = stack.front().first; - iter = stack.front().second; - - while (!iter->done()) - { - //std::cout << "while (!iter->done())" << std::endl; - succ = iter->current_state(); - - hi = h.find(succ); - if (hi != h.end() && - (hi->second.in_stack || - hi->second.processed)) - { - delete succ; - iter->next(); - continue; - } - - iter->next(); - - iter = a->succ_iter(succ); - iter->first(); - stack.push_front(state_iter_pair(succ, iter)); - - state_info si = { 1, 0, bddfalse }; - h[succ] = si; - goto recurse; - } - - iter = a->succ_iter(s); - hi = h.find(s); - - for (iter->first(); !iter->done(); iter->next()) - { - //std::cout << "for (iter->first(); !iter->done(); iter->next())" - //<< std::endl; - s_next = iter->current_state(); // - hi_next = h.find(s_next); - if (hi != h.end()) - cond1 = hi->second.cond; - else - cond1 = bddfalse; - if (hi_next != h.end()) - cond2 = hi_next->second.cond; - else - cond2 = bddfalse; - if ((!(iter->current_acceptance_conditions() | cond1) | - cond2) != bddtrue) - markConditions(s_next, - iter->current_acceptance_conditions() - | cond1); - else - delete s_next; - } - delete iter; - - if (hi != h.end() && - hi->second.cond == a->all_acceptance_conditions()) - { - std::cout << "Counter example found" << std::endl; - return 1; - } - - if (hi == h.end()) - { - state_info si = { 0, 1, bddfalse }; - h[s] = si; - } - else - { - hi->second.processed = 1; - } - - hi = h.find(stack.front().first); - if (hi == h.end()) - delete stack.front().first; - delete stack.front().second; - stack.pop_front(); - - } - - std::cout << "Automate is inf-empty" << std::endl; - return 0; - } - - void - nesteddfsgen_search::markConditions(const state* s, bdd conditions) - { - //std::cout << "markConditions" << std::endl; - - states = new std::list; - hash_type::iterator hi; - tgba_succ_iterator* iter; - const state *q_next, *q; - bdd cond; - - states->push_front(s); - do - { - q = states->front(); - states->pop_front(); - hi = h.find(q); - if (hi != h.end()) - { - delete q; - q = hi->first; - hi->second.cond |= conditions; - } - else - { - state_info si = { 0, 0, conditions }; - h[q] = si; - } - iter = a->succ_iter(q); - for (iter->first(); !iter->done(); iter->next()) - { - q_next = iter->current_state(); - hi = h.find(q_next); - if (hi != h.end()) - cond = hi->second.cond; - else - cond = bddfalse; - if ((hi != h.end() && - (hi->second.in_stack || hi->second.processed)) && - ((!conditions | cond) != bddtrue)) - { - states->push_front(q_next); - } - else - delete q_next; - } - delete iter; - } - while (!states->empty()); - - //delete s; // ?? - - free_states(); - } - - void - nesteddfsgen_search::print_stats(std::ostream& os) const - { - os << h.size() << " unique states visited" << std::endl; - os << "size of stack : " << stack.size() << std::endl; - } - -} diff --git a/src/tgbaalgos/nesteddfsgen.hh b/src/tgbaalgos/nesteddfsgen.hh deleted file mode 100644 index 78d1e4be3..000000000 --- a/src/tgbaalgos/nesteddfsgen.hh +++ /dev/null @@ -1,81 +0,0 @@ -// 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_NESTEDDFSGEN_HH -# define SPOT_TGBAALGOS_NESTEDDFSGEN_HH - -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgba.hh" -#include "tgbaalgos/minimalce.hh" - -namespace spot -{ - class nesteddfsgen_search - { - - public: - - /// Initialize the Nesteddfs Search algorithm on the automaton \a a. - nesteddfsgen_search(const tgba *a); - ~nesteddfsgen_search(); - - /// \brief Find a counter example. - //ce::counter_example* check(); - bool check(); - - void print_stats(std::ostream& os) const; - - private: - - struct state_info - { - bool in_stack : 1; - bool processed : 1; - bdd cond; - }; - - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - //hash_type processed; ///< Map of processed states. - - - typedef std::pair state_iter_pair; - typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - std::list *states; - - void markConditions(const state* s, bdd cond); - void free_states(); - - const tgba* a; - ce::counter_example* counter_; - - }; - - -} - -#endif // SPOT_TGBAALGOS_NESTEDDFS_HH diff --git a/src/tgbaalgos/tarjan_on_fly.cc b/src/tgbaalgos/tarjan_on_fly.cc deleted file mode 100644 index 5e0f82625..000000000 --- a/src/tgbaalgos/tarjan_on_fly.cc +++ /dev/null @@ -1,193 +0,0 @@ -// 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 "tgbaalgos/tarjan_on_fly.hh" - - -namespace spot -{ - - tarjan_on_fly::tarjan_on_fly(const tgba_tba_proxy *a) - : a(a), x(0) - { - } - - tarjan_on_fly::~tarjan_on_fly() - { - for (stack_type::iterator i = stack.begin(); - i != stack.end(); ++i) - { - hash_type::iterator hi = h.find(i->s); - if (hi != h.end()) - h.erase(hi); - delete i->s; - delete i->lasttr; - } - - for (hash_type::iterator i = h.begin(); - i != h.end();) - { - const state *s = i->first; - ++i; - delete s; - } - } - - bool - tarjan_on_fly::check() - { - tgba_succ_iterator* iter = 0; - const state* succ = 0; - int pos = 0; - top = dftop = -1; - violation = false; - - const state* s = a->get_init_state(); - push(s); - - while (!violation && dftop >= 0) - { - s = stack[dftop].s; - iter = stack[dftop].lasttr; - if (iter == 0) - { - iter = a->succ_iter(s); - iter->first(); - stack[dftop].lasttr = iter; - } - else - { - iter->next(); - } - - succ = 0; - if (!iter->done()) - { - succ = iter->current_state(); - if (h.find(succ) == h.end()) - push(succ); - else - { - pos = in_stack(succ); - delete succ; - if (pos != -1) // succ is in stack - lowlinkupdate(dftop, pos); - } - } - else - pop(); - } - - return violation; - } - - void - tarjan_on_fly::push(const state* s) - { - h[s] = top++; - - struct_state ss = { s, 0, top, dftop, 0 }; - - if (a->state_is_accepting(s)) - { - ss.acc = top; - x = s; // FIXME - } - else if (dftop >= 0) - ss.acc = stack[dftop].acc; - else - ss.acc = -1; - - if (top < (int)stack.size()) - { - const state* sdel = stack[top].s; - tgba_succ_iterator* iter = stack[top].lasttr; - - if (h.find(sdel) == h.end()) - { - assert(0); - delete sdel; - } - if (iter) - delete iter; - - - stack[top] = ss; - } - else - { - stack.push_back(ss); - } - - dftop = top; - } - - void - tarjan_on_fly::pop() - { - int p = stack[dftop].pre; - - if (p >= 0) - lowlinkupdate(p, dftop); - - if (stack[dftop].lowlink == dftop) - top = dftop - 1; - - dftop = p; - } - - void - tarjan_on_fly::lowlinkupdate(int f, int t) - { - if (stack[t].lowlink <= stack[f].lowlink) - { - if (stack[t].lowlink <= stack[f].acc) - { - violation = true; - } - stack[f].lowlink = stack[t].lowlink; - } - } - - int - tarjan_on_fly::in_stack(const state* s) const - { - int n = 0; - - stack_type::const_iterator i; - for (i = stack.begin(); i != stack.end(); ++i, ++n) - if (s->compare(i->s) == 0) - break; - - if (i == stack.end()) - return -1; - - return n; - } - - std::ostream& - tarjan_on_fly::print_stat(std::ostream& os) const - { - os << "States explored : " << h.size() << std::endl; - return os; - } - -} diff --git a/src/tgbaalgos/tarjan_on_fly.hh b/src/tgbaalgos/tarjan_on_fly.hh deleted file mode 100644 index 8cef1642b..000000000 --- a/src/tgbaalgos/tarjan_on_fly.hh +++ /dev/null @@ -1,83 +0,0 @@ -// 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_TARJAN_ON_FLY_HH -# define SPOT_TGBAALGOS_TARJAN_ON_FLY_HH - -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" - -namespace spot -{ - - class tarjan_on_fly - { - - public: - - tarjan_on_fly(const tgba_tba_proxy *a); - virtual ~tarjan_on_fly(); - - /// \brief Return true if there exits an accepting path. - bool check(); - - /// \brief Print Stat. - std::ostream& print_stat(std::ostream& os) const; - - private: - - struct struct_state - { - const state* s; - tgba_succ_iterator* lasttr; - int lowlink; - int pre; - int acc; - }; - - //typedef std::pair state_iter_pair; - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - typedef std::vector stack_type; - stack_type stack; ///< Stack of visited states on the path. - - const tgba_tba_proxy* a; ///< The automata to check. - - int top; - int dftop; - bool violation; - - const state* x; - - void push(const state* s); - void pop(); - void lowlinkupdate(int f, int t); - int in_stack(const state* s) const; - }; - -} - -#endif // SPOT_TGBAALGOS_MINIMALCE_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 76f182c76..0ffc81bb4 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -64,8 +64,6 @@ tripprod_SOURCES = tripprod.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. TESTS = \ - reduccmp.test \ - reductgba.test \ explicit.test \ tgbaread.test \ readsave.test \ @@ -79,6 +77,8 @@ TESTS = \ tripprod.test \ mixprod.test \ dupexp.test \ + reduccmp.test \ + reductgba.test \ emptchk.test \ emptchke.test \ spotlbtt.test diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 028cf895b..1f0c38c70 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -27,53 +27,32 @@ set -e expect_ce() { - #run 0 ./ltl2tgba -m -f "$1" - #run 0 ./ltl2tgba -ndfs -f "$1" - run 0 ./ltl2tgba -tj -f "$1" - #run 0 ./ltl2tgba -c -f "$1" - #run 0 ./ltl2tgba -ndfs2 -f "$1" - #run 0 ./ltl2tgba -ng -f "$1" - - #run 0 ./ltl2tgba -ms -f "$1" - #run 0 ./ltl2tgba -msit -f "$1" - - #run 0 ./ltl2tgba -e "$1" - #run 0 ./ltl2tgba -e -D "$1" - #run 0 ./ltl2tgba -e -f "$1" - #run 0 ./ltl2tgba -e -f -D "$1" - #run 0 ./ltl2tgba -e2 "$1" - #run 0 ./ltl2tgba -e2 -D "$1" - #run 0 ./ltl2tgba -e2 -f "$1" - #run 0 ./ltl2tgba -e2 -f -D "$1" - #run 0 ./ltl2tgba -mold "$1" - #run 0 ./ltl2tgba -mold -f "$1" + run 0 ./ltl2tgba -e "$1" + run 0 ./ltl2tgba -e -D "$1" + run 0 ./ltl2tgba -e -f "$1" + run 0 ./ltl2tgba -e -f -D "$1" + run 0 ./ltl2tgba -e2 "$1" + run 0 ./ltl2tgba -e2 -D "$1" + run 0 ./ltl2tgba -e2 -f "$1" + run 0 ./ltl2tgba -e2 -f -D "$1" + run 0 ./ltl2tgba -m "$1" + run 0 ./ltl2tgba -m -f "$1" } expect_no() { - #run 0 ./ltl2tgba -M -f "$1" - #run 0 ./ltl2tgba -Ndfs -f "$1" - run 0 ./ltl2tgba -TJ -f "$1" - #run 0 ./ltl2tgba -C -f "$1" - #run 0 ./ltl2tgba -Ndfs2 -f "$1" - #run 0 ./ltl2tgba -NG -f "$1" - - #run 0 ./ltl2tgba -Ms -f "$1" - - #run 0 ./ltl2tgba -E "$1" - #run 0 ./ltl2tgba -E -D "$1" - #run 0 ./ltl2tgba -E -f "$1" - #run 0 ./ltl2tgba -E -f -D "$1" - #run 0 ./ltl2tgba -E2 "$1" - #run 0 ./ltl2tgba -E2 -D "$1" - #run 0 ./ltl2tgba -E2 -f "$1" - #run 0 ./ltl2tgba -E2 -f -D "$1" - #run 0 ./ltl2tgba -M "$1" - #run 0 ./ltl2tgba -M -f "$1" + run 0 ./ltl2tgba -E "$1" + run 0 ./ltl2tgba -E -D "$1" + run 0 ./ltl2tgba -E -f "$1" + run 0 ./ltl2tgba -E -f -D "$1" + run 0 ./ltl2tgba -E2 "$1" + run 0 ./ltl2tgba -E2 -D "$1" + run 0 ./ltl2tgba -E2 -f "$1" + run 0 ./ltl2tgba -E2 -f -D "$1" + run 0 ./ltl2tgba -M "$1" + run 0 ./ltl2tgba -M -f "$1" } -expect_ce 'Fa & Xb & GFc & Gd' - expect_ce 'a' expect_ce 'a U b' expect_ce 'X a' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 10659e89b..316d17ed3 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -36,11 +36,6 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgbaalgos/magic.hh" -#include "tgbaalgos/nesteddfs.hh" -#include "tgbaalgos/nesteddfsgen.hh" -#include "tgbaalgos/colordfs.hh" -#include "tgbaalgos/tarjan_on_fly.hh" -//#include "tgbaalgos/minimalce.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/ce.hh" #include "tgbaparse/public.hh" @@ -60,10 +55,6 @@ syntax(char* prog) << "reachability graph" << std::endl << " -A same as -a, but as a set" << std::endl - << " -c color-search (implies -D), expect a counter-example" - << std::endl - << " -C color-search (implies -D), expect no counter-example" - << std::endl << " -d turn on traces during parsing" << std::endl << " -D degeneralize the automaton" << std::endl << " -e emptiness-check (Couvreur), expect and compute " @@ -80,38 +71,12 @@ syntax(char* prog) << " -L fair-loop approximation (implies -f)" << std::endl << " -m magic-search (implies -D), expect a counter-example" << std::endl - << " -ms minmimal-search (implies -D), expect a counter-example" - << std::endl - << " -msit minmimal-search (implies -D), expect a counter-example" - << std::endl - << " -mold magic-search (implies -D), expect a counter-example" - << std::endl << " -M magic-search (implies -D), expect no counter-example" << std::endl - << " -Mold magic-search (implies -D), expect no counter-example" - << std::endl << " -n same as -m, but display more counter-examples" << std::endl << " -N display the never clain for Spin " << "(implies -D)" << std::endl - << " -ndfs nesteddfs-search (implies -D), expect a " - << "counter-example" - << std::endl - << " -Ndfs nesteddfs-search (implies -D), expect no " - << "counter-example" - << std::endl - << " -ndfs2 modify-nesteddfs-search (implies -D), " - << "expect a counter-example" - << std::endl - << " -Ndfs2 modify-nesteddfs-search (implies -D), " - << "expect no counter-example" - << std::endl - << " -ng nesteddfs-search generalized (implies -D), expect a " - << "counter-example" - << std::endl - << " -NG nesteddfs-search generalized (implies -D), expect no " - << "counter-example" - << std::endl << " -p branching postponement (implies -f)" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl @@ -146,12 +111,6 @@ syntax(char* prog) << " -S convert to explicit automata, and number states " << "in BFS order" << std::endl << " -t display reachable states in LBTT's format" << std::endl - << " -T display reachable states in LBTT's format w/o " - << "acceptance conditions" << std::endl - << " -tj tarjan-on-fly (implies -D), expect a counter-example" - << std::endl - << " -TJ tarjan-on-fly (implies -D), expect no counter-example" - << std::endl << " -U[PROPS] consider atomic properties PROPS as exclusive " << "events (implies -f)" << std::endl << " -v display the BDD variables used by the automaton" @@ -178,12 +137,7 @@ main(int argc, char** argv) bool file_opt = false; int output = 0; int formula_index = 0; - enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld, - NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch, - TarjanOnFly, MinimalSearch, MinimalSearchIterative, - NestedGeneSearch} echeck = None; - spot::emptiness_search* es = 0; - spot::search_opt opt_nested_search = spot::magic; + enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; bool expect_counter_example = false; @@ -213,21 +167,6 @@ main(int argc, char** argv) { output = 4; } - else if (!strcmp(argv[formula_index], "-c")) - { - echeck = ColorDFSSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - magic_many = false; - } - else if (!strcmp(argv[formula_index], "-C")) - { - echeck = ColorDFSSearch; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } else if (!strcmp(argv[formula_index], "-d")) { debug_opt = true; @@ -275,61 +214,21 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-m")) { - opt_nested_search = spot::magic; echeck = MagicSearch; degeneralize_opt = true; expect_counter_example = true; output = -1; - magic_many = true; } else if (!strcmp(argv[formula_index], "-M")) { - opt_nested_search = spot::magic; echeck = MagicSearch; degeneralize_opt = true; expect_counter_example = false; output = -1; } - else if (!strcmp(argv[formula_index], "-mold")) - { - echeck = MagicSearchOld; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - magic_many = true; - } - else if (!strcmp(argv[formula_index], "-Mold")) - { - echeck = MagicSearchOld; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-ms")) - { - echeck = MinimalSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-Ms")) - { - echeck = MinimalSearch; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-msit")) - { - echeck = MinimalSearchIterative; - degeneralize_opt = true; - expect_counter_example = true; - magic_many = true; - output = -1; - } else if (!strcmp(argv[formula_index], "-n")) { - echeck = MagicSearchOld; + echeck = MagicSearch; degeneralize_opt = true; expect_counter_example = true; output = -1; @@ -340,53 +239,6 @@ main(int argc, char** argv) degeneralize_opt = true; output = 8; } - else if (!strcmp(argv[formula_index], "-ndfs")) - { - opt_nested_search = spot::nested; - echeck = NestedDFSSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - magic_many = true; - } - else if (!strcmp(argv[formula_index], "-Ndfs")) - { - opt_nested_search = spot::nested; - echeck = NestedDFSSearch; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-ndfs2")) - { - opt_nested_search = spot::my_nested; - echeck = NestedDFSSearchModify; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-Ndfs2")) - { - opt_nested_search = spot::my_nested; - echeck = NestedDFSSearchModify; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-ng")) - { - echeck = NestedGeneSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-NG")) - { - echeck = NestedGeneSearch; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } else if (!strcmp(argv[formula_index], "-p")) { post_branching = true; @@ -460,20 +312,6 @@ main(int argc, char** argv) { output = 6; } - else if (!strcmp(argv[formula_index], "-tj")) - { - echeck = TarjanOnFly; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-TJ")) - { - echeck = TarjanOnFly; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } else if (!strncmp(argv[formula_index], "-U", 2)) { unobservables = new spot::ltl::atomic_prop_set; @@ -730,18 +568,7 @@ main(int argc, char** argv) } break; - case NestedGeneSearch: - { - std::cout << "Nested DFS generalized" << std::endl; - spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a); - bool res = ec->check(); - ec->print_stats(std::cout); - exit_code = expect_counter_example ? !res : res; - delete ec; - } - break; - - case MagicSearchOld: + case MagicSearch: { std::cout << "Magic Search" << std::endl; spot::magic_search ms(degeneralized); @@ -764,96 +591,10 @@ main(int argc, char** argv) } break; - case ColorDFSSearch: - std::cout << "Colored Search" << std::endl; - es = new spot::colordfs_search(degeneralized); - break; - - case TarjanOnFly: - { - std::cout << "Tarjan On Fly" << std::endl; - spot::tarjan_on_fly* tof = new spot::tarjan_on_fly(degeneralized); - bool res = tof->check(); - exit_code = expect_counter_example ? !res : res; - delete tof; - break; - } - - case MinimalSearch: - { - std::cout << "Recursive Minimal Search" << std::endl; - es = new spot::colordfs_search(degeneralized); - spot::ce::counter_example* res = es->check(); - res->print(std::cout); - std::cout << "Minimisation:" << std::endl; - es = new spot::minimalce_search(degeneralized, false); - res = es->check(); - res->print(std::cout); - } - break; - - case MinimalSearchIterative: - std::cout << "Iterative Minimal Search" << std::endl; - es = new spot::minimalce_search(degeneralized, true); - break; - - case MagicSearch: - std::cout << "Magic Search" << std::endl; - es = new spot::nesteddfs_search(degeneralized, opt_nested_search); - break; - - case NestedDFSSearch: - case NestedDFSSearchModify: - std::cout << "Nested DFS" << std::endl; - es = new spot::nesteddfs_search(degeneralized, opt_nested_search); - break; - default: assert(0); } - if (es) - { - spot::ce::counter_example* res = es->check(); - if (expect_counter_example) - { - do - { - if (!res) - { - exit_code = 1; - break; - } - std::cout << "CE : " << std::endl - << " size : " << res->size() - << std::endl; - spot::tgba* aut = res->ce2tgba(); - //spot::dotty_reachable(std::cout, aut); - res->print(std::cout); - es->print_stat(std::cout); - delete aut; - delete res; - res = 0; - } - while (magic_many && (res = es->check())); - } - else if (res) - { - exit_code = res->size(); - std::cout << "res->size ?? : " << exit_code << std::endl; - } - else - { - exit_code = (res != 0); - std::cout << "res != 0 ?? : " << exit_code << std::endl; - } - if (res) - delete res; - } - - - if (es) - delete es; if (f) spot::ltl::destroy(f); if (expl)