From bf8becccea9aeca4773d0a18e24ab183b687e66c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 1 May 2011 20:52:12 +0200 Subject: [PATCH] DVE2: Optionally use the new compression. * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc: Add a -Z option and pass it through. --- ChangeLog | 7 +++++++ iface/dve2/dve2.cc | 29 ++++++++++++++++++----------- iface/dve2/dve2.hh | 2 +- iface/dve2/dve2check.cc | 10 ++++++++-- 4 files changed, 34 insertions(+), 14 deletions(-) diff --git a/ChangeLog b/ChangeLog index c3c0e796c..7de46f4ca 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-05-01 Alexandre Duret-Lutz + + DVE2: Optionally use the new compression. + + * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc: + Add a -Z option and pass it through. + 2011-05-01 Alexandre Duret-Lutz Implement a new compression inspired from simple-9. diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 527eaec8d..cad15940b 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -31,6 +31,7 @@ #include "misc/fixpool.hh" #include "misc/mspool.hh" #include "misc/intvcomp.hh" +#include "misc/intvcmp2.hh" namespace spot @@ -200,11 +201,12 @@ namespace spot struct callback_context { - typedef std::vector transitions_t; // FIXME: Vector->List + typedef std::list transitions_t; transitions_t transitions; int state_size; void* pool; int* compressed; + void (*compress)(const int*, size_t, int*, size_t&); ~callback_context() { @@ -231,7 +233,7 @@ namespace spot multiple_size_pool* p = static_cast(ctx->pool); size_t csize = ctx->state_size * 2; - int_array_array_compress(dst, ctx->state_size, ctx->compressed, csize); + ctx->compress(dst, ctx->state_size, ctx->compressed, csize); void* mem = p->allocate(sizeof(dve2_compressed_state) + sizeof(int) * csize); @@ -593,12 +595,17 @@ namespace spot public: dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps, - const ltl::formula* dead, bool compress) + const ltl::formula* dead, int compress) : d_(d), state_size_(d_->get_state_variable_count()), dict_(dict), ps_(ps), - compress_(compress), - uncompressed_(compress ? new int[state_size_] : 0), + compress_(compress == 0 ? 0 + : compress == 1 ? int_array_array_compress + : int_array_array_compress2), + decompress_(compress == 0 ? 0 + : compress == 1 ? int_array_array_decompress + : int_array_array_decompress2), + uncompressed_(compress ? new int[state_size_ + 30] : 0), compressed_(compress ? new int[state_size_ * 2] : 0), statepool_(compress ? sizeof(dve2_compressed_state) : (sizeof(dve2_state) + state_size_ * sizeof(int))), @@ -667,8 +674,7 @@ namespace spot { d_->get_initial_state(uncompressed_); size_t csize = state_size_ * 2; - int_array_array_compress(uncompressed_, state_size_, - compressed_, csize); + compress_(uncompressed_, state_size_, compressed_, csize); multiple_size_pool* p = const_cast(&compstatepool_); @@ -739,6 +745,7 @@ namespace spot const_cast(compress_ ? static_cast(&compstatepool_) : static_cast(&statepool_)); + cc->compress = compress_; cc->compressed = compressed_; t = d_->get_successors(0, const_cast(vars), compress_ @@ -799,8 +806,7 @@ namespace spot down_cast(st); assert(s); - int_array_array_decompress(s->vars, s->size, - uncompressed_, state_size_); + decompress_(s->vars, s->size, uncompressed_, state_size_); vars = uncompressed_; } else @@ -883,7 +889,8 @@ namespace spot const prop_set* ps_; bdd alive_prop; bdd dead_prop; - bool compress_; + void (*compress_)(const int*, size_t, int*, size_t&); + void (*decompress_)(const int*, size_t, int*, size_t); int* uncompressed_; int* compressed_; fixed_size_pool statepool_; @@ -956,7 +963,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, + int compress, bool verbose) { std::string file; diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh index 9516b6bd3..93d738c60 100644 --- a/iface/dve2/dve2.hh +++ b/iface/dve2/dve2.hh @@ -61,7 +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, + int compress = 0, bool verbose = true); } diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index db63f9c74..f7512d957 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -61,6 +61,9 @@ syntax(char* prog) << " -T time the different phases of the execution" << std::endl << " -z compress states to handle larger models" + << std::endl + << " -Z compress states (faster) " + << "assuming all values in [0 .. 2^28-1]" << std::endl; exit(1); @@ -78,7 +81,7 @@ main(int argc, char **argv) bool accepting_run = false; bool expect_counter_example = false; char *dead = 0; - bool compress_states = false; + int compress_states = 0; const char* echeck_algo = "Cou99"; @@ -128,7 +131,10 @@ main(int argc, char **argv) use_timer = true; break; case 'z': - compress_states = true; + compress_states = 1; + break; + case 'Z': + compress_states = 2; break; default: error: