Spinroot

A forum for Spin users

You are not logged in.

#1 2020-08-08 01:56:02

Maxvonhippel
Member
Registered: 2019-09-13
Posts: 19

[SOLVED] Best practice for bounded signed integers?

Suppose I want to deal with some bounded signed integers, such as, -30 through 30.  In particular, what I want is something like this:

chan example = [1] of { -30 ... 30 }

What is the best way to accomplish this?  If I didn't want negative numbers I think I could use an unsigned of only so-many bits, and I guess I could do that with a sign-bit to get what I want, but it seems kind of inelegent.

Thank you!

Last edited by Maxvonhippel (2020-08-15 03:33:42)

Offline

#2 2020-08-08 20:19:38

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

Re: [SOLVED] Best practice for bounded signed integers?

there's currently no mechanism in the language for specifying this.
the closest you could get would be to use a short, or, as you suggested,
a bitfield of 6 bits -- giving 64 possible values, the first 31 of which
could be treated as negative numbers and the rest 0..31 positive

Offline

#3 2020-08-14 00:22:22

Maxvonhippel
Member
Registered: 2019-09-13
Posts: 19

Re: [SOLVED] Best practice for bounded signed integers?

Thank you for the quick response Gerard, I appreciate it.  Wiring my own arithmetic seems a bit ugly, although of course doable.  Is there some way I could alternatively just tell Spin to ignore states under some condition?  Then I could say, "ignore any states where such-and-such integers are out-of-bounds."  I know this is a feature in Alloy, which makes me think maybe it is available in Promela ... if not no worries, I can work out the arithmetic.  Thank you!

Offline

#4 2020-08-14 06:08:59

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

Re: [SOLVED] Best practice for bounded signed integers?

sorry, no there's no mechanism to specify that...

Offline

Board footer

Powered by FluxBB