4

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

Lao Tse
  • 171
  • 3
  • 12
  • I had a similar question, the answer may be useful https://stackoverflow.com/questions/52690845/alloy-define-relation-to-only-positive-integers/52697248?noredirect=1#comment92330595_52697248 – Anentropic Oct 09 '18 at 12:29

1 Answers1

2

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 }
Aleksandar Milicevic
  • 3,837
  • 1
  • 13
  • 17
  • but i have a little issue with that: I want to say: that an int is between 0 and somewhat. for example i have this sig: sig A{ id: int } and i use this facts: fact{ all a:A | a.id > 0 } fact{ all a:A | a.id < 20 } I get no instances. what am i doing wrong? – Lao Tse Apr 11 '14 at 06:40
  • I realized that one fact is wrong. in the following my model and the fact I think is wrong: ` sig State extends StateOrJunction{ actionID:one Int, superState:lone State, subStates:set State} sig Transition{ conditionID:one Int, destination:one StateOrJunction, source:lone StateOrJunction} abstract sig StateOrJunction{ transitions:set Transition}` The fact I suppose is wrong is the following: fact{ all s:State | no s':(State-s) | s.actionID = s'.actionID } I want to say that all states have disjoint actionIDs. – Lao Tse Apr 28 '14 at 08:34