diff --git a/ChangeLog b/ChangeLog index fc1062ee7..3c2a63d24 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-11-15 Poitrenaud Denis + + * src/tgbaalgos/magic.cc: Add a bit state hashing version. + * src/tgbaalgos/se05.cc: Add a bit state hashing version. + * src/tgbaalgos/magic.hh: Make them public. + * src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks. + * src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test. + * src/tgbatest/dfs.test: Introduce new characteristic explicit tests. + 2004-11-14 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in: Add options to check the produced diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 1cc4ec055..a56f6f512 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include #include "misc/hash.hh" #include @@ -42,8 +43,8 @@ namespace spot /// /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). - magic_search(const tgba *a) - : a(a), all_cond(a->all_acceptance_conditions()) + magic_search(const tgba *a, size_t size) + : h(size), a(a), all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -165,7 +166,7 @@ namespace spot /// The automata to check. const tgba* a; - /// The automata to check. + /// The unique accepting condition of the automaton \a a. bdd all_cond; bool dfs_blue() @@ -181,7 +182,7 @@ namespace spot bdd acc = f.it->current_acceptance_conditions(); f.it->next(); typename heap::color_ref c = h.get_color_ref(s_prime); - if (c.is_null()) + if (c.is_white()) // Go down the edge (f.s, , s_prime) { ++nbn; @@ -202,6 +203,8 @@ namespace spot if (dfs_red()) return true; } + else + h.pop_notify(s_prime); } } else @@ -213,7 +216,7 @@ namespace spot delete f.it; st_blue.pop_front(); typename heap::color_ref c = h.get_color_ref(f_dest.s); - assert(!c.is_null()); + assert(!c.is_white()); if (c.get() == BLUE && f_dest.acc == all_cond && !st_blue.empty()) // the test 'c.get() == BLUE' is added to limit @@ -251,10 +254,10 @@ namespace spot bdd acc = f.it->current_acceptance_conditions(); f.it->next(); typename heap::color_ref c = h.get_color_ref(s_prime); - if (c.is_null()) + if (c.is_white()) // Notice that this case is taken into account only to // support successive calls to the check method. Without - // this functionnality, one can check assert(c.is_null()). + // this functionnality, one can check assert(c.is_white()). // Go down the edge (f.s, , s_prime) { ++nbn; @@ -270,6 +273,8 @@ namespace spot if (target->compare(s_prime) == 0) return true; } + else + h.pop_notify(s_prime); } } else // Backtrack @@ -342,16 +347,16 @@ namespace spot color_ref(color* c) :p(c) { } - int get() const + color get() const { return *p; } void set(color c) { - assert(!is_null()); + assert(!is_white()); *p=c; } - bool is_null() const + bool is_white() const { return p==0; } @@ -359,7 +364,7 @@ namespace spot color *p; }; - explicit_magic_search_heap() + explicit_magic_search_heap(size_t) { } @@ -405,11 +410,78 @@ namespace spot hash_type h; }; + class bsh_magic_search_heap + { + public: + class color_ref + { + public: + color_ref(unsigned char *b, unsigned char o): base(b), offset(o*2) + { + } + color get() const + { + return color(((*base) >> offset) & 3U); + } + void set(color c) + { + *base = (*base & ~(3U << offset)) | (c << offset); + } + bool is_white() const + { + return get()==WHITE; + } + private: + unsigned char *base; + unsigned char offset; + }; + + bsh_magic_search_heap(size_t s) + { + size = s; + h = new unsigned char[size]; + memset(h, WHITE, size); + } + + ~bsh_magic_search_heap() + { + delete[] h; + } + + color_ref get_color_ref(const state*& s) + { + size_t ha = s->hash(); + return color_ref(&(h[ha%size]), ha%4); + } + + void add_new_state(const state* s, color c) + { + color_ref cr(get_color_ref(s)); + assert(cr.is_white()); + cr.set(c); + } + + void pop_notify(const state* s) + { + delete s; + } + + private: + size_t size; + unsigned char* h; + }; + } // anonymous emptiness_check* explicit_magic_search(const tgba *a) { - return new magic_search(a); + return new magic_search(a, 0); + } + + emptiness_check* bit_state_hashing_magic_search( + const tgba *a, size_t size) + { + return new magic_search(a, size); } } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 975b292d2..40770bd10 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -27,19 +27,19 @@ namespace spot { - /// \brief Returns an emptiness check on the spot::tgba automaton \a a. + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker stores explicitely all + /// the traversed states. /// /// \pre The automaton \a a must have at most one accepting condition (i.e. /// it is a TBA). /// /// The method \a check() of the returned checker can be called several times /// (until it returns a null pointer) to enumerate all the visited accepting - /// paths. The method visits only a finite set of accepting paths. - /// - /// The implemented algorithm is the following. + /// paths. The implemented algorithm is the following. /// /// \verbatim - /// procedure nested_dfs () + /// procedure check () /// begin /// call dfs_blue(s0); /// end; @@ -72,8 +72,8 @@ namespace spot /// end; /// \endverbatim /// - /// It is an adaptation to TBA of the Magic Search algorithm - /// which deals with accepting states and is presented in + /// This algorithm is an adaptation to TBA of the one + /// (which deals with accepting states) presented in /// /// \verbatim /// Article{ courcoubertis.92.fmsd, @@ -87,20 +87,35 @@ namespace spot /// volume = {1} /// } /// \endverbatim + /// emptiness_check* explicit_magic_search(const tgba *a); + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker does not store explicitely + /// the traversed states but uses the bit state hashing technic. However, the + /// implemented algorithm is the same as the one of + /// spot::explicit_magic_search. + /// + /// \pre The automaton \a a must have at most one accepting condition (i.e. + /// it is a TBA). + /// + /// \sa spot::explicit_magic_search + /// + emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size); + /// \brief Returns an emptiness check on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker stores explicitely all + /// the traversed states. /// /// \pre The automaton \a a must have at most one accepting condition (i.e. /// it is a TBA). /// /// The method \a check() of the returned checker can be called several times /// (until it returns a null pointer) to enumerate all the visited accepting - /// paths. The method visits only a finite set of accepting paths. + /// paths. The implemented algorithm is the following: /// - /// The implemented algorithm is the following: - /// - /// procedure nested_dfs () + /// \verbatim + /// procedure check () /// begin /// weight = 0; /// call dfs_blue(s0); @@ -143,8 +158,9 @@ namespace spot /// end if; /// end for; /// end; + /// \endverbatim /// - /// It is an adaptation to TBA and an extension of the one + /// It is an adaptation to TBA (and a slight extension) of the one /// presented in /// \verbatim /// InProceedings{ schwoon.05.tacas, @@ -159,12 +175,27 @@ namespace spot /// } /// \endverbatim /// - /// the extention consists in the introduction of a weight associated - /// to each state in the blue stack. The weight represents the number of - /// accepting arcs traversed to reach it from the initial state. + /// The extention consists in the introduction of a weight associated + /// to each state in the blue stack (the cyan states). The weight of a + /// cyan state corresponds to the number of accepting arcs traversed to reach + /// it from the initial state. Weights are used to detect accepting cycle in + /// the blue dfs. /// emptiness_check* explicit_se05_search(const tgba *a); + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker does not store explicitely + /// the traversed states but uses the bit state hashing technic. However, the + /// implemented algorithm is the same as the one of + /// spot::explicit_se05_search. + /// + /// \pre The automaton \a a must have at most one accepting condition (i.e. + /// it is a TBA). + /// + /// \sa spot::explicit_se05_search + /// + emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size); + } #endif // SPOT_TGBAALGOS_MAGIC_HH diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 2a0898f02..88a2ab7a5 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -42,8 +42,9 @@ namespace spot /// /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). - se05_search(const tgba *a) - : current_weight(0), a(a), all_cond(a->all_acceptance_conditions()) + se05_search(const tgba *a, size_t size) + : current_weight(0), h(size), + a(a), all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -82,7 +83,7 @@ namespace spot assert(st_blue.empty()); const state* s0 = a->get_init_state(); ++nbn; - h.add_new_state(s0, CYAN); + h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) return new result(*this); @@ -182,7 +183,7 @@ namespace spot bdd acc = f.it->current_acceptance_conditions(); f.it->next(); typename heap::color_ref c = h.get_color_ref(s_prime); - if (c.is_null()) + if (c.is_white()) // Go down the edge (f.s, , s_prime) { if (acc == all_cond) @@ -211,6 +212,8 @@ namespace spot if (dfs_red()) return true; } + else + h.pop_notify(s_prime); } } else @@ -224,7 +227,7 @@ namespace spot if (f_dest.acc == all_cond) --current_weight; typename heap::color_ref c = h.get_color_ref(f_dest.s); - assert(!c.is_null()); + assert(!c.is_white()); if (c.get() == BLUE && f_dest.acc == all_cond && !st_blue.empty()) // the test 'c.get() == BLUE' is added to limit @@ -262,10 +265,10 @@ namespace spot bdd acc = f.it->current_acceptance_conditions(); f.it->next(); typename heap::color_ref c = h.get_color_ref(s_prime); - if (c.is_null()) + if (c.is_white()) // Notice that this case is taken into account only to // support successive calls to the check method. Without - // this functionnality => assert(c.is_null()) + // this functionnality => assert(c.is_white()) // Go down the edge (f.s, , s_prime) { ++nbn; @@ -285,6 +288,8 @@ namespace spot c.set(RED); push(st_red, s_prime, label, acc); } + else + h.pop_notify(s_prime); } } else // Backtrack @@ -372,10 +377,10 @@ namespace spot : is_cyan(false), weight(0), ph(0), phc(0), ps(0), pc(c) { } - int get() const + color get() const { if (is_cyan) - return CYAN; // the color cyan is fixed to 0 + return CYAN; return *pc; } int get_weight() const @@ -385,10 +390,12 @@ namespace spot } void set(color c) { - assert(!is_null()); + assert(!is_white()); if (is_cyan) { - phc->erase(ps); + int i = phc->erase(ps); + assert(i==1); + (void)i; ph->insert(std::make_pair(ps, c)); } else @@ -396,7 +403,7 @@ namespace spot *pc=c; } } - bool is_null() const + bool is_white() const { return !is_cyan && pc==0; } @@ -409,7 +416,7 @@ namespace spot color *pc; // point to the color of a state stored in main hash table }; - explicit_se05_search_heap() + explicit_se05_search_heap(size_t) { } @@ -454,9 +461,10 @@ namespace spot return color_ref(&h, &hc, ic->first, ic->second); // cyan state } - void add_new_state(const state* s, color c, int w=0) + void add_new_state(const state* s, color c, int w=-1) { assert(hc.find(s)==hc.end() && h.find(s)==h.end()); + assert(c!=CYAN || w>=0); if (c == CYAN) hc.insert(std::make_pair(s, w)); else @@ -469,7 +477,111 @@ namespace spot private: - hash_type h; + hash_type h; // associate to each blue and red state its color + hcyan_type hc; // associate to each cyan state its weight + }; + + class bsh_se05_search_heap + { + private: + typedef Sgi::hash_map hcyan_type; + public: + class color_ref + { + public: + color_ref(hcyan_type* h, const state* st, int w, + unsigned char *base, unsigned char offset) + : is_cyan(true), weight(w), phc(h), ps(st), b(base), o(offset*2) + { + } + color_ref(unsigned char *base, unsigned char offset) + : is_cyan(false), weight(0), phc(0), ps(0), b(base), o(offset*2) + { + } + color get() const + { + if (is_cyan) + return CYAN; + return color(((*b) >> o) & 3U); + } + int get_weight() const + { + assert(is_cyan); + return weight; + } + void set(color c) + { + if (is_cyan && c!=CYAN) + { + int i = phc->erase(ps); + assert(i==1); + (void)i; + } + *b = (*b & ~(3U << o)) | (c << o); + } + bool is_white() const + { + return !is_cyan && get()==WHITE; + } + const unsigned char* base() const + { + return b; + } + unsigned char offset() const + { + return o; + } + private: + bool is_cyan; + int weight; + hcyan_type* phc; + const state* ps; + unsigned char *b; + unsigned char o; + }; + + bsh_se05_search_heap(size_t s) : size(s) + { + h = new unsigned char[size]; + memset(h, WHITE, size); + } + + ~bsh_se05_search_heap() + { + delete[] h; + } + + color_ref get_color_ref(const state*& s) + { + size_t ha = s->hash(); + hcyan_type::iterator ic = hc.find(s); + if (ic!=hc.end()) + return color_ref(&hc, ic->first, ic->second, &h[ha%size], ha%4); + return color_ref(&h[ha%size], ha%4); + } + + void add_new_state(const state* s, color c, int w=-1) + { + assert(c!=CYAN || w>=0); + assert(get_color_ref(s).is_white()); + if (c==CYAN) + hc.insert(std::make_pair(s, w)); + else + { + color_ref cr(get_color_ref(s)); + cr.set(c); + } + } + + void pop_notify(const state* s) + { + delete s; + } + + private: + size_t size; + unsigned char* h; hcyan_type hc; }; @@ -477,7 +589,12 @@ namespace spot emptiness_check* explicit_se05_search(const tgba *a) { - return new se05_search(a); + return new se05_search(a, 0); + } + + emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size) + { + return new se05_search(a, size); } } diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test index 98e557c15..e3cf62d41 100755 --- a/src/tgbatest/dfs.test +++ b/src/tgbatest/dfs.test @@ -25,6 +25,14 @@ set -e +# All examples are TBA (i.e. they have a unique +# accepting condition). Accepting arcs are +# represented by double arrows. +# +# s1=>s2->s3->(large composant from s4 to s9) +# ^ | +# |_______| + cat >blue_counter <<'EOF' acc = a; s1, s2,, a; @@ -72,6 +80,11 @@ EOF run 0 ./ltl2tgba -emagic_search -X blue_counter run 0 ./ltl2tgba -ese05_search -X blue_counter +# s1->s2->s3->(large composant from s4 to s9) +# ^ || +# ||______|| +# ||______|| + cat >blue_last <<'EOF' acc = a; s1, s2,,; @@ -119,6 +132,14 @@ EOF run 0 ./ltl2tgba -emagic_search -X blue_last run 0 ./ltl2tgba -ese05_search -X blue_last +# _______ +# | | +# | v +# s1->s2->s3->(large composant from s4 to s9) +# || ^ +# ||______|| +# ||______|| + cat >red <<'EOF' acc = a; s1, s2,,; diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index b77d55497..940e6efb1 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -43,8 +43,12 @@ expect_ce() expect_ce_do -ecouvreur99_shy -f -D "$1" expect_ce_do -emagic_search "$1" expect_ce_do -emagic_search -f "$1" + run 0 ./ltl2tgba -ebsh_magic_search "$1" + run 0 ./ltl2tgba -ebsh_magic_search -f "$1" run 0 ./ltl2tgba -ese05_search "$1" run 0 ./ltl2tgba -ese05_search -f "$1" + run 0 ./ltl2tgba -ebsh_se05_search "$1" + run 0 ./ltl2tgba -ebsh_se05_search -f "$1" # Expect multiple accepting runs test `./ltl2tgba -emagic_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 test `./ltl2tgba -ese05_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 @@ -62,8 +66,12 @@ expect_no() run 0 ./ltl2tgba -Ecouvreur99_shy -f -D "$1" run 0 ./ltl2tgba -Emagic_search "$1" run 0 ./ltl2tgba -Emagic_search -f "$1" + run 0 ./ltl2tgba -Ebsh_magic_search "$1" + run 0 ./ltl2tgba -Ebsh_magic_search -f "$1" run 0 ./ltl2tgba -Ese05_search "$1" run 0 ./ltl2tgba -Ese05_search -f "$1" + run 0 ./ltl2tgba -Ebsh_se05_search "$1" + run 0 ./ltl2tgba -Ebsh_se05_search -f "$1" test `./ltl2tgba -emagic_search_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 test `./ltl2tgba -ese05_search_repeated "!($1)" | diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index fa53d25c9..da7fb8cc7 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -115,8 +115,16 @@ syntax(char* prog) << " couvreur99_shy" << std::endl << " magic_search" << std::endl << " magic_search_repeated" << std::endl + << " bsh_magic_search[(heap size in Mo - 10Mo by default)]" + << std::endl + << " bsh_magic_search_repeated[(heap size in MB - 10MB" + << " by default)]" << std::endl << " se05_search" << std::endl - << " se05_search_repeated" << std::endl; + << " se05_search_repeated" << std::endl + << " bsh_se05_search[(heap size in MB - 10MB by default)]" + << std::endl + << " bsh_se05_search_repeated[(heap size in MB - 10MB" + << " by default)]" << std::endl; exit(2); } @@ -134,9 +142,11 @@ main(int argc, char** argv) int output = 0; int formula_index = 0; std::string echeck_algo; - enum { None, Couvreur, Couvreur2, MagicSearch, Se04Search } echeck = None; + enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; + bool bit_state_hashing = false; + int heap_size = 10*1024*1024; bool expect_counter_example = false; bool from_file = false; int reduc_aut = spot::Reduce_None; @@ -174,23 +184,33 @@ main(int argc, char** argv) degeneralize_opt = true; } else if (!strncmp(argv[formula_index], "-e", 2)) - { - if (argv[formula_index][2] != 0) - echeck_algo = argv[formula_index] + 2; - else - echeck_algo = "couvreur99"; - expect_counter_example = true; - output = -1; - } + { + if (argv[formula_index][2] != 0) + { + char *p = strchr(argv[formula_index], '('); + if (p && sscanf(p+1, "%d)", &heap_size) == 1) + *p = '\0'; + echeck_algo = argv[formula_index] + 2; + } + else + echeck_algo = "couvreur99"; + expect_counter_example = true; + output = -1; + } else if (!strncmp(argv[formula_index], "-E", 2)) - { - if (argv[formula_index][2] != 0) - echeck_algo = argv[formula_index] + 2; - else - echeck_algo = "couvreur99"; - expect_counter_example = false; - output = -1; - } + { + if (argv[formula_index][2] != 0) + { + char *p = strchr(argv[formula_index], '('); + if (p && sscanf(p+1, "%d)", &heap_size) == 1) + *p = '\0'; + echeck_algo = argv[formula_index] + 2; + } + else + echeck_algo = "couvreur99"; + expect_counter_example = false; + output = -1; + } else if (!strcmp(argv[formula_index], "-f")) { fm_opt = true; @@ -344,17 +364,43 @@ main(int argc, char** argv) degeneralize_opt = true; magic_many = true; } + else if (echeck_algo == "bsh_magic_search") + { + echeck = MagicSearch; + degeneralize_opt = true; + bit_state_hashing = true; + } + else if (echeck_algo == "bsh_magic_search_repeated") + { + echeck = MagicSearch; + degeneralize_opt = true; + bit_state_hashing = true; + magic_many = true; + } else if (echeck_algo == "se05_search") { - echeck = Se04Search; + echeck = Se05Search; degeneralize_opt = true; } else if (echeck_algo == "se05_search_repeated") { - echeck = Se04Search; + echeck = Se05Search; degeneralize_opt = true; magic_many = true; } + else if (echeck_algo == "bsh_se05_search") + { + echeck = Se05Search; + degeneralize_opt = true; + bit_state_hashing = true; + } + else if (echeck_algo == "bsh_se05_search_repeated") + { + echeck = Se05Search; + degeneralize_opt = true; + bit_state_hashing = true; + magic_many = true; + } else { std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl; @@ -575,15 +621,22 @@ main(int argc, char** argv) ec = new spot::couvreur99_check_shy(a); break; - case MagicSearch: - ec_a = degeneralized; - ec = spot::explicit_magic_search(degeneralized); - break; + case MagicSearch: + ec_a = degeneralized; + if (bit_state_hashing) + ec = spot::bit_state_hashing_magic_search( + degeneralized, heap_size); + else + ec = spot::explicit_magic_search(degeneralized); + break; - case Se04Search: - ec_a = degeneralized; - ec = spot::explicit_se05_search(degeneralized); - break; + case Se05Search: + ec_a = degeneralized; + if (bit_state_hashing) + ec = spot::bit_state_hashing_se05_search(degeneralized, heap_size); + else + ec = spot::explicit_se05_search(degeneralized); + break; } if (ec) @@ -593,13 +646,23 @@ main(int argc, char** argv) spot::emptiness_check_result* res = ec->check(); if (!graph_run_opt) ec->print_stats(std::cout); - if (expect_counter_example != !!res) + if (expect_counter_example != !!res && + (!bit_state_hashing || !expect_counter_example)) exit_code = 1; if (!res) { - std::cout << "no accepting run found" << std::endl; - break; + std::cout << "no accepting run found"; + if (bit_state_hashing && expect_counter_example) + { + std::cout << " even if expected" << std::endl; + std::cout << "this is maybe due to the use of the bit " + << "state hashing technic" << std::endl; + std::cout << "you can try to increase the heap size " + << "or use an explicit storage" << std::endl; + } + std::cout << std::endl; + break; } else {