alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sanity: replace tabulars by spaces

Browse source 
* spot/ltsmin/ltsmin.cc,
spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/unionfind.cc,
spot/mc/utils.hh, spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: here.
This commit is contained in:
Etienne Renault 2016-04-11 14:20:34 +02:00
parent 681c2b2011
commit f04074bd6d
15 changed files with 935 additions and 936 deletions
Download patch file Download diff file Expand all files Collapse all files

871
spot/ltsmin/ltsmin.cc
View file

@ -1144,9 +1144,8 @@ namespace spot
}
};
//brick::hashset::FastConcurrent<both , both_hasher> ht2;
typedef brick::hashset::FastConcurrent<cspins_state,
cspins_state_hasher> cspins_state_map;
cspins_state_hasher> cspins_state_map;
////////////////////////////////////////////////////////////////////////
// A manager for Cspins states.
@ -1205,9 +1204,9 @@ namespace spot
void dealloc(cspins_state s)
{
if (compress_)
msp_.deallocate(s, (s[1]+2)*sizeof(int));
msp_.deallocate(s, (s[1]+2)*sizeof(int));
else
p_.deallocate(s);
p_.deallocate(s);
}
unsigned int size() const
@ -1249,15 +1248,15 @@ namespace spot
{
public:
cspins_iterator(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner,
int defvalue,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx)
const spot::spins_interface* d,
cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner,
int defvalue,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx)
: current_(0), cond_(cond)
{
successors_.reserve(10);
@ -1270,41 +1269,41 @@ 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),
[](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);
auto it = inner->map->insert({s});
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
},
&inner);
(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);
auto it = inner->map->insert({s});
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
},
&inner);
if (!n && selfloopize)
{
successors_.push_back(s);
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
{
successors_.push_back(s);
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
}
void recycle(cspins_state s,
const spot::spins_interface* d,
cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner,
int defvalue,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx)
const spot::spins_interface* d,
cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner,
int defvalue,
cube cond,
bool compress,
bool selfloopize,
cubeset& cubeset, int dead_idx)
{
cond_ = cond;
current_ = 0;
@ -1319,35 +1318,35 @@ 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),
[](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);
auto it = inner->map->insert({s});
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
},
&inner);
(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);
auto it = inner->map->insert({s});
inner->succ->push_back(*it);
if (!it.isnew())
inner->manager->dealloc(s);
},
&inner);
if (!n && selfloopize)
{
successors_.push_back(s);
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
{
successors_.push_back(s);
if (dead_idx != -1)
cubeset.set_true_var(cond, dead_idx);
}
}
~cspins_iterator()
{
// Do not release successors states, the manager
// will do it on time.
// Do not release successors states, the manager
// will do it on time.
}
void next()
@ -1420,20 +1419,20 @@ namespace spot
}
~kripkecube()
{
for (auto i: recycle_)
{
cubeset_.release(i->condition());
delete i;
}
delete inner_.compressed_;
delete inner_.uncompressed_;
for (auto i: recycle_)
{
cubeset_.release(i->condition());
delete i;
}
delete inner_.compressed_;
delete inner_.uncompressed_;
}
cspins_state initial()
{
d_->get_initial_state(inner_.uncompressed_);
return manager_.alloc_setup(inner_.uncompressed_, inner_.compressed_,
manager_.size() * 2);
manager_.size() * 2);
}
std::string to_string(const cspins_state s) const
@ -1442,13 +1441,13 @@ namespace spot
cspins_state out = manager_.unbox_state(s);
cspins_state ref = out;
if (compress_)
{
manager_.decompress(s, inner_.uncompressed_, manager_.size());
ref = inner_.uncompressed_;
}
{
manager_.decompress(s, inner_.uncompressed_, manager_.size());
ref = inner_.uncompressed_;
}
for (int i = 0; i < d_->get_state_size(); ++i)
res += (d_->get_state_variable_name(i)) +
("=" + std::to_string(ref[i])) + ",";
res += (d_->get_state_variable_name(i)) +
("=" + std::to_string(ref[i])) + ",";
res.pop_back();
return res;
}
@ -1456,20 +1455,20 @@ namespace spot
cspins_iterator* succ(const cspins_state s)
{
if (SPOT_LIKELY(!recycle_.empty()))
{
auto tmp = recycle_.back();
recycle_.pop_back();
compute_condition(tmp->condition(), s);
tmp->recycle(s, d_, manager_, map_, inner_, -1,
tmp->condition(), compress_, selfloopize_,
cubeset_, dead_idx_);
return tmp;
}
{
auto tmp = recycle_.back();
recycle_.pop_back();
compute_condition(tmp->condition(), s);
tmp->recycle(s, d_, manager_, map_, inner_, -1,
tmp->condition(), compress_, selfloopize_,
cubeset_, dead_idx_);
return tmp;
}
cube cond = cubeset_.alloc();
compute_condition(cond, s);
return new cspins_iterator(s, d_, manager_, map_, inner_,
-1, cond, compress_, selfloopize_,
cubeset_, dead_idx_);
-1, cond, compress_, selfloopize_,
cubeset_, dead_idx_);
}
void recycle(cspins_iterator* it)
@ -1518,80 +1517,80 @@ namespace spot
// State is compressed, uncompress it
if (compress_)
{
manager_.decompress(s, inner_.uncompressed_+2, manager_.size());
vars = inner_.uncompressed_ + 2;
manager_.decompress(s, inner_.uncompressed_+2, manager_.size());
vars = inner_.uncompressed_ + 2;
}
for (auto& ap: pset_)
{
++i;
bool cond = false;
switch (ap.op)
{
case OP_EQ_VAR:
cond = (ap.lval == vars[ap.rval]);
break;
case OP_NE_VAR:
cond = (ap.lval != vars[ap.rval]);
break;
case OP_LT_VAR:
cond = (ap.lval < vars[ap.rval]);
break;
case OP_GT_VAR:
cond = (ap.lval > vars[ap.rval]);
break;
case OP_LE_VAR:
cond = (ap.lval <= vars[ap.rval]);
break;
case OP_GE_VAR:
cond = (ap.lval >= vars[ap.rval]);
break;
case VAR_OP_EQ:
cond = (vars[ap.lval] == ap.rval);
break;
case VAR_OP_NE:
cond = (vars[ap.lval] != ap.rval);
break;
case VAR_OP_LT:
cond = (vars[ap.lval] < ap.rval);
break;
case VAR_OP_GT:
cond = (vars[ap.lval] > ap.rval);
break;
case VAR_OP_LE:
cond = (vars[ap.lval] <= ap.rval);
break;
case VAR_OP_GE:
cond = (vars[ap.lval] >= ap.rval);
break;
case VAR_OP_EQ_VAR:
cond = (vars[ap.lval] == vars[ap.rval]);
break;
case VAR_OP_NE_VAR:
cond = (vars[ap.lval] != vars[ap.rval]);
break;
case VAR_OP_LT_VAR:
cond = (vars[ap.lval] < vars[ap.rval]);
break;
case VAR_OP_GT_VAR:
cond = (vars[ap.lval] > vars[ap.rval]);
break;
case VAR_OP_LE_VAR:
cond = (vars[ap.lval] <= vars[ap.rval]);
break;
case VAR_OP_GE_VAR:
cond = (vars[ap.lval] >= vars[ap.rval]);
break;
case VAR_DEAD:
break;
default:
assert(false);
}
++i;
bool cond = false;
switch (ap.op)
{
case OP_EQ_VAR:
cond = (ap.lval == vars[ap.rval]);
break;
case OP_NE_VAR:
cond = (ap.lval != vars[ap.rval]);
break;
case OP_LT_VAR:
cond = (ap.lval < vars[ap.rval]);
break;
case OP_GT_VAR:
cond = (ap.lval > vars[ap.rval]);
break;
case OP_LE_VAR:
cond = (ap.lval <= vars[ap.rval]);
break;
case OP_GE_VAR:
cond = (ap.lval >= vars[ap.rval]);
break;
case VAR_OP_EQ:
cond = (vars[ap.lval] == ap.rval);
break;
case VAR_OP_NE:
cond = (vars[ap.lval] != ap.rval);
break;
case VAR_OP_LT:
cond = (vars[ap.lval] < ap.rval);
break;
case VAR_OP_GT:
cond = (vars[ap.lval] > ap.rval);
break;
case VAR_OP_LE:
cond = (vars[ap.lval] <= ap.rval);
break;
case VAR_OP_GE:
cond = (vars[ap.lval] >= ap.rval);
break;
case VAR_OP_EQ_VAR:
cond = (vars[ap.lval] == vars[ap.rval]);
break;
case VAR_OP_NE_VAR:
cond = (vars[ap.lval] != vars[ap.rval]);
break;
case VAR_OP_LT_VAR:
cond = (vars[ap.lval] < vars[ap.rval]);
break;
case VAR_OP_GT_VAR:
cond = (vars[ap.lval] > vars[ap.rval]);
break;
case VAR_OP_LE_VAR:
cond = (vars[ap.lval] <= vars[ap.rval]);
break;
case VAR_OP_GE_VAR:
cond = (vars[ap.lval] >= vars[ap.rval]);
break;
case VAR_DEAD:
break;
default:
assert(false);
}
if (cond)
cubeset_.set_true_var(c, i);
else
cubeset_.set_false_var(c, i);
if (cond)
cubeset_.set_true_var(c, i);
else
cubeset_.set_false_var(c, i);
}
}
@ -1615,10 +1614,10 @@ namespace spot
std::unordered_map<std::string, int> matcher;
for (int i = 0; i < type_count; ++i)
{
matcher[d_->get_type_name(i)] = i;
int enum_count = d_->get_type_value_count(i);
for (int j = 0; j < enum_count; ++j)
enum_map[i].emplace(d_->get_type_value_name(i, j), j);
matcher[d_->get_type_name(i)] = i;
int enum_count = d_->get_type_value_count(i);
for (int j = 0; j < enum_count; ++j)
enum_map[i].emplace(d_->get_type_value_name(i, j), j);
}
// Then we extract the basic atomics propositions from the Kripke
@ -1630,308 +1629,308 @@ namespace spot
int i = -1;
for (auto ap: aps)
{
++i;
++i;
// Grab dead property
if (ap.compare(dead_prop) == 0)
{
dead_idx_ = i;
pset_.push_back({i , VAR_DEAD, 0});
continue;
}
// Grab dead property
if (ap.compare(dead_prop) == 0)
{
dead_idx_ = i;
pset_.push_back({i , VAR_DEAD, 0});
continue;
}
// Get ap name and remove all extra whitespace
ap.erase(std::remove_if(ap.begin(), ap.end(),
[](char x){
return std::isspace(x);
}),
ap.end());
// Get ap name and remove all extra whitespace
ap.erase(std::remove_if(ap.begin(), ap.end(),
[](char x){
return std::isspace(x);
}),
ap.end());
// Look if it is a well known atomic proposition
auto it = std::find(k_aps.begin(), k_aps.end(), ap);
if (it != k_aps.end())
{
// 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});
continue;
}
// Look if it is a well known atomic proposition
auto it = std::find(k_aps.begin(), k_aps.end(), ap);
if (it != k_aps.end())
{
// 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});
continue;
}
// The ap is not known. We distinguish many cases:
// - It is a State name, i.e P_0.S or P_0 == S
// - It refers a specific variable value, i.e. P_0.var == 2,
// P_0.var < 2, P_0.var != 2, ...
// - It's an unknown variable
// Note that we do not support P_0.state1 == 12 since we do not
// know how to interpret such atomic proposition.
// The ap is not known. We distinguish many cases:
// - It is a State name, i.e P_0.S or P_0 == S
// - It refers a specific variable value, i.e. P_0.var == 2,
// P_0.var < 2, P_0.var != 2, ...
// - It's an unknown variable
// Note that we do not support P_0.state1 == 12 since we do not
// know how to interpret such atomic proposition.
// We split the formula according to operators
std::size_t found_op_first = ap.find_first_of("=<>!");
std::size_t found_op_last = ap.find_last_of("=<>!");
std::string left;
std::string right;
std::string ap_error;
std::string op;
// We split the formula according to operators
std::size_t found_op_first = ap.find_first_of("=<>!");
std::size_t found_op_last = ap.find_last_of("=<>!");
std::string left;
std::string right;
std::string ap_error;
std::string op;
if (found_op_first == 0 || found_op_last == ap.size()-1)
{
err << "Invalid operator use in " << ap << '\n';
++errors;
continue;
}
if (found_op_first == 0 || found_op_last == ap.size()-1)
{
err << "Invalid operator use in " << ap << '\n';
++errors;
continue;
}
if (std::string::npos == found_op_first)
{
left = ap;
right = "";
op = "";
}
else
{
left = ap.substr(0, found_op_first);
right = ap.substr(found_op_last+1, ap.size()-found_op_last);
op = ap.substr(found_op_first, found_op_last+1-found_op_first);
}
if (std::string::npos == found_op_first)
{
left = ap;
right = "";
op = "";
}
else
{
left = ap.substr(0, found_op_first);
right = ap.substr(found_op_last+1, ap.size()-found_op_last);
op = ap.substr(found_op_first, found_op_last+1-found_op_first);
}
// Variables to store the left part of the atomic proposition
bool left_is_digit = false;
int lval;
// Variables to store the left part of the atomic proposition
bool left_is_digit = false;
int lval;
// Variables to store the right part of the atomic proposition
bool right_is_digit = false;
int rval;
// Variables to store the right part of the atomic proposition
bool right_is_digit = false;
int rval;
// And finally the operator
relop oper;
// And finally the operator
relop oper;
// Now, left and (possibly) right are should refer atomic
// propositions or specific state inside of a process.
// First check if it is a known atomic proposition
it = std::find(k_aps.begin(), k_aps.end(), left);
if (it != k_aps.end())
{
// The aps is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
lval = std::distance(k_aps.begin(), it);
}
else
{
// Detect if it is a process state
std::size_t found_dot = left.find_first_of('.');
if (std::string::npos != found_dot)
{
std::string proc_name = left.substr(0, found_dot);
std::string st_name = left.substr(found_dot+1,
left.size()-found_dot);
// Now, left and (possibly) right are should refer atomic
// propositions or specific state inside of a process.
// First check if it is a known atomic proposition
it = std::find(k_aps.begin(), k_aps.end(), left);
if (it != k_aps.end())
{
// The aps is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
lval = std::distance(k_aps.begin(), it);
}
else
{
// Detect if it is a process state
std::size_t found_dot = left.find_first_of('.');
if (std::string::npos != found_dot)
{
std::string proc_name = left.substr(0, found_dot);
std::string st_name = left.substr(found_dot+1,
left.size()-found_dot);
auto ni = matcher.find(proc_name);
if (ni == matcher.end())
{
ap_error = left;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(st_name);
if (ei == enum_map[type_num].end())
{
ap_error = left;
goto error_ap_unknown;
}
auto ni = matcher.find(proc_name);
if (ni == matcher.end())
{
ap_error = left;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(st_name);
if (ei == enum_map[type_num].end())
{
ap_error = left;
goto error_ap_unknown;
}
if (right.compare("") != 0)
{
// We are in the case P.state1 == something.. We don't
// know how to interpret this.
ap_error = op + right;
err << "\nOperation " << op << " in \"" << ap_error
<< "\" is not available for process's state"
<< " (i.e. " << left << ")\n";
++errors;
continue;
}
if (right.compare("") != 0)
{
// We are in the case P.state1 == something.. We don't
// know how to interpret this.
ap_error = op + right;
err << "\nOperation " << op << " in \"" << ap_error
<< "\" is not available for process's state"
<< " (i.e. " << left << ")\n";
++errors;
continue;
}
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), proc_name)),
VAR_OP_EQ, ei->second});
continue;
}
else
{
// Finally, it's a number...
left_is_digit = true;
for (auto c: left)
if (!isdigit(c))
left_is_digit = false;
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), proc_name)),
VAR_OP_EQ, ei->second});
continue;
}
else
{
// Finally, it's a number...
left_is_digit = true;
for (auto c: left)
if (!isdigit(c))
left_is_digit = false;
if (left_is_digit)
lval = std::strtol (left.c_str(), nullptr, 10);
else
{
// ... or something like: State1 == P_0
// so it doesn't contains '.'
if (std::string::npos != right.find_first_of('.'))
{
err << "\nOperation \"" << right
<< "\" does not refer a process"
<< " (i.e. " << left << " is not valid)\n";
++errors;
continue;
}
if (left_is_digit)
lval = std::strtol (left.c_str(), nullptr, 10);
else
{
// ... or something like: State1 == P_0
// so it doesn't contains '.'
if (std::string::npos != right.find_first_of('.'))
{
err << "\nOperation \"" << right
<< "\" does not refer a process"
<< " (i.e. " << left << " is not valid)\n";
++errors;
continue;
}
// or something like: P_0 == State1
auto ni = matcher.find(right);
if (ni == matcher.end())
{
ap_error = ap;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(left);
if (ei == enum_map[type_num].end())
{
ap_error = left;
goto error_ap_unknown;
}
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), right)),
VAR_OP_EQ, ei->second});
continue;
}
}
}
// or something like: P_0 == State1
auto ni = matcher.find(right);
if (ni == matcher.end())
{
ap_error = ap;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(left);
if (ei == enum_map[type_num].end())
{
ap_error = left;
goto error_ap_unknown;
}
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), right)),
VAR_OP_EQ, ei->second});
continue;
}
}
}
// Here Left is known. Just detect cases where left is digit there is
// no right part.
if (left_is_digit && right.empty())
{
ap_error = ap;
goto error_ap_unknown;
}
// Here Left is known. Just detect cases where left is digit there is
// no right part.
if (left_is_digit && right.empty())
{
ap_error = ap;
goto error_ap_unknown;
}
assert(!right.empty() && !op.empty());
assert(!right.empty() && !op.empty());
// Parse right part of the atomic proposition
// Check if it is a known atomic proposition
it = std::find(k_aps.begin(), k_aps.end(), right);
if (it != k_aps.end())
{
// The aps is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
rval = std::distance(k_aps.begin(), it);
}
else
{
// We are is the right part, so if it is a process state
// we do not know how to interpret (xxx == P.state1). Abort
std::size_t found_dot = right.find_first_of('.');
if (std::string::npos != found_dot)
{
ap_error = left + op;
err << "\nOperation " << op << " in \"" << ap_error
<< "\" is not available for process's state"
<< " (i.e. " << right << ")\n";
++errors;
continue;
}
else
{
// Finally, it's a number
right_is_digit = true;
for (auto c: right)
if (!isdigit(c))
right_is_digit = false;
// Parse right part of the atomic proposition
// Check if it is a known atomic proposition
it = std::find(k_aps.begin(), k_aps.end(), right);
if (it != k_aps.end())
{
// The aps is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
rval = std::distance(k_aps.begin(), it);
}
else
{
// We are is the right part, so if it is a process state
// we do not know how to interpret (xxx == P.state1). Abort
std::size_t found_dot = right.find_first_of('.');
if (std::string::npos != found_dot)
{
ap_error = left + op;
err << "\nOperation " << op << " in \"" << ap_error
<< "\" is not available for process's state"
<< " (i.e. " << right << ")\n";
++errors;
continue;
}
else
{
// Finally, it's a number
right_is_digit = true;
for (auto c: right)
if (!isdigit(c))
right_is_digit = false;
if (right_is_digit)
rval = std::strtol (right.c_str(), nullptr, 10);
else
{
if (std::string::npos != left.find_first_of('.'))
{
err << "\nProposition \"" << ap
<< "\" cannot be interpreted"
<< " (i.e. " << op + right << " is not valid)\n";
++errors;
continue;
}
if (right_is_digit)
rval = std::strtol (right.c_str(), nullptr, 10);
else
{
if (std::string::npos != left.find_first_of('.'))
{
err << "\nProposition \"" << ap
<< "\" cannot be interpreted"
<< " (i.e. " << op + right << " is not valid)\n";
++errors;
continue;
}
// or something like: P_0 == State1
auto ni = matcher.find(left);
if (ni == matcher.end())
{
// or something like: P_0 == State1
auto ni = matcher.find(left);
if (ni == matcher.end())
{
ap_error = left;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(right);
if (ei == enum_map[type_num].end())
{
ap_error = right;
goto error_ap_unknown;
}
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), left)),
VAR_OP_EQ, ei->second});
continue;
}
}
}
ap_error = left;
goto error_ap_unknown;
}
int type_num = ni->second;
enum_map_t::const_iterator ei =
enum_map[type_num].find(right);
if (ei == enum_map[type_num].end())
{
ap_error = right;
goto error_ap_unknown;
}
pset_.push_back({
(int) std::distance(k_aps.begin(),
std::find(k_aps.begin(),
k_aps.end(), left)),
VAR_OP_EQ, ei->second});
continue;
}
}
}
if (left_is_digit && right_is_digit)
{
err << "\nOperation \"" << op
<< "\" between two numbers not available"
<< " (i.e. " << right << " and, "
<< left << ")\n";
++errors;
continue;
}
if (left_is_digit && right_is_digit)
{
err << "\nOperation \"" << op
<< "\" between two numbers not available"
<< " (i.e. " << right << " and, "
<< left << ")\n";
++errors;
continue;
}
// 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);
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);
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);
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);
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);
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);
else
{
err << "\nOperation \"" << op
<< "\" is unknown\n";
++errors;
continue;
}
// 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);
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);
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);
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);
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);
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);
else
{
err << "\nOperation \"" << op
<< "\" is unknown\n";
++errors;
continue;
}
pset_.push_back({lval, oper, rval});
continue;
pset_.push_back({lval, oper, rval});
continue;
error_ap_unknown:
err << "\nProposition \"" << ap_error << "\" does not exist\n";
++errors;
continue;
err << "\nProposition \"" << ap_error << "\" does not exist\n";
++errors;
continue;
}
if (errors)

162
spot/mc/ec.hh
View file

@ -31,24 +31,24 @@ namespace spot
/// emptiness check that has been proposed we opted to implement
/// the Gabow's one.
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
typename StateHash, typename StateEqual>
class ec_renault13lpar : public intersect<State, SuccIterator,
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
{
// Ease the manipulation
using typename intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
public:
ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
twacube* twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
acc_(twa->acc())
{
}
@ -84,13 +84,13 @@ namespace spot
/// to true and both \a newtop and \a newtop_dfsnum have inconsistency
/// values.
bool pop_state(product_state, unsigned top_dfsnum, bool,
product_state, unsigned)
product_state, unsigned)
{
if (top_dfsnum == roots_.back().dfsnum)
{
roots_.pop_back();
uf_.markdead(top_dfsnum);
}
{
roots_.pop_back();
uf_.markdead(top_dfsnum);
}
return true;
}
@ -101,7 +101,7 @@ namespace spot
acc_cond::mark_t cond)
{
if (uf_.isdead(dst_dfsnum))
return false;
return false;
while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
{
@ -127,18 +127,18 @@ namespace spot
// Compute the prefix of the accepting run
for (auto& s : this->todo)
res += " " + std::to_string(s.st.st_prop) +
+ "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
res += " " + std::to_string(s.st.st_prop) +
+ "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
// Compute the accepting cycle
res += "Cycle:\n";
struct ctrx_element
{
const product_state* prod_st;
ctrx_element* parent_st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
const product_state* prod_st;
ctrx_element* parent_st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
};
std::queue<ctrx_element*> bfs;
@ -148,65 +148,65 @@ namespace spot
this->sys_.succ(this->todo.back().st.st_kripke),
this->twa_->succ(this->todo.back().st.st_prop)}));
while (true)
{
here:
auto* front = bfs.front();
bfs.pop();
// PUSH all successors of the state.
while (!front->it_kripke->done())
{
while (!front->it_prop->done())
{
if (this->twa_->get_cubeset().intersect
(this->twa_->trans_data(front->it_prop).cube_,
front->it_kripke->condition()))
{
const product_state dst = {
front->it_kripke->state(),
this->twa_->trans_storage(front->it_prop).dst
};
{
here:
auto* front = bfs.front();
bfs.pop();
// PUSH all successors of the state.
while (!front->it_kripke->done())
{
while (!front->it_prop->done())
{
if (this->twa_->get_cubeset().intersect
(this->twa_->trans_data(front->it_prop).cube_,
front->it_kripke->condition()))
{
const product_state dst = {
front->it_kripke->state(),
this->twa_->trans_storage(front->it_prop).dst
};
// Skip Unknown states or not same SCC
auto it = this->map.find(dst);
if (it == this->map.end() ||
!uf_.sameset(it->second,
this->map[this->todo.back().st]))
{
front->it_prop->next();
continue;
}
// Skip Unknown states or not same SCC
auto it = this->map.find(dst);
if (it == this->map.end() ||
!uf_.sameset(it->second,
this->map[this->todo.back().st]))
{
front->it_prop->next();
continue;
}
// This is a valid transition. If this transition
// is the one we are looking for, update the counter-
// -example and flush the bfs queue.
auto mark = this->twa_->trans_data(front->it_prop).acc_;
if (!acc.has(mark))
{
ctrx_element* current = front;
while (current != nullptr)
{
// FIXME also display acc?
res = res + " " +
std::to_string(current->prod_st->st_prop) +
+ "*" +
this->sys_. to_string(current->prod_st
->st_kripke) +
"\n";
current = current->parent_st;
}
// This is a valid transition. If this transition
// is the one we are looking for, update the counter-
// -example and flush the bfs queue.
auto mark = this->twa_->trans_data(front->it_prop).acc_;
if (!acc.has(mark))
{
ctrx_element* current = front;
while (current != nullptr)
{
// FIXME also display acc?
res = res + " " +
std::to_string(current->prod_st->st_prop) +
+ "*" +
this->sys_. to_string(current->prod_st
->st_kripke) +
"\n";
current = current->parent_st;
}
// empty the queue
while (!bfs.empty())
{
auto* e = bfs.front();
bfs.pop();
delete e;
}
// empty the queue
while (!bfs.empty())
{
auto* e = bfs.front();
bfs.pop();
delete e;
}
// update acceptance
acc |= mark;
if (this->twa_->acc().accepting(acc))
return res;
// update acceptance
acc |= mark;
if (this->twa_->acc().accepting(acc))
return res;
const product_state* q = &(it->first);
ctrx_element* root = new ctrx_element({
@ -242,15 +242,15 @@ namespace spot
virtual std::string stats() override
{
return
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
}
private:
bool found_ = false; ///< \brief A counterexample is detected?
bool found_ = false; ///< \brief A counterexample is detected?
struct root_element {
unsigned dfsnum;

174
spot/mc/intersect.hh
View file

@ -42,8 +42,8 @@ namespace spot
/// The other template parameters allows to consider any kind
/// of state (and so any kind of kripke structures).
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename EmptinessCheck>
typename StateHash, typename StateEqual,
typename EmptinessCheck>
class SPOT_API intersect
{
public:
@ -78,64 +78,64 @@ namespace spot
self().setup();
product_state initial = {sys_.initial(), twa_->get_initial()};
if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U)))
{
todo.push_back({initial, sys_.succ(initial.st_kripke),
twa_->succ(initial.st_prop)});
{
todo.push_back({initial, sys_.succ(initial.st_kripke),
twa_->succ(initial.st_prop)});
// Not going further! It's a product with a single state.
if (todo.back().it_prop->done())
return false;
// Not going further! It's a product with a single state.
if (todo.back().it_prop->done())
return false;
forward_iterators(true);
map[initial] = ++dfs_number;
}
forward_iterators(true);
map[initial] = ++dfs_number;
}
while (!todo.empty())
{
// Check the kripke is enough since it's the outer loop. More
// details in forward_iterators.
if (todo.back().it_kripke->done())
{
bool is_init = todo.size() == 1;
auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
if (SPOT_LIKELY(self().pop_state(todo.back().st,
map[todo.back().st],
is_init,
newtop,
map[newtop])))
{
sys_.recycle(todo.back().it_kripke);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
}
}
else
{
++transitions;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop).dst
};
auto acc = twa_->trans_data(todo.back().it_prop).acc_;
forward_iterators(false);
auto it = map.find(dst);
if (it == map.end())
{
if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke),
twa_->succ(dst.st_prop)});
forward_iterators(true);
}
}
else if (SPOT_UNLIKELY(self().update(todo.back().st,
dfs_number,
dst, map[dst], acc)))
return true;
}
}
{
// Check the kripke is enough since it's the outer loop. More
// details in forward_iterators.
if (todo.back().it_kripke->done())
{
bool is_init = todo.size() == 1;
auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
if (SPOT_LIKELY(self().pop_state(todo.back().st,
map[todo.back().st],
is_init,
newtop,
map[newtop])))
{
sys_.recycle(todo.back().it_kripke);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
}
}
else
{
++transitions;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop).dst
};
auto acc = twa_->trans_data(todo.back().it_prop).acc_;
forward_iterators(false);
auto it = map.find(dst);
if (it == map.end())
{
if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke),
twa_->succ(dst.st_prop)});
forward_iterators(true);
}
}
else if (SPOT_UNLIKELY(self().update(todo.back().st,
dfs_number,
dst, map[dst], acc)))
return true;
}
}
return false;
}
@ -158,8 +158,8 @@ namespace spot
virtual std::string stats()
{
return
std::to_string(dfs_number) + " unique states visited\n" +
std::to_string(transitions) + " transitions explored\n";
std::to_string(dfs_number) + " unique states visited\n" +
std::to_string(transitions) + " transitions explored\n";
}
protected:
@ -175,37 +175,37 @@ namespace spot
// Sometimes kripke state may have no successors.
if (todo.back().it_kripke->done())
return;
return;
// The state has just been push and the 2 iterators intersect.
// There is no need to move iterators forward.
assert(!(todo.back().it_prop->done()));
if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition()))
return;
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition()))
return;
// Otherwise we have to compute the next valid successor (if it exits).
// This requires two loops. The most inner one is for the twacube since
// its costless
if (todo.back().it_prop->done())
todo.back().it_prop->reset();
todo.back().it_prop->reset();
else
todo.back().it_prop->next();
todo.back().it_prop->next();
while (!todo.back().it_kripke->done())
{
while (!todo.back().it_prop->done())
{
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition())))
return;
todo.back().it_prop->next();
}
todo.back().it_prop->reset();
todo.back().it_kripke->next();
}
{
while (!todo.back().it_prop->done())
{
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition())))
return;
todo.back().it_prop->next();
}
todo.back().it_prop->reset();
todo.back().it_kripke->next();
}
}
public:
@ -219,11 +219,11 @@ namespace spot
{
bool
operator()(const product_state lhs,
const product_state rhs) const
const product_state rhs) const
{
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
}
};
@ -232,10 +232,10 @@ namespace spot
size_t
operator()(const product_state that) const
{
// FIXME! wang32_hash(that.st_prop) could have
// been pre-calculated!
StateHash hasher;
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
// FIXME! wang32_hash(that.st_prop) could have
// been pre-calculated!
StateHash hasher;
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
}
};
@ -249,8 +249,8 @@ namespace spot
twacube* twa_;
std::vector<todo_element> todo;
typedef std::unordered_map<const product_state, int,
product_state_hash,
product_state_equal> visited_map;
product_state_hash,
product_state_equal> visited_map;
visited_map map;
unsigned int dfs_number = 0;
unsigned int transitions = 0;

58
spot/mc/reachability.hh
View file

@ -27,8 +27,8 @@ namespace spot
/// of a kripkecube. The algorithm uses a single DFS since it
/// is the most efficient in a sequential setting
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename Visitor>
typename StateHash, typename StateEqual,
typename Visitor>
class SPOT_API seq_reach_kripke
{
public:
@ -59,32 +59,32 @@ namespace spot
visited[initial] = ++dfs_number;
self().push(initial, dfs_number);
while (!todo.empty())
{
if (todo.back().it->done())
{
sys_.recycle(todo.back().it);
todo.pop_back();
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
self().push(dst, dfs_number);
self().edge(visited[todo.back().s], dfs_number);
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst)});
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
{
if (todo.back().it->done())
{
sys_.recycle(todo.back().it);
todo.pop_back();
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
self().push(dst, dfs_number);
self().edge(visited[todo.back().s], dfs_number);
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst)});
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
self().finalize();
}
@ -109,7 +109,7 @@ namespace spot
// FIXME: The system already handle a set of visited states so
// this map is redundant: an we avoid this new map?
typedef std::unordered_map<const State, int,
StateHash, StateEqual> visited_map;
StateHash, StateEqual> visited_map;
visited_map visited;
unsigned int dfs_number = 0;
unsigned int transitions = 0;

2
spot/mc/unionfind.cc
View file

@ -69,7 +69,7 @@ namespace spot
else {
id[root2] = root1;
if (rk1 == rk2)
id[root1] = -(rk1 + 1);
id[root1] = -(rk1 + 1);
}
return true;
}

88
spot/mc/utils.hh
View file

@ -27,18 +27,18 @@
namespace spot
{
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
typename StateHash, typename StateEqual>
class SPOT_API kripke_to_twa :
public seq_reach_kripke<State, SuccIterator,
StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>
StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>
{
public:
kripke_to_twa(kripkecube<State, SuccIterator>& sys, bdd_dict_ptr dict)
: seq_reach_kripke<State, SuccIterator, StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys),
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys),
dict_(dict)
{}
@ -57,10 +57,10 @@ namespace spot
// Compute the reverse binder.
auto aps = this->sys_.get_ap();
for (unsigned i = 0; i < aps.size(); ++i)
{
auto k = res_->register_ap(aps[i]);
reverse_binder_.insert({i, k});
}
{
auto k = res_->register_ap(aps[i]);
reverse_binder_.insert({i, k});
}
}
void push(State s, unsigned i)
@ -74,7 +74,7 @@ namespace spot
{
cubeset cs(this->sys_.get_ap().size());
bdd cond = cube_to_bdd(this->todo.back().it->condition(),
cs, reverse_binder_);
cs, reverse_binder_);
res_->new_edge(src, dst, cond);
}
@ -101,25 +101,25 @@ namespace spot
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
typename StateHash, typename StateEqual>
class SPOT_API product_to_twa :
public intersect<State, SuccIterator,
StateHash, StateEqual,
product_to_twa<State, SuccIterator,
StateHash, StateEqual>>
StateHash, StateEqual,
product_to_twa<State, SuccIterator,
StateHash, StateEqual>>
{
// Ease the manipulation
using typename intersect<State, SuccIterator, StateHash, StateEqual,
product_to_twa<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
product_to_twa<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
public:
product_to_twa(kripkecube<State, SuccIterator>& sys,
twacube* twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
product_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys, twa)
product_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys, twa)
{
}
@ -141,50 +141,50 @@ namespace spot
int i = 0;
for (auto ap : this->twa_->get_ap())
{
auto idx = res_->register_ap(ap);
std::cout << ap << idx << std::endl;
reverse_binder_[i++] = idx;
}
{
auto idx = res_->register_ap(ap);
std::cout << ap << idx << std::endl;
reverse_binder_[i++] = idx;
}
}
bool push_state(product_state s, unsigned i, acc_cond::mark_t)
{
// push also implies edge (when it's not the initial state)
if (this->todo.size())
{
auto c = this->twa_->get_cubeset()
.intersection(this->twa_->trans_data
(this->todo.back().it_prop).cube_,
this->todo.back().it_kripke->condition());
{
auto c = this->twa_->get_cubeset()
.intersection(this->twa_->trans_data
(this->todo.back().it_prop).cube_,
this->todo.back().it_kripke->condition());
bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
reverse_binder_);
this->twa_->get_cubeset().release(c);
res_->new_edge(this->map[this->todo.back().st]-1, i-1, x,
this->twa_->trans_data
(this->todo.back().it_prop).acc_);
}
bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
reverse_binder_);
this->twa_->get_cubeset().release(c);
res_->new_edge(this->map[this->todo.back().st]-1, i-1, x,
this->twa_->trans_data
(this->todo.back().it_prop).acc_);
}
unsigned st = res_->new_state();
names_->push_back(this->sys_.to_string(s.st_kripke) +
('*' + std::to_string(s.st_prop)));
('*' + std::to_string(s.st_prop)));
assert(st+1 == i);
return true;
}
bool update(product_state, unsigned src,
product_state, unsigned dst,
acc_cond::mark_t cond)
product_state, unsigned dst,
acc_cond::mark_t cond)
{
auto c = this->twa_->get_cubeset()
.intersection(this->twa_->trans_data
(this->todo.back().it_prop).cube_,
this->todo.back().it_kripke->condition());
.intersection(this->twa_->trans_data
(this->todo.back().it_prop).cube_,
this->todo.back().it_kripke->condition());
bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
reverse_binder_);
reverse_binder_);
this->twa_->get_cubeset().release(c);
res_->new_edge(src-1, dst-1, x, cond);
return false;

54
spot/twacube/cube.cc
View file

@ -79,9 +79,9 @@ namespace spot
bool incompatible = false;
for (unsigned int i = 0; i < uint_size_ && !incompatible; ++i)
{
true_elt = *(lhs+i) | *(rhs+i);
false_elt = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
incompatible |= (true_elt & false_elt);
true_elt = *(lhs+i) | *(rhs+i);
false_elt = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
incompatible |= (true_elt & false_elt);
}
return !incompatible;
}
@ -91,8 +91,8 @@ namespace spot
auto* res = new unsigned int[2*uint_size_];
for (unsigned int i = 0; i < uint_size_; ++i)
{
res[i] = *(lhs+i) | *(rhs+i);
res[i+uint_size_] = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
res[i] = *(lhs+i) | *(rhs+i);
res[i+uint_size_] = *(lhs+i+uint_size_) | *(rhs+i+uint_size_);
}
return res;
}
@ -119,11 +119,11 @@ namespace spot
{
for (unsigned int i = 0; i < 2*uint_size_; ++i)
{
if (i == uint_size_)
std::cout << '\n';
if (i == uint_size_)
std::cout << '\n';
for (unsigned x = 0; x < nb_bits_; ++x)
std::cout << ((*(c+i) >> x) & 1);
for (unsigned x = 0; x < nb_bits_; ++x)
std::cout << ((*(c+i) >> x) & 1);
}
std::cout << '\n';
}
@ -135,24 +135,24 @@ namespace spot
unsigned int cpt = 0;
for (unsigned int i = 0; i < uint_size_; ++i)
{
for (unsigned x = 0; x < nb_bits_ && cpt != size_; ++x)
{
bool true_var = (*(c+i) >> x) & 1;
bool false_var = (*(c+i+uint_size_) >> x) & 1;
if (true_var)
{
oss << aps[cpt]
<< (cpt != (size_ - 1) ? "&": "");
all_free = false;
}
else if (false_var)
{
oss << '!' << aps[cpt]
<< (cpt != (size_ - 1) ? "&": "");
all_free = false;
}
++cpt;
}
for (unsigned x = 0; x < nb_bits_ && cpt != size_; ++x)
{
bool true_var = (*(c+i) >> x) & 1;
bool false_var = (*(c+i+uint_size_) >> x) & 1;
if (true_var)
{
oss << aps[cpt]
<< (cpt != (size_ - 1) ? "&": "");
all_free = false;
}
else if (false_var)
{
oss << '!' << aps[cpt]
<< (cpt != (size_ - 1) ? "&": "");
all_free = false;
}
++cpt;
}
}
if (all_free)
oss << '1';

42
spot/twacube/twacube.cc
View file

@ -42,7 +42,7 @@ namespace spot
{ }
transition::transition(const cube& cube,
acc_cond::mark_t acc):
acc_cond::mark_t acc):
cube_(cube), acc_(acc)
{ }
@ -104,7 +104,7 @@ namespace spot
void
twacube::create_transition(unsigned int src, const cube& cube,
const acc_cond::mark_t& mark, unsigned int dst)
const acc_cond::mark_t& mark, unsigned int dst)
{
theg_.new_edge(src, dst, cube, mark);
}
@ -121,24 +121,24 @@ namespace spot
unsigned int i = 1;
while (i <= theg_.num_edges())
{
unsigned int j = i;
unsigned int j = i;
// Walk first bucket of successors
while (j <= theg_.num_edges() &&
theg_.edge_storage(i).src == theg_.edge_storage(j).src)
++j;
// Walk first bucket of successors
while (j <= theg_.num_edges() &&
theg_.edge_storage(i).src == theg_.edge_storage(j).src)
++j;
// Remove the next bucket
unsigned int itmp = j;
// Remove the next bucket
unsigned int itmp = j;
// Look if there are some transitions missing in this bucket.
while (j <= theg_.num_edges())
{
if (theg_.edge_storage(i).src == theg_.edge_storage(j).src)
return false;
++j;
}
i = itmp;
// Look if there are some transitions missing in this bucket.
while (j <= theg_.num_edges())
{
if (theg_.edge_storage(i).src == theg_.edge_storage(j).src)
return false;
++j;
}
i = itmp;
}
return true;
}
@ -150,10 +150,10 @@ namespace spot
os << "init : " << twa.init_ << '\n';
for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i)
os << twa.theg_.edge_storage(i).src << "->"
<< twa.theg_.edge_storage(i).dst << " : "
<< cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
<< ' ' << twa.theg_.edge_data(i).acc_
<< '\n';
<< twa.theg_.edge_storage(i).dst << " : "
<< cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
<< ' ' << twa.theg_.edge_data(i).acc_
<< '\n';
return os;
}
}

10
spot/twacube/twacube.hh
View file

@ -91,7 +91,7 @@ namespace spot
// no-swarming : since twacube are dedicated for parallelism, i.e.
// swarming, we expect swarming is activated.
if (SPOT_UNLIKELY(!seed))
return idx_;
return idx_;
// swarming.
return (((idx_-st_.succ+1)*seed) % (st_.succ_tail-st_.succ+1)) + st_.succ;
}
@ -115,7 +115,7 @@ namespace spot
unsigned int get_initial();
cstate* state_from_int(unsigned int i);
void create_transition(unsigned int src, const cube& cube,
const acc_cond::mark_t& mark, unsigned int dst);
const acc_cond::mark_t& mark, unsigned int dst);
const cubeset& get_cubeset() const;
bool succ_contiguous() const;
typedef digraph<cstate, transition> graph_t;
@ -126,12 +126,12 @@ namespace spot
typedef graph_t::edge_storage_t edge_storage_t;
const graph_t::edge_storage_t&
trans_storage(std::shared_ptr<trans_index> ci,
unsigned int seed = 0) const
unsigned int seed = 0) const
{
return theg_.edge_storage(ci->current(seed));
}
const transition& trans_data(std::shared_ptr<trans_index> ci,
unsigned int seed = 0) const
unsigned int seed = 0) const
{
return theg_.edge_data(ci->current(seed));
}
@ -142,7 +142,7 @@ namespace spot
}
friend SPOT_API std::ostream& operator<<(std::ostream& os,
const twacube& twa);
const twacube& twa);
private:
unsigned int init_;
acc_cond acc_;

128
spot/twacube_algos/convert.cc
View file

@ -23,45 +23,45 @@
namespace spot
{
spot::cube satone_to_cube(bdd one, cubeset& cubeset,
std::unordered_map<int, int>& binder)
std::unordered_map<int, int>& binder)
{
auto cube = cubeset.alloc();
while (one != bddtrue)
{
if (bdd_high(one) == bddfalse)
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_false_var(cube, binder[bdd_var(one)]);
one = bdd_low(one);
}
else
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_true_var(cube, binder[bdd_var(one)]);
one = bdd_high(one);
}
if (bdd_high(one) == bddfalse)
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_false_var(cube, binder[bdd_var(one)]);
one = bdd_low(one);
}
else
{
assert(binder.find(bdd_var(one)) != binder.end());
cubeset.set_true_var(cube, binder[bdd_var(one)]);
one = bdd_high(one);
}
}
return cube;
}
bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
std::unordered_map<int, int>& reverse_binder)
std::unordered_map<int, int>& reverse_binder)
{
bdd result = bddtrue;
for (unsigned int i = 0; i < cubeset.size(); ++i)
{
assert(reverse_binder.find(i) != reverse_binder.end());
if (cubeset.is_false_var(cube, i))
result &= bdd_nithvar(reverse_binder[i]);
if (cubeset.is_true_var(cube, i))
result &= bdd_ithvar(reverse_binder[i]);
assert(reverse_binder.find(i) != reverse_binder.end());
if (cubeset.is_false_var(cube, i))
result &= bdd_nithvar(reverse_binder[i]);
if (cubeset.is_true_var(cube, i))
result &= bdd_ithvar(reverse_binder[i]);
}
return result;
}
spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut,
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps)
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps)
{
// Declare the twa cube
spot::twacube* tg = new spot::twacube(aps);
@ -86,29 +86,29 @@ namespace spot
// spot::cube cube(aps);
for (unsigned n = 0; n < aut->num_states(); ++n)
for (auto& t: aut->out(n))
{
bdd cond = t.cond;
{
bdd cond = t.cond;
// Special case for bddfalse
if (cond == bddfalse)
{
spot::cube cube = tg->get_cubeset().alloc();
for (unsigned int i = 0; i < cs.size(); ++i)
cs.set_false_var(cube, i); // FIXME ! use fill!
tg->create_transition(st_binder[n], cube,
t.acc, st_binder[t.dst]);
}
else
// Split the bdd into multiple transitions
while (cond != bddfalse)
{
bdd one = bdd_satone(cond);
cond -= one;
spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, t.acc,
st_binder[t.dst]);
}
}
// Special case for bddfalse
if (cond == bddfalse)
{
spot::cube cube = tg->get_cubeset().alloc();
for (unsigned int i = 0; i < cs.size(); ++i)
cs.set_false_var(cube, i); // FIXME ! use fill!
tg->create_transition(st_binder[n], cube,
t.acc, st_binder[t.dst]);
}
else
// Split the bdd into multiple transitions
while (cond != bddfalse)
{
bdd one = bdd_satone(cond);
cond -= one;
spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, t.acc,
st_binder[t.dst]);
}
}
// Must be contiguous to support swarming.
assert(tg->succ_contiguous());
return tg;
@ -116,17 +116,17 @@ namespace spot
std::vector<std::string>*
extract_aps(spot::twa_graph_ptr& aut,
std::unordered_map<int, int>& ap_binder)
std::unordered_map<int, int>& ap_binder)
{
std::vector<std::string>* aps = new std::vector<std::string>();
for (auto f: aut->ap())
{
int size = aps->size();
if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end())
{
aps->push_back(f.ap_name());
ap_binder.insert({aut->get_dict()->var_map[f], size});
}
int size = aps->size();
if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end())
{
aps->push_back(f.ap_name());
ap_binder.insert({aut->get_dict()->var_map[f], size});
}
}
return aps;
}
@ -153,26 +153,26 @@ namespace spot
// Build all resulting states
for (unsigned int i = 0; i < theg.num_states(); ++i)
{
unsigned st = res->new_state();
(void) st;
assert(st == i);
unsigned st = res->new_state();
(void) st;
assert(st == i);
}
// Build all resulting conditions.
for (unsigned int i = 1; i <= theg.num_edges(); ++i)
{
bdd cond = bddtrue;
for (unsigned j = 0; j < cs.size(); ++j)
{
if (cs.is_true_var(theg.edge_data(i).cube_, j))
cond &= bdd_ithvar(bdds_ref[j]);
else if (cs.is_false_var(theg.edge_data(i).cube_, j))
cond &= bdd_nithvar(bdds_ref[j]);
// otherwise it 's a free variable do nothing
}
bdd cond = bddtrue;
for (unsigned j = 0; j < cs.size(); ++j)
{
if (cs.is_true_var(theg.edge_data(i).cube_, j))
cond &= bdd_ithvar(bdds_ref[j]);
else if (cs.is_false_var(theg.edge_data(i).cube_, j))
cond &= bdd_nithvar(bdds_ref[j]);
// otherwise it 's a free variable do nothing
}
res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
cond, theg.edge_data(i).acc_);
res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
cond, theg.edge_data(i).acc_);
}
// Fix the initial state

10
spot/twacube_algos/convert.hh
View file

@ -33,23 +33,23 @@ namespace spot
/// into a \a cube cube passed in parameter. The parameter
/// \a binder map bdd indexes to cube indexes.
SPOT_API spot::cube satone_to_cube(bdd one, cubeset& cubeset,
std::unordered_map<int, int>& binder);
std::unordered_map<int, int>& binder);
/// \brief Transform a \a cube cube into bdd using the map
/// that bind cube indexes to bdd indexes.
SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
std::unordered_map<int, int>& reverse_binder);
std::unordered_map<int, int>& reverse_binder);
/// \brief Extract the atomic propositions from the automaton
SPOT_API std::vector<std::string>*
extract_aps(spot::twa_graph_ptr& aut,
std::unordered_map<int, int>& ap_binder);
std::unordered_map<int, int>& ap_binder);
/// \brief Convert a twa into a twacube
SPOT_API spot::twacube*
twa_to_twacube(spot::twa_graph_ptr& aut,
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps);
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps);
/// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr

10
tests/core/bricks.cc
View file

@ -62,10 +62,10 @@ int main()
for (int i = 0; i < 6; i++)
workers.
push_back(std::thread([&ht2](int tid)
{
for (int i = 0; i< 2000; ++i)
ht2.insert({i, tid});
}, i));
{
for (int i = 0; i< 2000; ++i)
ht2.insert({i, tid});
}, i));
// Wait the end of all threads.
for (auto& t: workers)
@ -75,6 +75,6 @@ int main()
for (unsigned i = 0; i < ht2.size(); ++ i)
if (ht2.valid(i))
std::cout << i << ": {"
<< ht2[i].x << ',' << ht2[i].y << "}\n";
<< ht2[i].x << ',' << ht2[i].y << "}\n";
return 0;
}

6
tests/core/cube.cc
View file

@ -31,9 +31,9 @@
static bool test_translation(bdd& input, spot::cubeset& cubeset,
std::unordered_map<int, int>& binder,
std::unordered_map<int, int>& reverse_binder,
std::vector<std::string>& aps)
std::unordered_map<int, int>& binder,
std::unordered_map<int, int>& reverse_binder,
std::vector<std::string>& aps)
{
// The BDD used to detect if the convertion works
bdd res = bddfalse;

6
tests/core/twacube.cc
View file

@ -63,9 +63,9 @@ int main()
auto& t = aut->trans_storage(it, seed);
auto& d = aut->trans_data(it, seed);
std::cout << t.src << ' ' << t.dst << ' '
<< ' ' << aut->get_cubeset().dump(d.cube_, *aps)
<< ' ' << d.acc_
<< std::endl;
<< ' ' << aut->get_cubeset().dump(d.cube_, *aps)
<< ' ' << d.acc_
<< std::endl;
}
spot::print_dot(std::cout, spot::twacube_to_twa(aut));

250
tests/ltsmin/modelcheck.cc
View file

@ -75,17 +75,17 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
break;
case 'd':
if (strcmp(arg, "model") == 0)
mc_options.dot_output |= DOT_MODEL;
mc_options.dot_output |= DOT_MODEL;
else if (strcmp(arg, "product") == 0)
mc_options.dot_output |= DOT_PRODUCT;
mc_options.dot_output |= DOT_PRODUCT;
else if (strcmp(arg, "formula") == 0)
mc_options.dot_output |= DOT_FORMULA;
mc_options.dot_output |= DOT_FORMULA;
else
{
std::cerr << "Unknown argument: '" << arg
<< "' for option --dot\n";
return ARGP_ERR_UNKNOWN;
}
{
std::cerr << "Unknown argument: '" << arg
<< "' for option --dot\n";
return ARGP_ERR_UNKNOWN;
}
break;
case 'e':
mc_options.is_empty = true;
@ -154,8 +154,8 @@ static const argp_option options[] =
};
const struct argp finput_argp = { options, parse_opt_finput,
nullptr, nullptr, nullptr,
nullptr, nullptr };
nullptr, nullptr, nullptr,
nullptr, nullptr };
const struct argp_child children[] =
{
@ -184,12 +184,12 @@ static int checked_main()
if (mc_options.selfloopize)
{
if (mc_options.dead_ap == nullptr ||
!strcasecmp(mc_options.dead_ap, "true"))
deadf = spot::formula::tt();
!strcasecmp(mc_options.dead_ap, "true"))
deadf = spot::formula::tt();
else if (!strcasecmp(mc_options.dead_ap, "false"))
deadf = spot::formula::ff();
deadf = spot::formula::ff();
else
deadf = env.require(mc_options.dead_ap);
deadf = env.require(mc_options.dead_ap);
}
@ -197,39 +197,39 @@ static int checked_main()
{
tm.start("parsing formula");
{
auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
exit_code = pf.format_errors(std::cerr);
f = pf.f;
auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
exit_code = pf.format_errors(std::cerr);
f = pf.f;
}
tm.stop("parsing formula");
tm.start("translating formula");
{
spot::translator trans(dict);
// if (deterministic) FIXME
// trans.set_pref(spot::postprocessor::Deterministic);
prop = trans.run(&f);
spot::translator trans(dict);
// if (deterministic) FIXME
// trans.set_pref(spot::postprocessor::Deterministic);
prop = trans.run(&f);
}
tm.stop("translating formula");
atomic_prop_collect(f, &ap);
if (mc_options.dot_output & DOT_FORMULA)
{
tm.start("dot output");
spot::print_dot(std::cout, prop);
tm.stop("dot output");
}
{
tm.start("dot output");
spot::print_dot(std::cout, prop);
tm.stop("dot output");
}
}
if (mc_options.model != nullptr)
{
tm.start("loading ltsmin model");
try
{
model = spot::ltsmin_model::load(mc_options.model)
.kripke(&ap, dict, deadf, mc_options.compress);
}
{
model = spot::ltsmin_model::load(mc_options.model)
.kripke(&ap, dict, deadf, mc_options.compress);
}
catch (std::runtime_error& e)
{
std::cerr << e.what() << '\n';
@ -237,23 +237,23 @@ static int checked_main()
tm.stop("loading ltsmin model");
if (!model)
{
exit_code = 2;
goto safe_exit;
}
{
exit_code = 2;
goto safe_exit;
}
if (mc_options.dot_output & DOT_MODEL)
{
tm.start("dot output");
spot::print_dot(std::cout, model);
tm.stop("dot output");
}
{
tm.start("dot output");
spot::print_dot(std::cout, model);
tm.stop("dot output");
}
if (mc_options.kripke_output)
{
tm.start("kripke output");
spot::print_hoa(std::cout, model);
tm.stop("kripke output");
}
{
tm.start("kripke output");
spot::print_hoa(std::cout, model);
tm.stop("kripke output");
}
}
if (mc_options.formula != nullptr &&
@ -262,92 +262,92 @@ static int checked_main()
product = spot::otf_product(model, prop);
if (mc_options.is_empty)
{
const char* err;
echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err);
if (!echeck_inst)
{
std::cerr << "Unknown emptiness check algorihm `"
<< err << "'\n";
exit_code = 1;
goto safe_exit;
}
{
const char* err;
echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err);
if (!echeck_inst)
{
std::cerr << "Unknown emptiness check algorihm `"
<< err << "'\n";
exit_code = 1;
goto safe_exit;
}
auto ec = echeck_inst->instantiate(product);
assert(ec);
int memused = spot::memusage();
tm.start("running emptiness check");
spot::emptiness_check_result_ptr res;
try
{
res = ec->check();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory during emptiness check."
<< std::endl;
if (!mc_options.compress)
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;
auto ec = echeck_inst->instantiate(product);
assert(ec);
int memused = spot::memusage();
tm.start("running emptiness check");
spot::emptiness_check_result_ptr res;
try
{
res = ec->check();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory during emptiness check."
<< std::endl;
if (!mc_options.compress)
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;
ec->print_stats(std::cout);
std::cout << memused << " pages allocated for emptiness check"
<< std::endl;
if (!res)
{
std::cout << "no accepting run found";
}
else if (!mc_options.compute_counterexample)
{
std::cout << "an accepting run exists "
<< "(use -c to print it)" << std::endl;
exit_code = 1;
}
else
{
exit_code = 1;
spot::twa_run_ptr run;
tm.start("computing accepting run");
try
{
run = res->accepting_run();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory while looking for counterexample."
<< std::endl;
exit_code = 2;
exit(exit_code);
}
tm.stop("computing accepting run");
if (!res)
{
std::cout << "no accepting run found";
}
else if (!mc_options.compute_counterexample)
{
std::cout << "an accepting run exists "
<< "(use -c to print it)" << std::endl;
exit_code = 1;
}
else
{
exit_code = 1;
spot::twa_run_ptr run;
tm.start("computing accepting run");
try
{
run = res->accepting_run();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory while looking for counterexample."
<< std::endl;
exit_code = 2;
exit(exit_code);
}
tm.stop("computing accepting run");
if (!run)
{
std::cout << "an accepting run exists" << std::endl;
}
else
{
tm.start("reducing accepting run");
run = run->reduce();
tm.stop("reducing accepting run");
tm.start("printing accepting run");
std::cout << *run;
tm.stop("printing accepting run");
}
}
}
if (!run)
{
std::cout << "an accepting run exists" << std::endl;
}
else
{
tm.start("reducing accepting run");
run = run->reduce();
tm.stop("reducing accepting run");
tm.start("printing accepting run");
std::cout << *run;
tm.stop("printing accepting run");
}
}
}
if (mc_options.dot_output & DOT_PRODUCT)
{
tm.start("dot output");
spot::print_dot(std::cout, product);
tm.stop("dot output");
}
{
tm.start("dot output");
spot::print_dot(std::cout, product);
tm.stop("dot output");
}
}
safe_exit:
@ -363,7 +363,7 @@ main(int argc, char** argv)
{
setup(argv);
const argp ap = { nullptr, nullptr, nullptr,
argp_program_doc, children, nullptr, nullptr };
argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
exit(err);