Commit 273cce37 authored by Etienne Renault's avatar Etienne Renault
Browse files

spins_kripke: rewrite, clean and document

Some parts of the kripke were confusing, lacked
of documentation or could be factorized. This patch
cleans all of this.

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
parent a947de25
......@@ -33,7 +33,6 @@
/// to build a kripke that is thread safe
namespace spot
{
/// \brief A Spins state is represented as an array of integer
/// Note that this array has two reserved slots (position 0 an 1).
///
......@@ -64,16 +63,33 @@ namespace spot
/// \brief The management of states (i.e. allocation/deallocation) can
/// be painless since every time we have to consider wether the state will
/// be compressed or not. This class aims to simplify this management
/// be compressed or not. This class aims to simplify this management.
class cspins_state_manager final
{
public:
/// \brief Build a manager for a state of \a state_size variables
/// and indicate wether compression should be used:
/// - 1 for handle large models
/// - 2 (faster) assume all values in [0 .. 2^28-1]
cspins_state_manager(unsigned int state_size, int compress);
/// \brief Get Rid of the internal representation of the state
int* unbox_state(cspins_state s) const;
// cmp is the area we can use to compute the compressed rep of dst.
cspins_state alloc_setup(int *dst, int* cmp, size_t cmpsize);
/// \brief Builder for a state from a raw description given in \a dst
///
/// \a cmp is the area we can use to compute the compressed
/// representatation of dst.
/// \a cmpsize the size of the previous area
cspins_state alloc_setup(int* dst, int* cmp, size_t cmpsize);
/// \brief Helper to decompress a state
void decompress(cspins_state s, int* uncompressed, unsigned size) const;
/// \brief Help the manager to reclam the memory of a state
void dealloc(cspins_state s);
/// \brief The size of a state
unsigned int size() const;
private:
......@@ -85,56 +101,67 @@ namespace spot
void (*fn_decompress_)(const int*, size_t, int*, size_t);
};
// This structure is used as a parameter during callback when
// generating states from the shared librarie produced by LTSmin
// \brief This structure is used as a parameter during callback when
// generating states from the shared librarie produced by LTSmin.
struct inner_callback_parameters
{
cspins_state_manager* manager; // The state manager
std::vector<cspins_state>* succ; // The successors of a state
int* compressed_;
int* uncompressed_;
bool compress;
bool selfloopize;
int* compressed; // Area to store compressed state
int* uncompressed; // Area to store uncompressed state
bool compress; // Should the state be compressed?
bool selfloopize; // Should the state be selfloopized
};
// This class provides an iterator over the successors of a state.
// All successors are computed once when an iterator is recycled or
// created.
/// \brief This class provides an iterator over the successors of a state.
/// All successors are computed once when an iterator is recycled or
/// created.
///
/// Note: Two threads will explore sucessors with two different orders
class cspins_iterator final
{
public:
// Inner struct used to pack the various arguments required by the iterator
struct cspins_iterator_param
{
cspins_state s;
const spot::spins_interface* d;
cspins_state_manager& manager;
inner_callback_parameters& inner;
cube cond;
bool compress;
bool selfloopize;
spot::cubeset& cubeset;
int dead_idx;
unsigned tid;
};
cspins_iterator(const cspins_iterator&) = delete;
cspins_iterator(cspins_iterator&) = delete;
cspins_iterator(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
inner_callback_parameters& inner,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset,
int dead_idx, unsigned tid);
void recycle(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
inner_callback_parameters& inner,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx, unsigned tid);
cspins_iterator(cspins_iterator_param& p);
void recycle(cspins_iterator_param& p);
~cspins_iterator();
void next();
bool done() const;
cspins_state state() const;
cube condition() const;
private:
/// Compute the real index in the successor vector
/// \brief Compute the real index in the successor vector
unsigned compute_index() const;
inline void setup_iterator(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
inner_callback_parameters& inner,
cube& cond,
bool compress,
bool selfloopize,
cubeset& cubeset,
int dead_idx);
std::vector<cspins_state> successors_;
unsigned int current_;
cube cond_;
......@@ -146,20 +173,36 @@ namespace spot
template<>
class kripkecube<cspins_state, cspins_iterator> final
{
typedef enum {
OP_EQ_VAR, OP_NE_VAR, OP_LT_VAR, OP_GT_VAR, OP_LE_VAR, OP_GE_VAR,
VAR_OP_EQ, VAR_OP_NE, VAR_OP_LT, VAR_OP_GT, VAR_OP_LE, VAR_OP_GE,
VAR_OP_EQ_VAR, VAR_OP_NE_VAR, VAR_OP_LT_VAR,
VAR_OP_GT_VAR, VAR_OP_LE_VAR, VAR_OP_GE_VAR, VAR_DEAD
} relop;
// Define operators that are available for atomic proposition
enum class relop
{
OP_EQ_VAR, // 1 == a
OP_NE_VAR, // 1 != a
OP_LT_VAR, // 1 < a
OP_GT_VAR, // 1 > a
OP_LE_VAR, // 1 <= a
OP_GE_VAR, // 1 >= a
VAR_OP_EQ, // a == 1
VAR_OP_NE, // a != 1
VAR_OP_LT, // a < 1
VAR_OP_GT, // a >= 1
VAR_OP_LE, // a <= 1
VAR_OP_GE, // a >= 1
VAR_OP_EQ_VAR, // a == b
VAR_OP_NE_VAR, // a != b
VAR_OP_LT_VAR, // a < b
VAR_OP_GT_VAR, // a > b
VAR_OP_LE_VAR, // a <= b
VAR_OP_GE_VAR, // a >= b
VAR_DEAD // The atomic proposition used to label deadlock
};
// Structure for complex atomic proposition
struct one_prop
{
int lval;
relop op;
int rval;
int lval; // Index of left variable or raw number
relop op; // The operator
int rval; // Index or right variable or raw number
};
// Data structure to store complex atomic propositions
......@@ -176,29 +219,36 @@ namespace spot
std::string to_string(const cspins_state s, unsigned tid = 0) const;
cspins_iterator* succ(const cspins_state s, unsigned tid);
void recycle(cspins_iterator* it, unsigned tid);
/// \brief List the atomic propositions used by *this* kripke
const std::vector<std::string> get_ap();
/// \brief The number of thread used by *this* kripke
unsigned get_threads();
private:
/// Parse the set of atomic proposition to have a more
/// \brief Parse the set of atomic proposition to have a more
/// efficient data strucure for computation
void match_aps(std::vector<std::string>& aps, std::string dead_prop);
/// Compute the cube associated to each state. The cube
/// \brief Compute the cube associated to each state. The cube
/// will then be given to all iterators.
void compute_condition(cube c, cspins_state s, unsigned tid = 0);
spins_interface_ptr sip_;
spins_interface_ptr sip_; // The interface to the shared library
const spot::spins_interface* d_; // To avoid numerous sip_.get()
cspins_state_manager* manager_;
bool compress_;
cspins_state_manager* manager_; // One manager per thread
bool compress_; // Should a compression be performed
// One per threads to store no longer used iterators (and save memory)
std::vector<std::vector<cspins_iterator*>> recycle_;
inner_callback_parameters* inner_;
cubeset cubeset_;
bool selfloopize_;
int dead_idx_;
std::vector<std::string> aps_;
unsigned int nb_threads_;
inner_callback_parameters* inner_; // One callback per thread
cubeset cubeset_; // A single cubeset to manipulate cubes
bool selfloopize_; // Should selfloopize be performed
int dead_idx_; // If yes, index of the "dead ap"
std::vector<std::string> aps_; // All the atomic propositions
unsigned int nb_threads_; // The number of threads used
};
/// \brief shortcut to manipulate the kripke below
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -95,65 +95,35 @@ namespace spot
return state_size_;
}
// This class provides an iterator over the successors of a state.
// All successors are computed once when an iterator is recycled or
// created.
cspins_iterator::cspins_iterator(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
inner_callback_parameters& inner,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset,
int dead_idx, unsigned tid)
: current_(0), cond_(cond), tid_(tid)
cspins_iterator::cspins_iterator(cspins_iterator_param& p)
: current_(0), cond_(p.cond), tid_(p.tid)
{
successors_.reserve(10);
inner.manager = &manager;
inner.succ = &successors_;
inner.compress = compress;
inner.selfloopize = selfloopize;
int* ref = s;
if (compress)
// already filled by compute_condition
ref = inner.uncompressed_;
setup_iterator(p.s, p.d, p.manager, p.inner, p.cond, p.compress,
p.selfloopize, p.cubeset, p.dead_idx);
}
int n = d->get_successors
(nullptr, manager.unbox_state(ref),
[](void* arg, transition_info_t*, int *dst){
inner_callback_parameters* inner =
static_cast<inner_callback_parameters*>(arg);
cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->size() * 2);
inner->succ->push_back(s);
},
&inner);
if (!n && selfloopize)
void cspins_iterator::recycle(cspins_iterator_param& p)
{
successors_.push_back(s);
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
tid_ = p.tid;
cond_ = p.cond;
current_ = 0;
// Constant time since int* is is_trivially_destructible
successors_.clear();
setup_iterator(p.s, p.d, p.manager, p.inner, p.cond, p.compress,
p.selfloopize, p.cubeset, p.dead_idx);
}
void cspins_iterator::recycle(cspins_state s,
void cspins_iterator::setup_iterator(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
inner_callback_parameters& inner,
cube cond,
cube& cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx, unsigned tid)
cubeset& cubeset,
int dead_idx)
{
tid_ = tid;
cond_ = cond;
current_ = 0;
// Constant time since int* is is_trivially_destructible
successors_.clear();
inner.manager = &manager;
inner.succ = &successors_;
inner.compress = compress;
......@@ -161,8 +131,8 @@ namespace spot
int* ref = s;
if (compress)
// Already filled by compute_condition
ref = inner.uncompressed_;
// already filled by compute_condition
ref = inner.uncompressed;
int n = d->get_successors
(nullptr, manager.unbox_state(ref),
......@@ -170,7 +140,7 @@ namespace spot
inner_callback_parameters* inner =
static_cast<inner_callback_parameters*>(arg);
cspins_state s =
inner->manager->alloc_setup(dst, inner->compressed_,
inner->manager->alloc_setup(dst, inner->compressed,
inner->manager->size() * 2);
inner->succ->push_back(s);
},
......@@ -181,6 +151,7 @@ namespace spot
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
}
cspins_iterator::~cspins_iterator()
......@@ -240,8 +211,8 @@ namespace spot
recycle_.back().reserve(2000000);
new (&manager_[i])
cspins_state_manager(d_->get_state_size(), compress);
inner_[i].compressed_ = new int[d_->get_state_size() * 2];
inner_[i].uncompressed_ = new int[d_->get_state_size()+30];
inner_[i].compressed = new int[d_->get_state_size() * 2];
inner_[i].uncompressed = new int[d_->get_state_size()+30];
}
dead_idx_ = -1;
match_aps(visible_aps, dead_prop);
......@@ -262,8 +233,8 @@ namespace spot
for (unsigned i = 0; i < nb_threads_; ++i)
{
manager_[i].~cspins_state_manager();
delete[] inner_[i].compressed_;
delete[] inner_[i].uncompressed_;
delete[] inner_[i].compressed;
delete[] inner_[i].uncompressed;
}
::operator delete(manager_);
delete[] inner_;
......@@ -271,9 +242,9 @@ namespace spot
cspins_state kripkecube<cspins_state, cspins_iterator>::initial(unsigned tid)
{
d_->get_initial_state(inner_[tid].uncompressed_);
return manager_[tid].alloc_setup(inner_[tid].uncompressed_,
inner_[tid].compressed_,
d_->get_initial_state(inner_[tid].uncompressed);
return manager_[tid].alloc_setup(inner_[tid].uncompressed,
inner_[tid].compressed,
manager_[tid].size() * 2);
}
......@@ -286,9 +257,9 @@ namespace spot
cspins_state ref = out;
if (compress_)
{
manager_[tid].decompress(s, inner_[tid].uncompressed_,
manager_[tid].decompress(s, inner_[tid].uncompressed,
manager_[tid].size());
ref = inner_[tid].uncompressed_;
ref = inner_[tid].uncompressed;
}
for (int i = 0; i < d_->get_state_size(); ++i)
res += (d_->get_state_variable_name(i)) +
......@@ -301,21 +272,26 @@ namespace spot
kripkecube<cspins_state, cspins_iterator>::succ(const cspins_state s,
unsigned tid)
{
cspins_iterator::cspins_iterator_param p =
{
s, d_, manager_[tid], inner_[tid],
nullptr, compress_, selfloopize_,
cubeset_, dead_idx_, tid
};
if (SPOT_LIKELY(!recycle_[tid].empty()))
{
auto tmp = recycle_[tid].back();
recycle_[tid].pop_back();
compute_condition(tmp->condition(), s, tid);
tmp->recycle(s, d_, manager_[tid], inner_[tid],
tmp->condition(), compress_, selfloopize_,
cubeset_, dead_idx_, tid);
p.cond = tmp->condition();
compute_condition(p.cond, s, tid);
tmp->recycle(p);
return tmp;
}
cube cond = cubeset_.alloc();
p.cond = cond;
compute_condition(cond, s, tid);
return new cspins_iterator(s, d_, manager_[tid], inner_[tid],
cond, compress_, selfloopize_,
cubeset_, dead_idx_, tid);
return new cspins_iterator(p);
}
void
......@@ -346,9 +322,9 @@ namespace spot
// State is compressed, uncompress it
if (compress_)
{
manager_[tid].decompress(s, inner_[tid].uncompressed_+2,
manager_[tid].decompress(s, inner_[tid].uncompressed+2,
manager_[tid].size());
vars = inner_[tid].uncompressed_ + 2;
vars = inner_[tid].uncompressed + 2;
}
for (auto& ap: pset_)
......@@ -357,61 +333,61 @@ namespace spot
bool cond = false;
switch (ap.op)
{
case OP_EQ_VAR:
case relop::OP_EQ_VAR:
cond = (ap.lval == vars[ap.rval]);
break;
case OP_NE_VAR:
case relop::OP_NE_VAR:
cond = (ap.lval != vars[ap.rval]);
break;
case OP_LT_VAR:
case relop::OP_LT_VAR:
cond = (ap.lval < vars[ap.rval]);
break;
case OP_GT_VAR:
case relop::OP_GT_VAR:
cond = (ap.lval > vars[ap.rval]);
break;
case OP_LE_VAR:
case relop::OP_LE_VAR:
cond = (ap.lval <= vars[ap.rval]);
break;
case OP_GE_VAR:
case relop::OP_GE_VAR:
cond = (ap.lval >= vars[ap.rval]);
break;
case VAR_OP_EQ:
case relop::VAR_OP_EQ:
cond = (vars[ap.lval] == ap.rval);
break;
case VAR_OP_NE:
case relop::VAR_OP_NE:
cond = (vars[ap.lval] != ap.rval);
break;
case VAR_OP_LT:
case relop::VAR_OP_LT:
cond = (vars[ap.lval] < ap.rval);
break;
case VAR_OP_GT:
case relop::VAR_OP_GT:
cond = (vars[ap.lval] > ap.rval);
break;
case VAR_OP_LE:
case relop::VAR_OP_LE:
cond = (vars[ap.lval] <= ap.rval);
break;
case VAR_OP_GE:
case relop::VAR_OP_GE:
cond = (vars[ap.lval] >= ap.rval);
break;
case VAR_OP_EQ_VAR:
case relop::VAR_OP_EQ_VAR:
cond = (vars[ap.lval] == vars[ap.rval]);
break;
case VAR_OP_NE_VAR:
case relop::VAR_OP_NE_VAR:
cond = (vars[ap.lval] != vars[ap.rval]);
break;
case VAR_OP_LT_VAR:
case relop::VAR_OP_LT_VAR:
cond = (vars[ap.lval] < vars[ap.rval]);
break;
case VAR_OP_GT_VAR:
case relop::VAR_OP_GT_VAR:
cond = (vars[ap.lval] > vars[ap.rval]);
break;
case VAR_OP_LE_VAR:
case relop::VAR_OP_LE_VAR:
cond = (vars[ap.lval] <= vars[ap.rval]);
break;
case VAR_OP_GE_VAR:
case relop::VAR_OP_GE_VAR:
cond = (vars[ap.lval] >= vars[ap.rval]);
break;
case VAR_DEAD:
case relop::VAR_DEAD:
break;
default:
SPOT_ASSERT(false);
......@@ -465,7 +441,7 @@ namespace spot
if (ap.compare(dead_prop) == 0)
{
dead_idx_ = i;
pset_.push_back({i , VAR_DEAD, 0});
pset_.push_back({i , relop::VAR_DEAD, 0});
continue;
}
......@@ -483,7 +459,7 @@ namespace spot
// The aps is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
pset_.push_back({(int)std::distance(k_aps.begin(), it),
VAR_OP_NE, 0});
relop::VAR_OP_NE, 0});
continue;
}
......@@ -534,7 +510,6 @@ namespace spot
// And finally the operator
relop oper;
// Now, left and (possibly) right may refer atomic
// propositions or specific state inside of a process.
// First check if it is a known atomic proposition
......@@ -586,7 +561,7 @@ namespace spot
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), proc_name)),
VAR_OP_EQ, ei->second});
relop::VAR_OP_EQ, ei->second});
continue;
}
else
......@@ -631,7 +606,7 @@ namespace spot
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), right)),
VAR_OP_EQ, ei->second});
relop::VAR_OP_EQ, ei->second});
continue;
}
}
......@@ -711,7 +686,7 @@ namespace spot
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), left)),
VAR_OP_EQ, ei->second});
relop::VAR_OP_EQ, ei->second});
continue;
}
}
......@@ -729,23 +704,23 @@ namespace spot
// Left and Right are know, just analyse the operator.
if (op.compare("==") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_EQ_VAR :
(left_is_digit? OP_EQ_VAR : VAR_OP_EQ);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_EQ_VAR :
(left_is_digit? relop::OP_EQ_VAR : relop::VAR_OP_EQ);
else if (op.compare("!=") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_NE_VAR :
(left_is_digit? OP_NE_VAR : VAR_OP_NE);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_NE_VAR :
(left_is_digit? relop::OP_NE_VAR : relop::VAR_OP_NE);
else if (op.compare("<") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_LT_VAR :
(left_is_digit? OP_LT_VAR : VAR_OP_LT);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_LT_VAR :
(left_is_digit? relop::OP_LT_VAR : relop::VAR_OP_LT);
else if (op.compare(">") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_GT_VAR :
(left_is_digit? OP_GT_VAR : VAR_OP_GT);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_GT_VAR :
(left_is_digit? relop::OP_GT_VAR : relop::VAR_OP_GT);
else if (op.compare("<=") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_LE_VAR :
(left_is_digit? OP_LE_VAR : VAR_OP_LE);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_LE_VAR :
(left_is_digit? relop::OP_LE_VAR : relop::VAR_OP_LE);
else if (op.compare(">=") == 0)
oper = !left_is_digit && !right_is_digit? VAR_OP_GE_VAR :
(left_is_digit? OP_GE_VAR : VAR_OP_GE);
oper = !left_is_digit && !right_is_digit? relop::VAR_OP_GE_VAR :
(left_is_digit? relop::OP_GE_VAR : relop::VAR_OP_GE);
else
{
err << "\nOperation \"" << op
......
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