Commit d956fdc3 authored by Etienne Renault's avatar Etienne Renault

swarming: bug fix

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.
parent cbc17663
...@@ -149,6 +149,9 @@ namespace spot ...@@ -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_;
......
...@@ -203,8 +203,15 @@ namespace spot ...@@ -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
......
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