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

ltsmin: simplify iterator

Browse source 
* spot/ltsmin/ltsmin.cc: here.
This commit is contained in:
Etienne Renault 2017-03-15 16:01:00 +01:00
parent ac54acbb9d
commit 8a930c7572
1 changed files with 5 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

18
spot/ltsmin/ltsmin.cc
View file

@ -1237,10 +1237,9 @@ namespace spot
{ {
cspins_state_manager* manager; // The state manager cspins_state_manager* manager; // The state manager
std::vector<cspins_state>* succ; // The successors of a state std::vector<cspins_state>* succ; // The successors of a state
cspins_state_map map; // Must be a copy! cspins_state_map map; // Must be a copy and only one copy/thread
int* compressed_; int* compressed_;
int* uncompressed_; int* uncompressed_;
int default_value_;
bool compress; bool compress;
bool selfloopize; bool selfloopize;
}; };
@ -1254,9 +1253,7 @@ namespace spot
cspins_iterator(cspins_state s, cspins_iterator(cspins_state s,
const spot::spins_interface* d, const spot::spins_interface* d,
cspins_state_manager& manager, cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner, inner_callback_parameters& inner,
int defvalue,
cube cond, cube cond,
bool compress, bool compress,
bool selfloopize, bool selfloopize,
@ -1266,9 +1263,7 @@ namespace spot
{ {
successors_.reserve(10); successors_.reserve(10);
inner.manager = &manager; inner.manager = &manager;
inner.map = map;
inner.succ = &successors_; inner.succ = &successors_;
inner.default_value_ = defvalue;
inner.compress = compress; inner.compress = compress;
inner.selfloopize = selfloopize; inner.selfloopize = selfloopize;
int* ref = s; int* ref = s;
@ -1302,9 +1297,7 @@ namespace spot
void recycle(cspins_state s, void recycle(cspins_state s,
const spot::spins_interface* d, const spot::spins_interface* d,
cspins_state_manager& manager, cspins_state_manager& manager,
cspins_state_map& map,
inner_callback_parameters& inner, inner_callback_parameters& inner,
int defvalue,
cube cond, cube cond,
bool compress, bool compress,
bool selfloopize, bool selfloopize,
@ -1317,8 +1310,6 @@ namespace spot
successors_.clear(); successors_.clear();
inner.manager = &manager; inner.manager = &manager;
inner.succ = &successors_; inner.succ = &successors_;
inner.map = map;
inner.default_value_ = defvalue;
inner.compress = compress; inner.compress = compress;
inner.selfloopize = selfloopize; inner.selfloopize = selfloopize;
int* ref = s; int* ref = s;
@ -1433,6 +1424,7 @@ namespace spot
cspins_state_manager(d_->get_state_size(), compress); cspins_state_manager(d_->get_state_size(), compress);
inner_[i].compressed_ = new int[d_->get_state_size() * 2]; inner_[i].compressed_ = new int[d_->get_state_size() * 2];
inner_[i].uncompressed_ = new int[d_->get_state_size()+30]; inner_[i].uncompressed_ = new int[d_->get_state_size()+30];
inner_[i].map = map_; // Must be a copy per thread
} }
dead_idx_ = -1; dead_idx_ = -1;
match_aps(visible_aps, dead_prop); match_aps(visible_aps, dead_prop);
@ -1492,15 +1484,15 @@ namespace spot
auto tmp = recycle_[tid].back(); auto tmp = recycle_[tid].back();
recycle_[tid].pop_back(); recycle_[tid].pop_back();
compute_condition(tmp->condition(), s, tid); compute_condition(tmp->condition(), s, tid);
tmp->recycle(s, d_, manager_[tid], map_, inner_[tid], -1, tmp->recycle(s, d_, manager_[tid], inner_[tid],
tmp->condition(), compress_, selfloopize_, tmp->condition(), compress_, selfloopize_,
cubeset_, dead_idx_, tid); cubeset_, dead_idx_, tid);
return tmp; return tmp;
} }
cube cond = cubeset_.alloc(); cube cond = cubeset_.alloc();
compute_condition(cond, s, tid); compute_condition(cond, s, tid);
return new cspins_iterator(s, d_, manager_[tid], map_, inner_[tid], return new cspins_iterator(s, d_, manager_[tid], inner_[tid],
-1, cond, compress_, selfloopize_, cond, compress_, selfloopize_,
cubeset_, dead_idx_, tid); cubeset_, dead_idx_, tid);
} }