Commit bf8beccc authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent a832eab1
2011-05-01 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-05-01 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Implement a new compression inspired from simple-9. Implement a new compression inspired from simple-9.
......
...@@ -31,6 +31,7 @@ ...@@ -31,6 +31,7 @@
#include "misc/fixpool.hh" #include "misc/fixpool.hh"
#include "misc/mspool.hh" #include "misc/mspool.hh"
#include "misc/intvcomp.hh" #include "misc/intvcomp.hh"
#include "misc/intvcmp2.hh"
namespace spot namespace spot
...@@ -200,11 +201,12 @@ namespace spot ...@@ -200,11 +201,12 @@ namespace spot
struct callback_context struct callback_context
{ {
typedef std::vector<state*> transitions_t; // FIXME: Vector->List typedef std::list<state*> transitions_t;
transitions_t transitions; transitions_t transitions;
int state_size; int state_size;
void* pool; void* pool;
int* compressed; int* compressed;
void (*compress)(const int*, size_t, int*, size_t&);
~callback_context() ~callback_context()
{ {
...@@ -231,7 +233,7 @@ namespace spot ...@@ -231,7 +233,7 @@ namespace spot
multiple_size_pool* p = static_cast<multiple_size_pool*>(ctx->pool); multiple_size_pool* p = static_cast<multiple_size_pool*>(ctx->pool);
size_t csize = ctx->state_size * 2; 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) void* mem = p->allocate(sizeof(dve2_compressed_state)
+ sizeof(int) * csize); + sizeof(int) * csize);
...@@ -593,12 +595,17 @@ namespace spot ...@@ -593,12 +595,17 @@ namespace spot
public: public:
dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps, 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), : d_(d),
state_size_(d_->get_state_variable_count()), state_size_(d_->get_state_variable_count()),
dict_(dict), ps_(ps), dict_(dict), ps_(ps),
compress_(compress), compress_(compress == 0 ? 0
uncompressed_(compress ? new int[state_size_] : 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), compressed_(compress ? new int[state_size_ * 2] : 0),
statepool_(compress ? sizeof(dve2_compressed_state) : statepool_(compress ? sizeof(dve2_compressed_state) :
(sizeof(dve2_state) + state_size_ * sizeof(int))), (sizeof(dve2_state) + state_size_ * sizeof(int))),
...@@ -667,8 +674,7 @@ namespace spot ...@@ -667,8 +674,7 @@ namespace spot
{ {
d_->get_initial_state(uncompressed_); d_->get_initial_state(uncompressed_);
size_t csize = state_size_ * 2; size_t csize = state_size_ * 2;
int_array_array_compress(uncompressed_, state_size_, compress_(uncompressed_, state_size_, compressed_, csize);
compressed_, csize);
multiple_size_pool* p = multiple_size_pool* p =
const_cast<multiple_size_pool*>(&compstatepool_); const_cast<multiple_size_pool*>(&compstatepool_);
...@@ -739,6 +745,7 @@ namespace spot ...@@ -739,6 +745,7 @@ namespace spot
const_cast<void*>(compress_ const_cast<void*>(compress_
? static_cast<const void*>(&compstatepool_) ? static_cast<const void*>(&compstatepool_)
: static_cast<const void*>(&statepool_)); : static_cast<const void*>(&statepool_));
cc->compress = compress_;
cc->compressed = compressed_; cc->compressed = compressed_;
t = d_->get_successors(0, const_cast<int*>(vars), t = d_->get_successors(0, const_cast<int*>(vars),
compress_ compress_
...@@ -799,8 +806,7 @@ namespace spot ...@@ -799,8 +806,7 @@ namespace spot
down_cast<const dve2_compressed_state*>(st); down_cast<const dve2_compressed_state*>(st);
assert(s); assert(s);
int_array_array_decompress(s->vars, s->size, decompress_(s->vars, s->size, uncompressed_, state_size_);
uncompressed_, state_size_);
vars = uncompressed_; vars = uncompressed_;
} }
else else
...@@ -883,7 +889,8 @@ namespace spot ...@@ -883,7 +889,8 @@ namespace spot
const prop_set* ps_; const prop_set* ps_;
bdd alive_prop; bdd alive_prop;
bdd dead_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* uncompressed_;
int* compressed_; int* compressed_;
fixed_size_pool statepool_; fixed_size_pool statepool_;
...@@ -956,7 +963,7 @@ namespace spot ...@@ -956,7 +963,7 @@ namespace spot
load_dve2(const std::string& file_arg, bdd_dict* dict, load_dve2(const std::string& file_arg, bdd_dict* dict,
const ltl::atomic_prop_set* to_observe, const ltl::atomic_prop_set* to_observe,
const ltl::formula* dead, const ltl::formula* dead,
bool compress, int compress,
bool verbose) bool verbose)
{ {
std::string file; std::string file;
......
...@@ -61,7 +61,7 @@ namespace spot ...@@ -61,7 +61,7 @@ namespace spot
bdd_dict* dict, bdd_dict* dict,
const ltl::atomic_prop_set* to_observe, const ltl::atomic_prop_set* to_observe,
const ltl::formula* dead = ltl::constant::true_instance(), const ltl::formula* dead = ltl::constant::true_instance(),
bool compress = false, int compress = 0,
bool verbose = true); bool verbose = true);
} }
......
...@@ -61,6 +61,9 @@ syntax(char* prog) ...@@ -61,6 +61,9 @@ syntax(char* prog)
<< " -T time the different phases of the execution" << " -T time the different phases of the execution"
<< std::endl << std::endl
<< " -z compress states to handle larger models" << " -z compress states to handle larger models"
<< std::endl
<< " -Z compress states (faster) "
<< "assuming all values in [0 .. 2^28-1]"
<< std::endl; << std::endl;
exit(1); exit(1);
...@@ -78,7 +81,7 @@ main(int argc, char **argv) ...@@ -78,7 +81,7 @@ main(int argc, char **argv)
bool accepting_run = false; bool accepting_run = false;
bool expect_counter_example = false; bool expect_counter_example = false;
char *dead = 0; char *dead = 0;
bool compress_states = false; int compress_states = 0;
const char* echeck_algo = "Cou99"; const char* echeck_algo = "Cou99";
...@@ -128,7 +131,10 @@ main(int argc, char **argv) ...@@ -128,7 +131,10 @@ main(int argc, char **argv)
use_timer = true; use_timer = true;
break; break;
case 'z': case 'z':
compress_states = true; compress_states = 1;
break;
case 'Z':
compress_states = 2;
break; break;
default: default:
error: error:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment