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

swarming: bug fix

Browse source 
This is an important bug fix. When swarming
is activated, some multiplication is performed
to find a successor. This multiplication could,
eventually, overflow... Using larger types solves
the problem.

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
This commit is contained in:
Etienne Renault 2018-07-16 07:14:58 +00:00
parent 69457e957b
commit d1200cb579
2 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
spot/ltsmin/spins_kripke.hh
View file

@ -149,6 +149,9 @@ namespace spot
cube condition() const; cube condition() const;
private: private:
/// Compute the real index in the successor vector
unsigned compute_index() const;
std::vector<cspins_state> successors_; std::vector<cspins_state> successors_;
unsigned int current_; unsigned int current_;
cube cond_; cube cond_;

11
spot/ltsmin/spins_kripke.hxx
View file

@ -203,8 +203,15 @@ namespace spot
{ {
if (SPOT_UNLIKELY(!tid_)) if (SPOT_UNLIKELY(!tid_))
return successors_[current_]; return successors_[current_];
return successors_[(((current_+1)*primes[tid_]) return successors_[compute_index()];
% ((int)successors_.size()))]; }
unsigned cspins_iterator::compute_index() const
{
unsigned long long c = current_ + 1;
unsigned long long p = primes[tid_];
unsigned long long s = successors_.size();
return (unsigned) ((c*p) % s);
} }
cube cspins_iterator::condition() const cube cspins_iterator::condition() const