CODEWITHSUNDEEP
integeralloy
Lao Tse
Lao Tse

Reputation: 191

Alloy: facts etc. about Int

i am recently working with Alloy. Can I say something like:

fact{
all i: Int | i >= 0 
}

I want to say: all Integer which Alloy uses should be positive. Alloy doesn't fail but also don't give me instances.

greetings

Upvotes: 5

Views: 1512

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

You can't currently say that. The only scope you can specify for integers (which tells Alloy which integers to "use") is the bitwidth (e.g., 4 Int); Alloy then always uses all integers within that bitwidth (e.g., for bitwidth of 4, integers used are -8, ..., 7).

If you have a field of type Int in your model, you can use a fact (like you said above) to restrict its values:

sig S { i: Int }
fact  { all s: S | s.i >= 0 }

Upvotes: 3

Related Questions