A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

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

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

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

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

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