diff --git a/ChangeLog b/ChangeLog index cc7d469b3..6d50a756f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2003-07-28 Alexandre Duret-Lutz + + * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc + (tgba_tba_proxy::state_is_accepting): New method. + * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files. + * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, + tgbaalgos_HEADERS): Add them. + * src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files. + * src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES, + check_PROGRAMS): Add them. + 2003-07-25 Alexandre Duret-Lutz * src/tgba/tgba.hh (tgba::~tgba): Make it public. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 862d2ad20..5d19724c6 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -27,7 +27,7 @@ namespace spot { } - virtual + virtual ~state_tba_proxy() { delete s_; @@ -45,7 +45,7 @@ namespace spot return acc_; } - virtual int + virtual int compare(const state* other) const { const state_tba_proxy* o = dynamic_cast(other); @@ -55,8 +55,8 @@ namespace spot return res; return acc_.id() - o->accepting_cond().id(); } - - virtual + + virtual state_tba_proxy* clone() const { return new state_tba_proxy(*this); @@ -75,7 +75,7 @@ namespace spot tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, bdd acc, bdd next_acc, bdd the_accepting_cond) - : it_(it), acc_(acc), next_acc_(next_acc), + : it_(it), acc_(acc), next_acc_(next_acc), the_accepting_cond_(the_accepting_cond) { } @@ -87,19 +87,19 @@ namespace spot // iteration - void + void first() { it_->first(); } - void + void next() { it_->next(); } - bool + bool done() const { return it_->done(); @@ -107,14 +107,14 @@ namespace spot // inspection - state_tba_proxy* + state_tba_proxy* current_state() const { state* s = it_->current_state(); bdd acc; // Transition in the ACC_ accepting set should be directed // to the NEXT_ACC_ accepting set. - if (acc_ == bddtrue + if (acc_ == bddtrue || (acc_ & it_->current_accepting_conditions()) == acc_) acc = next_acc_; else @@ -122,13 +122,13 @@ namespace spot return new state_tba_proxy(s, acc); } - bdd + bdd current_condition() const { return it_->current_condition(); } - bdd + bdd current_accepting_conditions() const { return the_accepting_cond_; @@ -176,7 +176,7 @@ namespace spot get_dict()->unregister_all_my_variables(this); } - state* + state* tgba_tba_proxy::get_init_state() const { cycle_map::const_iterator i = acc_cycle_.find(bddtrue); @@ -189,62 +189,71 @@ namespace spot const state* global_state, const tgba* global_automaton) const { - const state_tba_proxy* s = + const state_tba_proxy* s = dynamic_cast(local_state); assert(s); - tgba_succ_iterator* it = a_->succ_iter(s->real_state(), + tgba_succ_iterator* it = a_->succ_iter(s->real_state(), global_state, global_automaton); bdd acc = s->accepting_cond(); cycle_map::const_iterator i = acc_cycle_.find(acc); assert(i != acc_cycle_.end()); - return + return new tgba_tba_proxy_succ_iterator(it, acc, i->second, - (acc == bddtrue) + (acc == bddtrue) ? the_accepting_cond_ : bddfalse); } - - bdd_dict* + + bdd_dict* tgba_tba_proxy::get_dict() const { return a_->get_dict(); } - - std::string + + std::string tgba_tba_proxy::format_state(const state* state) const { - const state_tba_proxy* s = + const state_tba_proxy* s = dynamic_cast(state); assert(s); - return a_->format_state(s->real_state()) + "(" + return a_->format_state(s->real_state()) + "(" + bdd_format_set(get_dict(), s->accepting_cond()) + ")"; } - - bdd + + bdd tgba_tba_proxy::all_accepting_conditions() const { return the_accepting_cond_; } - - bdd + + bdd tgba_tba_proxy::neg_accepting_conditions() const { return !the_accepting_cond_; } - - bdd + + bool + tgba_tba_proxy::state_is_accepting(const state* state) const + { + const state_tba_proxy* s = + dynamic_cast(state); + assert(s); + return bddtrue == s->accepting_cond(); + } + + bdd tgba_tba_proxy::compute_support_conditions(const state* state) const { - const state_tba_proxy* s = + const state_tba_proxy* s = dynamic_cast(state); assert(s); return a_->support_conditions(s->real_state()); } - - bdd + + bdd tgba_tba_proxy::compute_support_variables(const state* state) const { - const state_tba_proxy* s = + const state_tba_proxy* s = dynamic_cast(state); assert(s); return a_->support_variables(s->real_state()); diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 825bec6c2..46946eacd 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -44,6 +44,8 @@ namespace spot virtual bdd all_accepting_conditions() const; virtual bdd neg_accepting_conditions() const; + bool state_is_accepting(const state* state) const; + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 5b68e4a99..1f6d9dd24 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -8,6 +8,7 @@ tgbaalgos_HEADERS = \ dotty.hh \ lbtt.hh \ ltl2tgba.hh \ + magic.hh \ save.hh noinst_LTLIBRARIES = libtgbaalgos.la @@ -16,4 +17,5 @@ libtgbaalgos_la_SOURCES = \ dotty.cc \ lbtt.cc \ ltl2tgba.cc \ + magic.cc \ save.cc diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc new file mode 100644 index 000000000..0738c5ee8 --- /dev/null +++ b/src/tgbaalgos/magic.cc @@ -0,0 +1,143 @@ +#include +#include "magic.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + + const unsigned char seen_without_magic = 1; + const unsigned char seen_with_magic = 2; + + magic_search::magic_search(const tgba_tba_proxy* a) + : a(a), x(0) + { + } + + magic_search::~magic_search() + { + for (hash_type::iterator i = h.begin(); i != h.end(); ++i) + delete i->first; + if (x) + delete x; + } + + void + magic_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 }; + h[s] = d; + } + else + { + hi->second.seen_without |= !m; + hi->second.seen_with |= m; + if (hi->first != s) + delete s; + s = hi->first; + } + + magic_state ms = { s, m }; + stack.push_front(state_iter_pair(ms, i)); + } + + bool + magic_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 + magic_search::check() + { + 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: + magic_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(); + bdd c = i->current_condition(); + i->next(); + if (magic && 0 == s_prime->compare(x)) + { + delete s_prime; + tstack.push_front(c); + assert(stack.size() == tstack.size()); + return true; + } + if (! has(s_prime, magic)) + { + push(s_prime, magic); + tstack.push_front(c); + goto recurse; + } + delete s_prime; + } + + const state* s = p.first.s; + 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(); + } + + assert(tstack.empty()); + return false; + } + + std::ostream& + magic_search::print_result(std::ostream& os) 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:" <format_state(i->first.s) << std::endl; + os << " | " << bdd_format_set(d, *ti) << std::endl; + } + os << " " << a->format_state(x) << std::endl; + return os; + } + +} diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh new file mode 100644 index 000000000..9cfd8a131 --- /dev/null +++ b/src/tgbaalgos/magic.hh @@ -0,0 +1,98 @@ +#ifndef SPOT_TGBAALGOS_MAGIC_HH +# define SPOT_TGBAALGOS_MAGIC_HH + +#include +#include +#include +#include "tgba/tgbatba.hh" + +namespace spot +{ + /// \brief Emptiness check on spot::tgba_tba_proxy automata using + /// the Magic Search algorithm. + /// + /// This algorithm comes from + /// \verbatim + /// @InProceedings{ godefroid.93.pstv, + /// author = {Patrice Godefroid and Gerard .J. Holzmann}, + /// title = {On the verification of temporal properties}, + /// booktitle = {Proceedings of the 13th IFIP TC6/WG6.1 International + /// Symposium on Protocol Specification, Testing, and + /// Verification (PSTV'93)}, + /// month = {May}, + /// editor = {Andr{\'e} A. S. Danthine and Guy Leduc + /// and Pierre Wolper}, + /// address = {Liege, Belgium}, + /// pages = {109--124}, + /// publisher = {North-Holland}, + /// year = {1993}, + /// series = {IFIP Transactions}, + /// volume = {C-16}, + /// isbn = {0-444-81648-8} + /// } + /// \endverbatim + struct magic_search + { + /// Initialize the Magic Search algorithm on the automaton \a a. + magic_search(const tgba_tba_proxy *a); + ~magic_search(); + + /// \brief Perform a Magic 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. + bool check(); + + /// Print the last accepting path found. + std::ostream& print_result(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; + }; + + /// \brief A state for the spot::magic_search algorithm. + struct magic_state + { + const state* s; + bool m; ///< The state of the magic demon. + }; + + 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; + + // FIXME: use a hash_map. + typedef std::map hash_type; + hash_type h; ///< Map of visited states. + + /// Append a new state to the current path. + void 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; + + const tgba_tba_proxy* a; ///< The automata to check. + /// The state for which we are currently seeking an SCC. + const state* x; + }; + + +} + +#endif // SPOT_TGBAALGOS_MAGIC_HH diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index 1ae41702d..a1b482e8c 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -15,3 +15,4 @@ explprod tripprod mixprod spotlbtt +ltlmagic diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 9d72aec5e..4f6d7dcdc 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -4,16 +4,17 @@ LDADD = ../libspot.la check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ - explicit \ - readsave \ - tgbaread \ - ltl2tgba \ - ltlprod \ bddprod \ + explicit \ explprod \ - tripprod \ + ltl2tgba \ + ltlmagic \ + ltlprod \ mixprod \ - spotlbtt + readsave \ + spotlbtt \ + tgbaread \ + tripprod # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc @@ -21,6 +22,7 @@ bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT explicit_SOURCES = explicit.cc explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc +ltlmagic_SOURCES = ltlmagic.cc ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc readsave_SOURCES = readsave.cc @@ -40,7 +42,8 @@ TESTS = \ explprod.test \ tripprod.test \ mixprod.test \ - spotlbtt.test + spotlbtt.test \ + ltlmagic.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/ltlmagic.cc b/src/tgbatest/ltlmagic.cc new file mode 100644 index 000000000..91af123c9 --- /dev/null +++ b/src/tgbatest/ltlmagic.cc @@ -0,0 +1,77 @@ +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/magic.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " formula" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + int formula_index = 0; + bool all_opt = false; + + for (;;) + { + if (argc < formula_index + 1) + syntax(argv[0]); + + ++formula_index; + + if (!strcmp(argv[formula_index], "-a")) + { + all_opt = true; + } + else + { + break; + } + } + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + + spot::ltl::parse_error_list pel1; + spot::ltl::formula* f1 = spot::ltl::parse(argv[formula_index], pel1, env); + + if (spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel1)) + return 2; + + spot::bdd_dict* dict = new spot::bdd_dict(); + { + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_tba_proxy* a2 = new spot::tgba_tba_proxy(a1); + spot::ltl::destroy(f1); + + spot::magic_search ms(a2); + + if (ms.check()) + { + do + ms.print_result (std::cout); + while (all_opt && ms.check()); + } + else + { + exit_code = 1; + } + + delete a2; + delete a1; + } + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + delete dict; + return exit_code; +} diff --git a/src/tgbatest/ltlmagic.test b/src/tgbatest/ltlmagic.test new file mode 100755 index 000000000..de4f4f4ad --- /dev/null +++ b/src/tgbatest/ltlmagic.test @@ -0,0 +1,15 @@ +#!/bin/sh + +. ./defs + +set -e + +./ltlmagic a +./ltlmagic 0 || test $? = 1 +./ltlmagic 'a & !a' || test $? = 1 +./ltlmagic 'a U b' +./ltlmagic '!(a U b)' +./ltlmagic '!(a U b) & !(!a R !b)' || test $? = 1 +# Expect four satisfactions +test `./ltlmagic -a 'FFx <=> Fx' | grep Prefix: | wc -l` = 4 +./ltlmagic '!(FFx <=> Fx)' || test $? = 1