Spinroot

A forum for Spin users

You are not logged in.

#1 2012-06-07 21:37:18

Beth
Member
Registered: 2012-03-19
Posts: 11

Modelling large models with large integers limit

Hi,
   I am in the process of modelling an RSA-based digital signature in SPIN but i got a hitch. The integer limit in SPIN is approximately (2×10^9) but for my model to work as expected, i need to implement at least a limit of approximately (2×10^16) and more .What kind of abstraction would you advice me to apply??

Offline

#2 2012-06-09 18:42:14

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Modelling large models with large integers limit

Often you can verify problems that have very large limits by defining a much smaller version of the problem.
Basically, what you are looking for is what we call the 'smallest sufficient model:'  small enough to represent the boundary cases, but not so small that the essence of the problem itself changes.
So you'd want to find a representation of this problem that requires no more than, say a range of 2^8 or so (to pick a very low bound), rather than the real bound which would put a verification with model checking far out of reach....

Offline

#3 2012-06-10 23:14:42

Beth
Member
Registered: 2012-03-19
Posts: 11

Re: Modelling large models with large integers limit

Thanx alot, will do that.

Offline

Board footer

Powered by FluxBB