Meaning of 'private' keyword in Alloy? Meaning of 'enum' declaration?
-
26-06-2021 - |
Question
The Alloy 4 grammar allows signature declarations (and some other things) to carry a private
keyword. It also allows Allow specifications to contain enumeration declarations of the form
enum nephews { hughie, louis, dewey }
enum ducks { donald, daisy, scrooge, nephews }
The language reference doesn't (as far as I can tell) describe the meaning of either the private
keyword or the enum
construct.
Is there documentation available? Or are they in the grammar as constructs that are reserved for future specification?
Solution
This is my unofficial understanding of those two keywords.
enum nephews { hughie, louis, dewey }
is semantically equivalent to
open util/ordering[nephews] as nephewsOrd
abstract sig nephews {}
one sig hughie extends nephews {}
one sig louis extends nephews {}
one sig dewey extends nephews {}
fact {
nephewsOrd/first = hughie
nephewsOrd/next = hughie -> louis + louis -> dewey
}
The private
keyword means that if a sig has the private
attribute, its label is private within the same module. The same applies for private fields and private functions.
OTHER TIPS
In addition to the previous accepted answer, I'd like to add some useful insights coming from a one-week experience with Alloy on enum
s, in particular on the main differences with standard sig
.
If you use abstract sig + extend
, you'll come up with a model in which there are many sets corresponding to the same concept. Maybe an example could clarify it better.
Suppose somthing like
sig Car {
dameges: set Damage
}
You have the choice to use
abstract sig Damage {}
sig MajorDamage, MinorDamage extends Damage {}
vs
enum Damage {
MajorDamage, MinorDamage
}
In the first case we can come up wiht a model with different MinorDamage atoms (MinorDamage0, MinorDamage1, ...) associatet to Cars, while in the second case you always have only one MinorDamage to which different Cars can refer.
It could have some sense in this case to use an abstract sig + extend
form (because you can decide to track different MinorDamage or MajorDamage elements).
On the other hand, if you want to have a currentState: set State
, it could be better to use an
enum State {Damaged, Parked, Driven}
to map the concept, in order to have exactly three State
to which each Car
can refer to. In this way, in the Visualizer
, you can decide to project your model on exactly one of the states and it will highlight all the Car
s associated to this state. You can't do that with the abstract + extend
construct, of course, because projecting over MajorDamage0
will highlight only the Car
associated to that Damage
and nothing else.
So, in conclusion, it really depends on what you have to do.
Also, keep in mind that if you have an enum composed by X elements and execute
run some_predicate for Y
where Y < X, Alloy produces no instance at all. So, in our last example, we can't have a Y < 3.
As a last note, enums don't always appear in the Visualizer if you use the Magic Layout button, but as I said previously you can "project" your model over the enum and switch between the different elements of the enum.