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?

Answer 1

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.