Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2020-08-08 01:56:02
- Maxvonhippel
- Member
- Registered: 2019-09-13
- Posts: 20
[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
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: 20
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