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

simulation: use tuple and emplace_back for constraints

Browse source 
* src/tgbaalgos/simulation.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-29 21:50:57 +01:00
parent ba5aff2460
commit 83ed4f8c90
1 changed files with 16 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/tgbaalgos/simulation.cc
View file

@ -149,7 +149,7 @@ namespace spot
typedef std::map<constraint_key, bdd, typedef std::map<constraint_key, bdd,
constraint_key_comparator> map_constraint; constraint_key_comparator> map_constraint;
typedef std::pair<constraint_key, bdd> constraint; typedef std::tuple<const state*, const state*, bdd> constraint;
// Helper to create the map of constraints to give to the // Helper to create the map of constraints to give to the
// simulation. // simulation.
@ -157,10 +157,9 @@ namespace spot
map_constraint& feed_me) map_constraint& feed_me)
{ {
for (auto& p: list) for (auto& p: list)
{ feed_me.insert(std::make_pair(std::make_pair(std::get<0>(p),
if (feed_me.find(p.first) == feed_me.end()) std::get<1>(p)),
feed_me[p.first] = p.second; std::get<2>(p)));
}
} }
@ -1124,9 +1123,6 @@ namespace spot
// return bddfalse != bdd_restrict(b, !on_cycle_); // return bddfalse != bdd_restrict(b, !on_cycle_);
} }
#define create_cstr(src, dst, constraint) \
std::make_pair(std::make_pair(src, dst), constraint)
// This method solves three kind of problems, where we have two // This method solves three kind of problems, where we have two
// conjunctions of variable (that corresponds to a particular // conjunctions of variable (that corresponds to a particular
// transition), and where left could imply right. // transition), and where left could imply right.
@ -1165,10 +1161,9 @@ namespace spot
{ {
assert(src_right != dst_right); assert(src_right != dst_right);
constraint constraint.emplace_back(new_original_[old_name_[src_right]],
.push_back(create_cstr(new_original_[old_name_[src_right]], new_original_[old_name_[dst_right]],
new_original_[old_name_[dst_right]], add);
add));
} }
} }
else if (out_scc_left && !out_scc_right) else if (out_scc_left && !out_scc_right)
@ -1181,10 +1176,9 @@ namespace spot
{ {
assert(src_left != dst_left); assert(src_left != dst_left);
constraint constraint.emplace_back(new_original_[old_name_[src_left]],
.push_back(create_cstr(new_original_[old_name_[src_left]], new_original_[old_name_[dst_left]],
new_original_[old_name_[dst_left]], add);
add));
} }
} }
else if (out_scc_left && out_scc_right) else if (out_scc_left && out_scc_right)
@ -1197,14 +1191,12 @@ namespace spot
{ {
assert(src_left != dst_left && src_right != dst_right); assert(src_left != dst_left && src_right != dst_right);
// FIXME: cas pas compris. // FIXME: cas pas compris.
constraint constraint.emplace_back(new_original_[old_name_[src_left]],
.push_back(create_cstr(new_original_[old_name_[src_left]], new_original_[old_name_[dst_left]],
new_original_[old_name_[dst_left]], add);
add)); constraint.emplace_back(new_original_[old_name_[src_right]],
constraint new_original_[old_name_[dst_right]],
.push_back(create_cstr(new_original_[old_name_[src_right]], add);
new_original_[old_name_[dst_right]],
add));
} }
} }