From c938e652e4716dfe0b5a84ff8c9e256c11830274 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 8 Apr 2011 15:57:19 +0200 Subject: [PATCH] DVE2: preliminary implementation of compressed states. * iface/dve2/dve2.cc (dve2_compressed_state): New class. (callback_context): Deal with general state*s, not dve2_state*s. (transition_callback_compress): New function. (dve2_kripke): Take a compress option. (get_init_state, compute_state_condition, succ_iter, format_state, state_condition): Handle compressed states. (get_vars, compute_state_condition_aux): New helper methods. * iface/dve2/dve2.hh (load_dve2): Add a compress option. * iface/dve2/dve2check.cc: Add a -z option. * iface/dve2/finite.test, iface/dve2/dve2check.test: Add more tests. --- ChangeLog | 16 +++ iface/dve2/dve2.cc | 227 ++++++++++++++++++++++++++++++-------- iface/dve2/dve2.hh | 1 + iface/dve2/dve2check.cc | 16 ++- iface/dve2/dve2check.test | 25 +++-- iface/dve2/finite.test | 5 + src/tgbatest/intvcomp.cc | 20 ++++ 7 files changed, 254 insertions(+), 56 deletions(-) diff --git a/ChangeLog b/ChangeLog index 80cf1ea52..aad956e1d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2011-04-08 Alexandre Duret-Lutz + + DVE2: preliminary implementation of compressed states. + + * iface/dve2/dve2.cc (dve2_compressed_state): New class. + (callback_context): Deal with general state*s, not dve2_state*s. + (transition_callback_compress): New function. + (dve2_kripke): Take a compress option. + (get_init_state, compute_state_condition, succ_iter, + format_state, state_condition): Handle compressed states. + (get_vars, compute_state_condition_aux): New helper methods. + * iface/dve2/dve2.hh (load_dve2): Add a compress option. + * iface/dve2/dve2check.cc: Add a -z option. + * iface/dve2/finite.test, iface/dve2/dve2check.test: Add more + tests. + 2011-04-08 Alexandre Duret-Lutz Preliminary implementation of an int array compressor. diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 3cbe42aa3..65607c60a 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -26,9 +26,10 @@ #include #include +#include "dve2.hh" #include "misc/hashfunc.hh" #include "misc/fixpool.hh" -#include "dve2.hh" +#include "misc/intvcomp.hh" namespace spot @@ -127,12 +128,87 @@ namespace spot int vars[0]; }; + struct dve2_compressed_state: public state + { + dve2_compressed_state(fixed_size_pool* p) + : count(1), pool(p) + { + } + + void compute_hash() + { + hash_value = 0; + std::vector::const_iterator i; + for (i = data->begin(); i != data->end(); ++i) + hash_value = wang32_hash(hash_value ^ *i); + } + + dve2_compressed_state* clone() const + { + ++count; + return const_cast(this); + } + + void destroy() const + { + if (--count) + return; + delete data; + pool->deallocate(this); + } + + size_t hash() const + { + return hash_value; + } + + int compare(const state* other) const + { + if (this == other) + return 0; + const dve2_compressed_state* o = + down_cast(other); + assert(o); + if (hash_value < o->hash_value) + return -1; + if (hash_value > o->hash_value) + return 1; + + if (data->size() < o->data->size()) + return -1; + if (data->size() > o->data->size()) + return 1; + + std::pair::const_iterator, + std::vector::const_iterator> r; + r = std::mismatch(data->begin(), data->end(), o->data->begin()); + if (r.first == data->end()) + return 0; + if (*(r.first) < *(r.second)) + return -1; + else + return 1; + } + + private: + + ~dve2_compressed_state() + { + } + + public: + mutable unsigned count; + size_t hash_value; + fixed_size_pool* pool; + const std::vector* data; + }; + //////////////////////////////////////////////////////////////////////// // CALLBACK FUNCTION for transitions. struct callback_context { - typedef std::vector transitions_t; // FIXME: Vector->List + typedef std::vector transitions_t; // FIXME: Vector->List transitions_t transitions; int state_size; fixed_size_pool* pool; @@ -155,6 +231,18 @@ namespace spot ctx->transitions.push_back(out); } + void transition_callback_compress(void* arg, transition_info_t*, int *dst) + { + callback_context* ctx = static_cast(arg); + + dve2_compressed_state* out = + new(ctx->pool->allocate()) dve2_compressed_state(ctx->pool); + out->data = int_array_compress(dst, ctx->state_size); + // std::cerr << "dest " << out->data << std::endl; + out->compute_hash(); + ctx->transitions.push_back(out); + } + //////////////////////////////////////////////////////////////////////// // SUCC_ITERATOR @@ -507,11 +595,15 @@ namespace spot public: dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps, - const ltl::formula* dead) + const ltl::formula* dead, bool compress) : d_(d), state_size_(d_->get_state_variable_count()), dict_(dict), ps_(ps), - statepool_(sizeof(dve2_state) + state_size_ * sizeof(int)), + compress_(compress), + uncompressed_(compress ? new int[state_size_] : + 0), + statepool_(compress ? sizeof(dve2_compressed_state) : + (sizeof(dve2_state) + state_size_ * sizeof(int))), state_condition_last_state_(0), state_condition_last_cc_(0) { vname_ = new const char*[state_size_]; @@ -552,6 +644,8 @@ namespace spot ~dve2_kripke() { delete[] vname_; + if (compress_) + delete[] uncompressed_; lt_dlclose(d_->handle); dict_->unregister_all_my_variables(d_); @@ -569,34 +663,35 @@ namespace spot state* get_init_state() const { fixed_size_pool* p = const_cast(&statepool_); - dve2_state* res = new(p->allocate()) dve2_state(state_size_, p); - d_->get_initial_state(res->vars); - res->compute_hash(); - return res; + if (compress_) + { + dve2_compressed_state* res = + new(p->allocate()) dve2_compressed_state(p); + d_->get_initial_state(uncompressed_); + res->data = int_array_compress(uncompressed_, state_size_); + // std::cerr << "init " << res->data << std::endl; + res->compute_hash(); + return res; + } + else + { + dve2_state* res = new(p->allocate()) dve2_state(state_size_, p); + d_->get_initial_state(res->vars); + res->compute_hash(); + return res; + } } bdd - compute_state_condition(const dve2_state* s) const + compute_state_condition_aux(const int* vars) const { - // If we just computed it, don't do it twice. - if (s == state_condition_last_state_) - return state_condition_last_cond_; - - if (state_condition_last_state_) - { - state_condition_last_state_->destroy(); - delete state_condition_last_cc_; // Might be 0 already. - state_condition_last_cc_ = 0; - } - bdd res = bddtrue; for (prop_set::const_iterator i = ps_->begin(); i != ps_->end(); ++i) { - int l = s->vars[i->var_num]; + int l = vars[i->var_num]; int r = i->val; - bool cond = false; switch (i->op) { @@ -625,12 +720,35 @@ namespace spot else res &= bdd_nithvar(i->bddvar); } + return res; + } + + bdd + compute_state_condition(const state* st) const + { + // If we just computed it, don't do it twice. + if (st == state_condition_last_state_) + return state_condition_last_cond_; + + if (state_condition_last_state_) + { + state_condition_last_state_->destroy(); + delete state_condition_last_cc_; // Might be 0 already. + state_condition_last_cc_ = 0; + } + + const int* vars = get_vars(st); + + bdd res = compute_state_condition_aux(vars); callback_context* cc = new callback_context; cc->state_size = state_size_; cc->pool = const_cast(&statepool_); - int t = d_->get_successors(0, const_cast(s->vars), - transition_callback, cc); + int t = d_->get_successors(0, const_cast(vars), + compress_ + ? transition_callback_compress + : transition_callback, + cc); assert((unsigned)t == cc->transitions.size()); state_condition_last_cc_ = cc; @@ -644,28 +762,47 @@ namespace spot // Add a self-loop to dead-states if we care about these. if (res != bddfalse) - cc->transitions.push_back(s->clone()); + cc->transitions.push_back(st->clone()); } state_condition_last_cond_ = res; - state_condition_last_state_ = s->clone(); + state_condition_last_state_ = st->clone(); return res; } + const int* + get_vars(const state* st) const + { + const int* vars; + if (compress_) + { + const dve2_compressed_state* s = + down_cast(st); + assert(s); + + int_array_decompress(s->data, uncompressed_, state_size_); + vars = uncompressed_; + } + else + { + const dve2_state* s = down_cast(st); + assert(s); + vars = s->vars; + } + return vars; + } + + virtual dve2_succ_iterator* succ_iter(const state* local_state, const state*, const tgba*) const { - const dve2_state* s = down_cast(local_state); - assert(s); - // This may also compute successors in state_condition_last_cc - bdd scond = compute_state_condition(s); + bdd scond = compute_state_condition(local_state); callback_context* cc; - if (state_condition_last_cc_) { cc = state_condition_last_cc_; @@ -673,16 +810,21 @@ namespace spot } else { + const int* vars = get_vars(local_state); + cc = new callback_context; cc->state_size = state_size_; cc->pool = const_cast(&statepool_); - int t = d_->get_successors(0, const_cast(s->vars), - transition_callback, cc); + int t = d_->get_successors(0, const_cast(vars), + compress_ + ? transition_callback_compress + : transition_callback, + cc); assert((unsigned)t == cc->transitions.size()); // Add a self-loop to dead-states if we care about these. if (t == 0 && scond != bddfalse) - cc->transitions.push_back(s->clone()); + cc->transitions.push_back(local_state->clone()); } return new dve2_succ_iterator(cc, scond); @@ -692,16 +834,13 @@ namespace spot bdd state_condition(const state* st) const { - const dve2_state* s = down_cast(st); - assert(s); - return compute_state_condition(s); + return compute_state_condition(st); } virtual std::string format_state(const state *st) const { - const dve2_state* s = down_cast(st); - assert(s); + const int* vars = get_vars(st); std::stringstream res; @@ -711,7 +850,7 @@ namespace spot int i = 0; for (;;) { - res << vname_[i] << "=" << s->vars[i]; + res << vname_[i] << "=" << vars[i]; ++i; if (i == state_size_) break; @@ -734,7 +873,8 @@ namespace spot const prop_set* ps_; bdd alive_prop; bdd dead_prop; - + bool compress_; + int* uncompressed_; fixed_size_pool statepool_; // This cache is used to speedup repeated calls to state_condition() @@ -742,7 +882,7 @@ namespace spot // If state_condition_last_state_ != 0, then state_condition_last_cond_ // contain its (recently computed) condition. If additionally // state_condition_last_cc_ != 0, then it contains the successors. - mutable const dve2_state* state_condition_last_state_; + mutable const state* state_condition_last_state_; mutable bdd state_condition_last_cond_; mutable callback_context* state_condition_last_cc_; }; @@ -804,6 +944,7 @@ namespace spot load_dve2(const std::string& file_arg, bdd_dict* dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead, + bool compress, bool verbose) { std::string file; @@ -914,6 +1055,6 @@ namespace spot return 0; } - return new dve2_kripke(d, dict, ps, dead); + return new dve2_kripke(d, dict, ps, dead, compress); } } diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh index 8026bbfbd..9516b6bd3 100644 --- a/iface/dve2/dve2.hh +++ b/iface/dve2/dve2.hh @@ -61,6 +61,7 @@ namespace spot bdd_dict* dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead = ltl::constant::true_instance(), + bool compress = false, bool verbose = true); } diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index f289f032d..db63f9c74 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -58,7 +58,9 @@ syntax(char* prog) << std::endl << " -gp output the product state-space in dot format" << std::endl - << " -T time the different phases of the execution" + << " -T time the different phases of the execution" + << std::endl + << " -z compress states to handle larger models" << std::endl; exit(1); @@ -76,6 +78,7 @@ main(int argc, char **argv) bool accepting_run = false; bool expect_counter_example = false; char *dead = 0; + bool compress_states = false; const char* echeck_algo = "Cou99"; @@ -124,6 +127,9 @@ main(int argc, char **argv) case 'T': use_timer = true; break; + case 'z': + compress_states = true; + break; default: error: std::cerr << "Unknown option `" << argv[i] << "'." << std::endl; @@ -198,7 +204,7 @@ main(int argc, char **argv) if (output != DotFormula) { tm.start("loading dve2"); - model = spot::load_dve2(argv[1], dict, &ap, deadf, true); + model = spot::load_dve2(argv[1], dict, &ap, deadf, compress_states, true); tm.stop("loading dve2"); if (!model) @@ -256,6 +262,7 @@ main(int argc, char **argv) assert(ec); do { + int memused = spot::memusage(); tm.start("running emptiness check"); spot::emptiness_check_result* res; try @@ -266,12 +273,17 @@ main(int argc, char **argv) { std::cerr << "Out of memory during emptiness check." << std::endl; + if (!compress_states) + std::cerr << "Try option -z for state compression." << std::endl; exit_code = 2; exit(exit_code); } tm.stop("running emptiness check"); + memused = spot::memusage() - memused; ec->print_stats(std::cout); + std::cout << memused << " pages allocated for emptiness check" + << std::endl; if (expect_counter_example == !res && (!expect_counter_example || ec->safe())) diff --git a/iface/dve2/dve2check.test b/iface/dve2/dve2check.test index 66f2cd0ab..036f8e965 100755 --- a/iface/dve2/dve2check.test +++ b/iface/dve2/dve2check.test @@ -33,19 +33,22 @@ fi set -e -# The three examples from the README. -# (Don't run the first one using "run 0" because it would take too much -# time with valgrind.). -../dve2check -e $srcdir/beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' -run 0 ../dve2check -E $srcdir/beem-peterson.4.dve \ - '!G(P_0.wait -> F P_0.CS)' > stdout1 -# same formula, different syntax. -run 0 ../dve2check -E $srcdir/beem-peterson.4.dve \ - '!G("P_0 == wait" -> F "P_0 == CS")' > stdout2 -cmp stdout1 stdout2 -run 0 ../dve2check -E $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' +for opt in '' '-z'; do + # The three examples from the README. + # (Don't run the first one using "run 0" because it would take too much + # time with valgrind.). + ../dve2check $opt -e $srcdir/beem-peterson.4.dve \ + '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' + run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ + '!G(P_0.wait -> F P_0.CS)' > stdout1 + # same formula, different syntax. + run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ + '!G("P_0 == wait" -> F "P_0 == CS")' > stdout2 + cmp stdout1 stdout2 + run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' +done # Now check some error messages. run 1 ../dve2check foo.dve "F(P_0.CS)" 2>stderr diff --git a/iface/dve2/finite.test b/iface/dve2/finite.test index b2f50e83d..2725f0e76 100755 --- a/iface/dve2/finite.test +++ b/iface/dve2/finite.test @@ -43,6 +43,11 @@ run 0 ../dve2check -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout test "`grep ' -> ' stdout | wc -l`" = 19 test "`grep 'P=0' stdout | wc -l`" = 15 +# the same with compressed states +run 0 ../dve2check -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout +test "`grep ' -> ' stdout | wc -l`" = 19 +test "`grep 'P=0' stdout | wc -l`" = 15 + run 0 ../dve2check -ddead -e $srcdir/finite.dve \ '!(G(dead -> ("P.a==3" | "P.b==3")))' diff --git a/src/tgbatest/intvcomp.cc b/src/tgbatest/intvcomp.cc index 6462b081c..85c79f0ac 100644 --- a/src/tgbatest/intvcomp.cc +++ b/src/tgbatest/intvcomp.cc @@ -1,3 +1,23 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). +// +// 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 "misc/intvcomp.hh" #include