diff --git a/ChangeLog b/ChangeLog index 334cf51a3..4b72521c4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,28 @@ +2004-08-23 Thomas Martinez + + * src/tgbaalgos/tarjan_on_fly.hh, + src/tgbaalgos/tarjan_on_fly.cc, + src/tgbaalgos/nesteddfs.hh, + src/tgbaalgos/nesteddfs.cc, + src/tgbaalgos/minimalce.hh, + src/tgbaalgos/minimalce.cc, + src/tgbaalgos/colordfs.hh, + src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check. + + src/tgbaalgos/gtec/ce.hh, + src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce + object in minimalce.hh. + + src/tgbatest/ltl2tgba.cc, + src/tgbatest/emptchk.test, + src/tgbaalgos/Makefile.am: Add files for emptyness-check. + +2004-08-23 Thomas Martinez + + * src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata. + * src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition + for scc reduce. + 2004-08-13 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0y. diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index b10b41e2e..622ae74a7 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -123,6 +123,8 @@ namespace spot this->compute_scc(); this->prune_acc(); this->delete_scc(); + + this->merge_transitions(); } std::string @@ -424,6 +426,12 @@ namespace spot } + void + tgba_reduc::merge_state_delayed(const spot::state*, + const spot::state*) + { + } + ///////////////////////////////////////// ///////////////////////////////////////// @@ -580,8 +588,6 @@ namespace spot void tgba_reduc::remove_acc(const spot::state* s) { - //std::cout << "remove_acc" << std::endl; - tgba_explicit::state* s1; seen_map::iterator sm = si_.find(s); sm = si_.find(s); @@ -624,7 +630,6 @@ namespace spot tgba_reduc::is_not_accepting(const spot::state* s, int n) { - //std::cout << "is not accepting" << std::endl; bool b = false; // First call of is_terminal // @@ -726,8 +731,6 @@ namespace spot bool tgba_reduc::is_terminal(const spot::state* s, int n) { - // FIXME - // a SCC is terminal if there are no transition // leaving the SCC AND she doesn't contain all // the acceptance condition. diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index 98cd97216..91b4a4482 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -117,6 +117,12 @@ namespace spot void merge_state(const spot::state* s1, const spot::state* s2); + /// Redirect all transition leading to s1 to s2. + /// Note that we can do the reverse because + /// s1 and s2 belong to a co-simulate relation. + void merge_state_delayed(const spot::state* s1, + const spot::state* s2); + /// Remove all the scc which are terminal and doesn't /// contains all the acceptance conditions. void delete_scc(); diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 3ddabb01d..518c968ae 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -27,33 +27,41 @@ 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 \ neverclaim.hh \ powerset.hh \ reachiter.hh \ save.hh \ stats.hh \ - reductgba_sim.hh + reductgba_sim.hh \ + tarjan_on_fly.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 \ neverclaim.cc \ powerset.cc \ reachiter.cc \ save.cc \ stats.cc \ reductgba_sim.cc \ - reductgba_sim_del.cc + reductgba_sim_del.cc \ + tarjan_on_fly.cc libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/colordfs.cc b/src/tgbaalgos/colordfs.cc new file mode 100644 index 000000000..83ef8f6d0 --- /dev/null +++ b/src/tgbaalgos/colordfs.cc @@ -0,0 +1,296 @@ +// 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) + { + } + + 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++) + { + //std::cout << "iter : " << n << std::endl; + s2 = i->current_state(); + //std::cout << a->format_state(s2) << std::endl; + hi = h.find(s2); + if (hi != h.end()) + return_value &= (hi->second.c == black); + else + return_value = false; + delete s2; + } + delete i; + + //std::cout << "End Loop" << std::endl; + + 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(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 : " << a->format_state(s) << std::endl; + if (!push(s, blue)) + 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(); + //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)) + { + 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(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(s)) + return 1; + dfs_black(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; + + //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 new file mode 100644 index 000000000..a7fa97aac --- /dev/null +++ b/src/tgbaalgos/colordfs.hh @@ -0,0 +1,121 @@ +// 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 emptyness_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); + 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; + + 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 dac2f2415..ede0507da 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -35,6 +35,8 @@ namespace spot eccf) : ecs_(ecs) { + counter_ = new ce::counter_example(ecs->aut); + assert(!ecs_->root.empty()); assert(suffix.empty()); @@ -76,6 +78,10 @@ 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 @@ -113,21 +119,35 @@ namespace spot const state* h_dest = scc[k]->has_state(dest); if (!h_dest) { - // If we have found a state in the next SCC. + // If we have found a state in greater SCC which. // 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()) { @@ -211,14 +231,27 @@ 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()) @@ -256,6 +289,9 @@ namespace spot } + //////////////////////////////////////////////////////////////////////// + /* + void counter_example::accepting_path(const explicit_connected_component* scc, const state* start, bdd acc_to_traverse) @@ -380,7 +416,12 @@ 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); + { + period.push_back(*it); + ce::state_ce ce(it->first, it->second); + counter_->cycle.push_back(ce); + counter_->cycle.push_back(*it); + } // Prepare to find another path for the remaining acceptance // conditions. @@ -393,6 +434,153 @@ 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) + { + // 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); + 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 { @@ -444,4 +632,10 @@ 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 f541e3522..a5816bf94 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -25,6 +25,8 @@ #include "status.hh" #include "explscc.hh" +#include "tgbaalgos/minimalce.hh" + namespace spot { /// Compute a counter example from a spot::emptiness_check_status @@ -51,6 +53,8 @@ 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. @@ -64,6 +68,7 @@ namespace spot private: const emptiness_check_status* ecs_; + ce::counter_example* counter_; }; } diff --git a/src/tgbaalgos/minimalce.cc b/src/tgbaalgos/minimalce.cc new file mode 100644 index 000000000..a2453f722 --- /dev/null +++ b/src/tgbaalgos/minimalce.cc @@ -0,0 +1,539 @@ +// 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.size() != 0); + 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 emptyness search algorithm + emptyness_search::emptyness_search() + { + } + + emptyness_search::~emptyness_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& + emptyness_search::print_stat(std::ostream& os) const + { + return os; + } + + ///////////////////////////////////////////////////////////////////////////// + // minimal_search + + minimalce_search::minimalce_search(const tgba_tba_proxy *a) + : a(a), min_ce(0) + { + } + + 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; + min_ce = new ce::counter_example(a); + 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->size() == 0) + { + delete min_ce; + min_ce = 0; + } + + tps_ = clock(); + return min_ce; + } + + ce::counter_example* + minimalce_search::check(ce::counter_example*) + { + min_ce = new ce::counter_example(a); + + /* + ce::l_state_ce::iterator i; + int depth = 0; + for (i = min_ce->prefix.begin(); + i != min_ce->prefix.end(); ++i, ++depth) + { + stack.push_front(i->first); + //if (h_lenght.find(i->first) == h_lenght.end()) + h_lenght[i->first] = depth; + } + for (i = min_ce->cycle.begin(); + i != min_ce->cycle.end(); ++i, ++depth) + { + stack.push_front(i->first); + if (h_lenght.find(i->first) == h_lenght.end()) + h_lenght[i->first] = depth; + } + */ + + const state* s = a->get_init_state(); + std::ostringstream os; + recurse_find(s, os); + //if (recurse_find(s)) + //return min_ce; + //else + return min_ce; + } + + 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(); + + stack.push_front(state_pair(s, bddfalse)); + //stack.push_front(s); + + tgba_succ_iterator* iter = a->succ_iter(s); + iter->first(); + while (!iter->done()) + { + stack_type::iterator j = stack.begin(); + j->second = iter->current_condition(); + + const state* succ = iter->current_state(); + + std::cout << "stack.size() +1: " << (int)stack.size() + 1 + << "min_ce->size() : " << min_ce->size()<< std::endl; + if ((min_ce->size() == 0) || + ((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->size() != 0)) + { + //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; + } + + /* + if (depth <= last_depth) + std::cout << " : true => depth : " + << depth << ", last_depth" + << last_depth << std::endl; + else + std::cout << " : false => depth : " + << depth << ", last_depth : " + << last_depth << std::endl; + */ + + return depth <= last_depth; // May be '<=' + } + + 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; + + /* + if (return_value) + std::cout << " : true" << std::endl; + else + { + depth = -1; + std::cout << " : false" << std::endl; + } + */ + + 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->size()) + l_ce.push_front(min_ce); + else + 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); + //ce = ce::state_ce((*i)->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); + } + + 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 new file mode 100644 index 000000000..bde6e7005 --- /dev/null +++ b/src/tgbaalgos/minimalce.hh @@ -0,0 +1,150 @@ +// 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 +{ + + 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 for build a emptyness search algorithm + class emptyness_search + { + protected: + emptyness_search(); + + public: + virtual ~emptyness_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 emptyness_search + { + public: + minimalce_search(const tgba_tba_proxy *a); + + 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); + + /// \brief Print Stat. + std::ostream& print_stat(std::ostream& os) const; + + ce::counter_example* get_minimal_cyle() const; + ce::counter_example* get_minimal_prefix() const; + + private: + + enum search_mode + { + normal = 0, + careful = 1 + }; + //int mode; + + //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::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; + clock_t tps_; + + 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 new file mode 100644 index 000000000..4a20d365d --- /dev/null +++ b/src/tgbaalgos/nesteddfs.cc @@ -0,0 +1,355 @@ +// 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; + } + + 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) + { + 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 }; + h[s] = d; + } + else + { + hi->second.seen_without |= !m; + hi->second.seen_with |= m; + hi->second.seen_path = true; // for nested search + if (hi->first != s) + delete s; + s = hi->first; + + /* + if (hi->second.depth != -1 && + hi->second.depth > (int)stack.size()) + return false; + */ + + } + + magic_state ms = { s, m }; + stack.push_front(state_iter_pair(ms, i)); + + // We build the counter example. + /* + bdd b = bddfalse; + if (!i->done()) // if the state is dead. + b = i->current_condition(); + ce::state_ce ce; + ce = ce::state_ce(s->clone(), b); + counter_->prefix.push_back(ce); + */ + + 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() + { + + /// + 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; + while (!stack.empty()) + { + delete stack.front().second; + stack.pop_front(); + } + /// + + //counter_ = new ce::counter_example(a); + + clock(); + + 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(); + //counter_->build_cycle(x); + tps_ = clock(); + return counter_; + } + if (!has(s_prime, magic)) + { + if (my_nested_ && a->state_is_accepting(s_prime)) + { + accepted_path_ = true; + accepted_depth_ = stack.size(); + } + push(s_prime, magic); + tstack.push_front(c); + goto recurse; + } + 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(); + /* + delete (counter_->prefix.back()).first; + counter_->prefix.pop_back(); + */ + + 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()); + //delete counter_; + + tps_ = clock(); + + 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 + << "Computed time : " << tps_ << " microseconds" << 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 new file mode 100644 index 000000000..f15b564ee --- /dev/null +++ b/src/tgbaalgos/nesteddfs.hh @@ -0,0 +1,138 @@ +// 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 emptyness_search + { + + public: + + /// Initialize the Nesteddfs Search algorithm on the automaton \a a. + nesteddfs_search(const tgba_tba_proxy *a, int opt = my_nested); + + virtual ~nesteddfs_search(); + + /// \brief Perform 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; + }; + + /// \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_; + + ce::counter_example* counter_; + clock_t tps_; + + }; + + +} + +#endif // SPOT_TGBAALGOS_NESTEDDFS_HH diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index bc39a29c6..6319d6e03 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -58,8 +58,6 @@ namespace spot lead_2_acc_all_ = false; seen_ = false; - //seen_ = new bool(false); - //bool_v[nb_node++] = seen_; } spoiler_node_delayed::~spoiler_node_delayed() @@ -74,8 +72,6 @@ namespace spot // We take the max of the progress measure of the successor node // because we are on a spoiler. - //std::cout << "spoiler_node_delayed::set_win" << std::endl; - if (lnode_succ->size() == 0) progress_measure_ = nb_spoiler_loose_ + 1; @@ -125,7 +121,6 @@ namespace spot bool spoiler_node_delayed::compare(spoiler_node* n) { - //std::cout << "spoiler_node_delayed::compare" << std::endl; return (this->spoiler_node::compare(n) && (acceptance_condition_visited_ == dynamic_cast(n)-> @@ -183,7 +178,6 @@ namespace spot bool spoiler_node_delayed::get_lead_2_acc_all() { - //std::cout << "spoiler_node_delayed::get_lead_2_acc_all" << std::endl; return lead_2_acc_all_; } @@ -191,7 +185,6 @@ namespace spot bool spoiler_node_delayed::set_lead_2_acc_all(bdd acc) { - //std::cout << "spoiler_node_delayed::set_lead_2_acc_all" << std::endl; if (!seen_) { seen_ = true; @@ -201,7 +194,6 @@ namespace spot } else { - //seen_ = true; if (acc == all_acc_cond) lead_2_acc_all_ = true; } @@ -225,9 +217,6 @@ namespace spot lead_2_acc_all_ = false; seen_ = false; - //seen_ = new bool(false); - //bool_v[nb_node++] = seen_; - } duplicator_node_delayed::~duplicator_node_delayed() @@ -240,8 +229,6 @@ namespace spot // We take the min of the progress measure of the successor node // because we are on a duplicator. - //std::cout << "duplicator_node_delayed::set_win" << std::endl; - if (lnode_succ->size() == 0) progress_measure_ = nb_spoiler_loose_ + 1; @@ -251,11 +238,14 @@ namespace spot bool change; int tmpmin = 0; int tmp = 0; + int tmpminwin = -1; sn_v::iterator i = lnode_succ->begin(); if (i != lnode_succ->end()) { tmpmin = dynamic_cast(*i)->get_progress_measure(); + if (dynamic_cast(*i)->get_lead_2_acc_all()) + tmpminwin = tmpmin; ++i; } for (; i != lnode_succ->end(); ++i) @@ -263,7 +253,12 @@ namespace spot tmp = dynamic_cast(*i)->get_progress_measure(); if (tmp < tmpmin) tmpmin = tmp; + if (dynamic_cast(*i)->get_lead_2_acc_all() && + (tmp > tmpminwin)) + tmpminwin = tmp; } + if (tmpminwin != -1) + tmpmin = tmpminwin; change = (progress_measure_ < tmpmin); progress_measure_ = tmpmin; @@ -280,7 +275,14 @@ namespace spot << " [shape=box, label=\"(" << a->format_state(sc_->first) << ", " - << a->format_state(sc_->second); + << a->format_state(sc_->second) + << ", "; + if (label_ == bddfalse) + os << "0"; + else if (label_ == bddtrue) + os << "1"; + else + bdd_print_acc(os, a->get_dict(), label_); //<< ", "; //bdd_print_acc(os, a->get_dict(), acc_); os << ")" @@ -315,14 +317,12 @@ namespace spot bool duplicator_node_delayed::get_lead_2_acc_all() { - //std::cout << "duplicator_node_delayed::get_lead_2_acc_all" << std::endl; return lead_2_acc_all_; } bool duplicator_node_delayed::set_lead_2_acc_all(bdd acc) { - //std::cout << "duplicator_node_delayed::set_lead_2_acc_all" << std::endl; acc |= acc_; if (!seen_) { @@ -397,20 +397,14 @@ namespace spot build_recurse_successor_spoiler(spoiler_node* sn, std::ostringstream& os) { - //std::cout << os.str() << "build_recurse_successor_spoiler : begin" - //<< std::endl; - // FIXME if (sn == 0) return; tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); - //int i = 0; for (si->first(); !si->done(); si->next()) { - //std::cout << "transition " << i++ << std::endl; - bdd btmp = si->current_acceptance_conditions() | dynamic_cast(sn)-> get_acceptance_condition_visited(); @@ -445,9 +439,6 @@ namespace spot } delete si; - - //std::cout << os.str() << "build_recurse_successor_spoiler : end" - //<< std::endl; } void @@ -456,43 +447,15 @@ namespace spot spoiler_node* , std::ostringstream& os) { - /* - std::cout << os.str() << "build_recurse_successor_duplicator : begin" - << std::endl; - */ - tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); for (si->first(); !si->done(); si->next()) { - /* - std::cout << automata_->format_state(dn->get_spoiler_node()) - << std::endl; - std::cout << automata_->format_state(dn->get_duplicator_node()) - << std::endl; - */ - - /* - bdd_print_acc(std::cout, - automata_->get_dict(), - si->current_condition()); - std::cout << " // "; - bdd_print_acc(std::cout, - automata_->get_dict(), - dn->get_label()); - std::cout << " // "; - bdd_print_acc(std::cout, - automata_->get_dict(), - si->current_condition() | !dn->get_label()); - std::cout << std::endl; - */ - // if si->current_condition() doesn't implies dn->get_label() // then duplicator can't play. if ((si->current_condition() | !dn->get_label()) != bddtrue) { - //std::cout << "doesn't implies" << std::endl; continue; } @@ -528,11 +491,6 @@ namespace spot } delete si; - - /* - std::cout << os.str() << "build_recurse_successor_duplicator : end" - << std::endl; - */ } duplicator_node_delayed* @@ -600,41 +558,45 @@ namespace spot void parity_game_graph_delayed::lift() { - // TEST of the hash_map of node - /* - for (Sgi::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - seen_node_[*i] = 1; - - for (Sgi::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - seen_node_[*i] = 1; - */ - // - - // Before the lift we compute each vertices // to know if he belong to a all accepting cycle // of the graph. - /* FIXME + if (this->nb_set_acc_cond() > 1) - for (Sgi::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - for (Sgi::vector::iterator i2 - = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - dynamic_cast(*i2)->seen_ = false; - for (Sgi::vector::iterator i3 - = spoiler_vertice_.begin(); - i3 != spoiler_vertice_.end(); ++i3) - dynamic_cast(*i3)->seen_ = false; - dynamic_cast(*i)->set_lead_2_acc_all(); - } - */ + { + for (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end(); ++i) + { + /* + for (Sgi::vector::iterator i2 + = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + dynamic_cast(*i2)->seen_ = false; + for (Sgi::vector::iterator i3 + = spoiler_vertice_.begin(); + i3 != spoiler_vertice_.end(); ++i3) + dynamic_cast(*i3)->seen_ = false; + */ + dynamic_cast(*i)->set_lead_2_acc_all(); + } + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + /* + for (Sgi::vector::iterator i2 + = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + dynamic_cast(*i2)->seen_ = false; + for (Sgi::vector::iterator i3 + = spoiler_vertice_.begin(); + i3 != spoiler_vertice_.end(); ++i3) + dynamic_cast(*i3)->seen_ = false; + */ + dynamic_cast(*i)->set_lead_2_acc_all(); + } + } // Jurdzinski's algorithm //int iter = 0; @@ -667,12 +629,17 @@ namespace spot state_couple* p = 0; seen_map::iterator j; + if (this->nb_set_acc_cond() > 1) + return rel; + for (Sgi::vector::iterator i = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) { - if (dynamic_cast(*i)->get_progress_measure() - < nb_spoiler_loose_ + 1) + if ((dynamic_cast(*i)->get_progress_measure() + < nb_spoiler_loose_ + 1) && + (dynamic_cast(*i) + ->get_acceptance_condition_visited() == bddfalse)) { p = new state_couple((*i)->get_spoiler_node(), (*i)->get_duplicator_node()); @@ -702,18 +669,8 @@ namespace spot : parity_game_graph(a) { nb_spoiler_loose_ = 0; - - /* FIXME - if (this->nb_set_acc_cond() > 1) - return; - */ - - //std::cout << "build couple" << std::endl; this->build_graph(); - //std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl; this->lift(); - //std::cout << "lift end : " << nb_spoiler_loose_ << std::endl; - //std::cout << "END" << std::endl; } /////////////////////////////////////////// diff --git a/src/tgbaalgos/tarjan_on_fly.cc b/src/tgbaalgos/tarjan_on_fly.cc new file mode 100644 index 000000000..104fc2cc0 --- /dev/null +++ b/src/tgbaalgos/tarjan_on_fly.cc @@ -0,0 +1,258 @@ +// 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) + { + if ((*i).s) + delete (*i).s; + if ((*i).lasttr) + delete (*i).lasttr; + } + } + + ce::counter_example* + tarjan_on_fly::check() + { + std::cout << "tarjan_on_fly::check()" << std::endl; + + clock(); + + top = dftop = -1; + violation = false; + + const state* s = a->get_init_state(); + push(s); + + while (!violation && dftop >= 0) + { + //std::cout << "iter while" << std::endl; + s = stack[dftop].s; + std::cout << "s : " << a->format_state(s) << std::endl; + tgba_succ_iterator* iter = stack[dftop].lasttr; + if (iter == 0) + { + iter = a->succ_iter(s); + //std::cout << "iter->first" << std::endl; + iter->first(); + stack[dftop].lasttr = iter; + } + else + { + //std::cout << "iter->next" << std::endl; + iter->next(); + } + + const state* succ = 0; + if (!iter->done()) + { + succ = iter->current_state(); + if (h.find(succ) == h.end()) + push(succ); + else + { + int pos = in_stack(succ); + delete succ; + if (pos != -1) // succ is in stack + lowlinkupdate(dftop, pos); + } + } + else + pop(); + } + + tps_ = clock(); + if (violation) + return build_counter(); + + //std::cout << "NO COUNTER EXAMPLE FOUND" << std::endl; + + return 0; + } + + void + tarjan_on_fly::push(const state* s) + { + std::cout << "tarjan_on_fly::push() : " + << a->format_state(s) << " : " << std::endl; + + h[s] = 1; + top++; + + struct_state ss = { s, 0, top, dftop, 0, 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; + + /* + std::cout << " lowlink : " << ss.lowlink << std::endl; + std::cout << " pre : " << ss.pre << std::endl; + std::cout << " acc : " << ss.acc << std::endl; + */ + + if (top < (int)stack.size()) + { + std::cout << "MAJ" << std::endl; + + /* + const state* sdel = stack[top].s; + tgba_succ_iterator* iter = stack[top].lasttr; + */ + + stack[top] = ss; + + /* + delete sdel; + if (iter) + delete iter; + */ + + } + else + { + std::cout << "INS" << std::endl; + stack.push_back(ss); + } + + dftop = top; + } + + void + tarjan_on_fly::pop() + { + std::cout << "tarjan_on_fly::pop()" << std::endl; + + 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) + { + /* + std::cout << "tarjan_on_fly::lowlinkupdate() : " << std::endl + << " stack[t].lowlink : " << stack[t].lowlink + << " stack[f].lowlink : " << stack[f].lowlink + << " stack[f].acc : " << stack[f].acc + << std::endl; + */ + + if (stack[t].lowlink <= stack[f].lowlink) + { + if (stack[t].lowlink <= stack[f].acc) + { + violation = true; + std::cout << "VIOLATION DETECTED" << std::endl; + } + stack[f].lowlink = stack[t].lowlink; + } + } + + int + tarjan_on_fly::in_stack(const state* s) const + { + std::cout << "tarjan_on_fly::in_stack() : " + << a->format_state(s) << std::endl; + + 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; + } + + ce::counter_example* + tarjan_on_fly::build_counter() + { + std::cout << "tarjan_on_fly::build_counter()" << std::endl; + + ce = new ce::counter_example(a); + + stack_type::iterator i; + for (i = stack.begin(); i != stack.end(); ++i) + { + if (x && x->compare((*i).s) == 0) + break; + + //os << " " << a->format_state(i->first) << std::endl; + + ce->prefix.push_back(ce::state_ce((*i).s->clone(), + //bddtrue)); + (*i).lasttr->current_condition())); + } + + for (; i != stack.end(); ++i) + { + //os << " " << a->format_state(i->first) << std::endl; + + ce->cycle.push_back(ce::state_ce((*i).s->clone(), + //bddtrue)); + (*i).lasttr->current_condition())); + } + + return ce; + } + + std::ostream& + tarjan_on_fly::print_stat(std::ostream& os) const + { + int ce_size = 0; + if (ce) + ce_size = ce->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/tarjan_on_fly.hh b/src/tgbaalgos/tarjan_on_fly.hh new file mode 100644 index 000000000..f59e266e6 --- /dev/null +++ b/src/tgbaalgos/tarjan_on_fly.hh @@ -0,0 +1,94 @@ +// 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" +//#include "tgba/bddprint.hh" +#include "tgbaalgos/minimalce.hh" + +namespace spot +{ + + class tarjan_on_fly: public emptyness_search + { + + public: + + tarjan_on_fly(const tgba_tba_proxy *a); + virtual ~tarjan_on_fly(); + + /// \brief Find a counter example. + virtual ce::counter_example* 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; + + int pos; + }; + + //typedef std::pair state_iter_pair; + typedef Sgi::hash_map hash_type; + hash_type h; ///< Map of visited states. + + + //typedef std::pair pair_type; + 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; + ce::counter_example* ce; + + void push(const state* s); + void pop(); + void lowlinkupdate(int f, int t); + int in_stack(const state* s) const; + + ce::counter_example* build_counter(); + clock_t tps_; + + }; + +} + +#endif // SPOT_TGBAALGOS_MINIMALCE_HH diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 1f0c38c70..183d3d8c2 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -27,6 +27,13 @@ set -e expect_ce() { + run 0 ./ltl2tgba -ms -f "$1" + run 0 ./ltl2tgba -m -f "$1" + run 0 ./ltl2tgba -ndfs -f "$1" + #run 0 ./ltl2tgba -ndfs2 -f "$1" + run 0 ./ltl2tgba -tj -f "$1" + run 0 ./ltl2tgba -c -f "$1" + run 0 ./ltl2tgba -e "$1" run 0 ./ltl2tgba -e -D "$1" run 0 ./ltl2tgba -e -f "$1" @@ -35,12 +42,19 @@ expect_ce() 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 -mold "$1" + run 0 ./ltl2tgba -mold -f "$1" } expect_no() { + run 0 ./ltl2tgba -Ms -f "$1" + run 0 ./ltl2tgba -M -f "$1" + run 0 ./ltl2tgba -Ndfs -f "$1" + run 0 ./ltl2tgba -Ndfs2 -f "$1" + run 0 ./ltl2tgba -TJ -f "$1" + run 0 ./ltl2tgba -C -f "$1" + run 0 ./ltl2tgba -E "$1" run 0 ./ltl2tgba -E -D "$1" run 0 ./ltl2tgba -E -f "$1" @@ -53,6 +67,9 @@ expect_no() run 0 ./ltl2tgba -M -f "$1" } +#expect_no '!((FF a) <=> (F a))' +#expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' + 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 3a070adb5..25135ecf6 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -35,6 +35,10 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgbaalgos/magic.hh" +#include "tgbaalgos/nesteddfs.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" @@ -51,67 +55,95 @@ syntax(char* prog) << " "<< prog << " -X [OPTIONS...] file" << std::endl << std::endl << "Options:" << std::endl - << " -a display the acceptance_conditions BDD, not the " + << " -a display the acceptance_conditions BDD, not the " << "reachability graph" << std::endl - << " -A same as -a, but as a set" << std::endl - << " -d turn on traces during parsing" << std::endl - << " -D degeneralize the automaton" << std::endl - << " -e emptiness-check (Couvreur), expect and compute " - << "a counter-example" << std::endl - << " -e2 emptiness-check (Couvreur variant), expect and compute " - << "a counter-example" << std::endl - << " -E emptiness-check (Couvreur), expect no counter-example " + << " -A same as -a, but as a set" << std::endl + << " -c color-search (implies -D), expect a counter-example" << std::endl - << " -E2 emptiness-check (Couvreur variant), expect no " + << " -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 " + << "a counter-example" << std::endl + << " -e2 emptiness-check (Couvreur variant), expect and compute " + << "a counter-example" << std::endl + << " -E emptiness-check (Couvreur), expect no counter-example " + << std::endl + << " -E2 emptiness-check (Couvreur variant), expect no " << "counter-example " << std::endl - << " -f use Couvreur's FM algorithm for translation" + << " -f use Couvreur's FM algorithm for translation" << std::endl - << " -F read the formula from the file" << std::endl - << " -L fair-loop approximation (implies -f)" << std::endl - << " -m magic-search (implies -D), expect a counter-example" + << " -F read the formula from the file" << std::endl + << " -L fair-loop approximation (implies -f)" << std::endl + << " -m magic-search (implies -D), expect a counter-example" << std::endl - << " -M magic-search (implies -D), expect no counter-example" + << " -ms minmimal-search (implies -D), expect a counter-example" << std::endl - << " -n same as -m, but display more counter-examples" + << " -mold magic-search (implies -D), expect a counter-example" << std::endl - << " -N display the never clain for Spin " + << " -M magic-search (implies -D), expect no counter-example" + << std::endl + << " -Mold magic-search (implies -D), expect no counter-example" + << 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 + << " -n same as -m, but display more counter-examples" + << std::endl + << " -N display the never clain for Spin " << "(implies -D)" << std::endl - << " -p branching postponement (implies -f)" << std::endl - << " -r display the relation BDD, not the reachability graph" + << " -p branching postponement (implies -f)" << std::endl + << " -r display the relation BDD, not the reachability graph" << std::endl - << " -r1 reduce formula using basic rewriting" << std::endl - << " -r2 reduce formula using class of eventuality and " + << " -r1 reduce formula using basic rewriting" << std::endl + << " -r2 reduce formula using class of eventuality and " << "and universality" << std::endl - << " -r3 reduce formula using implication between " + << " -r3 reduce formula using implication between " << "sub-formulae" << std::endl - << " -r4 reduce formula using all rules" << std::endl - << " -rd display the reduce formula" << std::endl - << " -R same as -r, but as a set" << std::endl - << " -R1 use direct simulation to reduce the automata " + << " -r4 reduce formula using all rules" << std::endl + << " -rd display the reduce formula" << std::endl + << " -R same as -r, but as a set" << std::endl + << " -R1 use direct simulation to reduce the automata " << "(use -L for more reduction)" << std::endl - << " -R2 use delayed simulation to reduce the automata " + << " -R2 use delayed simulation to reduce the automata " << "(use -L for more reduction)" << std::endl - << " -R3 use SCC to reduce the automata" + << " -R3 use SCC to reduce the automata" << std::endl - << " -Rd display the simulation relation" + << " -Rd display the simulation relation" << std::endl - << " -RD display the parity game (dot format)" + << " -RD display the parity game (dot format)" << std::endl - << " -s convert to explicit automata, and number states " + << " -s convert to explicit automata, and number states " << "in DFS order" << std::endl - << " -S convert to explicit automata, and number states " + << " -S convert to explicit automata, and number states " << "in BFS order" << std::endl - << " -t display reachable states in LBTT's format" << std::endl - << " -v display the BDD variables used by the automaton" + << " -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 - << " -x try to produce a more deterministic automaton " + << " -TJ tarjan-on-fly (implies -D), expect no counter-example" + << std::endl + << " -v display the BDD variables used by the automaton" + << std::endl + << " -x try to produce a more deterministic automata " << "(implies -f)" << std::endl - << " -X do not compute an automaton, read it from a file" + << " -X do not compute an automaton, read it from a file" << std::endl - << " -y do not merge states with same symbolic representation " + << " -y do not merge states with same symbolic representation " << "(implies -f)" << std::endl; exit(2); } @@ -129,7 +161,12 @@ main(int argc, char** argv) bool file_opt = false; int output = 0; int formula_index = 0; - enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None; + enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld, + NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch, + TarjanOnFly, MinimalSearch} echeck = None; + spot::emptyness_search* es = 0; + //int opt_search = 0; //FIXME + spot::search_opt opt_nested_search = spot::magic; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; bool expect_counter_example = false; @@ -157,6 +194,22 @@ main(int argc, char** argv) { output = 4; } + else if (!strcmp(argv[formula_index], "-c")) + { + echeck = ColorDFSSearch; + //opt_search = 0; + 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; @@ -202,23 +255,92 @@ main(int argc, char** argv) fair_loop_approx = true; fm_opt = true; } - else if (!strcmp(argv[formula_index], "-m")) + else if (!strcmp(argv[formula_index], "-mold")) { - echeck = MagicSearch; + echeck = MagicSearchOld; + //opt_search = 0; degeneralize_opt = true; expect_counter_example = true; output = -1; } + else if (!strcmp(argv[formula_index], "-m")) + { + opt_nested_search = spot::magic; + echeck = MagicSearch; + //opt_search = 0; + degeneralize_opt = true; + expect_counter_example = true; + output = -1; + //magic_many = true; + } + else if (!strcmp(argv[formula_index], "-ms")) + { + echeck = MinimalSearch; + degeneralize_opt = true; + expect_counter_example = true; + output = -1; + } + else if (!strcmp(argv[formula_index], "-Mold")) + { + echeck = MagicSearchOld; // FIXME + degeneralize_opt = true; + expect_counter_example = false; + output = -1; + } 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], "-Ms")) + { + echeck = MinimalSearch; + degeneralize_opt = true; + expect_counter_example = false; + output = -1; + } + else if (!strcmp(argv[formula_index], "-ndfs")) + { + opt_nested_search = spot::nested; + echeck = NestedDFSSearch; + //opt_search = 1; + degeneralize_opt = true; + expect_counter_example = true; + output = -1; + } + else if (!strcmp(argv[formula_index], "-Ndfs")) + { + opt_nested_search = spot::nested; + echeck = NestedDFSSearch; + //opt_search = 1; + degeneralize_opt = true; + expect_counter_example = false; + output = -1; + } + else if (!strcmp(argv[formula_index], "-ndfs2")) + { + opt_nested_search = spot::my_nested; + echeck = NestedDFSSearchModify; + //opt_search = 2; + degeneralize_opt = true; + expect_counter_example = true; + output = -1; + } + else if (!strcmp(argv[formula_index], "-Ndfs2")) + { + opt_nested_search = spot::my_nested; + echeck = NestedDFSSearchModify; + //opt_search = 2; + degeneralize_opt = true; + expect_counter_example = false; + output = -1; + } else if (!strcmp(argv[formula_index], "-n")) { - echeck = MagicSearch; + echeck = MagicSearchOld; degeneralize_opt = true; expect_counter_example = true; output = -1; @@ -260,10 +382,12 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-R1")) { + //degeneralize_opt = true; // FIXME reduc_aut |= spot::Reduce_Dir_Sim; } else if (!strcmp(argv[formula_index], "-R2")) { + //degeneralize_opt = true; // FIXME reduc_aut |= spot::Reduce_Del_Sim; } else if (!strcmp(argv[formula_index], "-R3")) @@ -294,6 +418,20 @@ 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 (!strcmp(argv[formula_index], "-v")) { output = 5; @@ -497,6 +635,7 @@ main(int argc, char** argv) { case None: break; + case Couvreur: case Couvreur2: { @@ -505,9 +644,7 @@ main(int argc, char** argv) ec = new spot::emptiness_check(a); else ec = new spot::emptiness_check_shy(a); - bool res = ec->check(); - if (expect_counter_example) { if (res) @@ -517,7 +654,12 @@ main(int argc, char** argv) break; } spot::counter_example ce(ec->result()); - ce.print_result(std::cout); + //ce.print_result(std::cout); + spot::ce::counter_example* res2 = ce.get_counter_example(); + spot::tgba* aut = res2->ce2tgba(); + spot::dotty_reachable(std::cout, aut); + delete res2; + delete aut; } else { @@ -526,7 +668,8 @@ main(int argc, char** argv) delete ec; } break; - case MagicSearch: + + case MagicSearchOld: { spot::magic_search ms(degeneralized); bool res = ms.check(); @@ -547,8 +690,68 @@ main(int argc, char** argv) } } break; + + case ColorDFSSearch: + es = new spot::colordfs_search(degeneralized); + break; + + case TarjanOnFly: + es = new spot::tarjan_on_fly(degeneralized); + break; + + case MinimalSearch: + es = new spot::minimalce_search(degeneralized); + break; + + case MagicSearch: + case NestedDFSSearch: + case NestedDFSSearchModify: + es = new spot::nesteddfs_search(degeneralized, opt_nested_search); + break; + } + 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)