diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index c7bbec95e..ea3eec47b 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -149,6 +149,9 @@ namespace spot cube condition() const; private: + /// Compute the real index in the successor vector + unsigned compute_index() const; + std::vector successors_; unsigned int current_; cube cond_; diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx index 928d767b7..ff6457654 100644 --- a/spot/ltsmin/spins_kripke.hxx +++ b/spot/ltsmin/spins_kripke.hxx @@ -203,8 +203,15 @@ namespace spot { if (SPOT_UNLIKELY(!tid_)) return successors_[current_]; - return successors_[(((current_+1)*primes[tid_]) - % ((int)successors_.size()))]; + return successors_[compute_index()]; + } + + 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