I have a model with this sig:
sig Thing {}
sig World {
quantities: Thing ->one Int,
}
I want to define a constraint on the quantities
relationship such that the quantity of each Thing must be a positive int.
I am total beginner with Alloy (and I have no theory background to draw on, am just a Python programmer). I followed through the tutorial but I did not see a recipe for what I want to do.
I know how to:
fact {
all w: World | w.quantities <something>
}
...but I am not clear how to address members of the right-hand-side of the relationship when writing a fact.
I have defined it as a relationship (rather than having a quantity
property on the Thing
sig) because I understood from the tutorial that this was necessary in a dynamic model where I want to update the quantity of Things via predicates.
I tried defining a:
sig PositiveInt extends Int {}
...but this is not allowed.
updated This kind of subtyping works (imho) best with set enumeration: