Meaning of 'private' keyword in Alloy? Meaning of 'enum' declaration?

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?

score 3 · Accepted Answer · answered Aug 16 '12 at 18:57

3

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.

answered Aug 16 '12 at 18:57

Aleksandar Milicevic

3,837
1
13
17

Thank you; this is helpful. I suppose it follows that using the same name both in an enumeration and as the name of another enumeration would be an error. (Well, that's easily checkable, why am I asking when I can find out for myself? -- yes, Alloy 4.2RC flags it as an error. OK, thanks again.) – C. M. Sperberg-McQueen Aug 17 '12 at 00:16
I see also that `private` is documented at http://alloy.mit.edu/alloy/documentation/quickguide/private.html – C. M. Sperberg-McQueen Aug 17 '12 at 15:30

tigerjack · Answer 2 · 2016-11-06T08:00:49.910

In addition to the previous accepted answer, I'd like to add some useful insights coming from a one-week experience with Alloy on enums, 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 Cars 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.

Meaning of 'private' keyword in Alloy? Meaning of 'enum' declaration?

2 Answers2