Значение ключевого слова «частное» в Alloy? Значение объявления enum?

Это мое неофициальное понимание этих двух ключевых слов.

enum nephews { hughie, louis, dewey }

семантически эквивалентен

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
}

Ключевое слово private означает, что если сигнал имеет атрибут private, его метка является частной в пределах того же модуля. То же самое относится к приватным полям и приватным функциям.

В дополнение к предыдущему принятому ответу я хотел бы добавить некоторые полезные идеи, полученные в результате недельного опыта работы с Alloy на enums, в частности об основных отличиях от стандартного sig.

Если вы используете abstract sig + extend, вы получите модель, в которой есть много наборов, соответствующих одному и тому же понятию. Может быть, пример мог бы прояснить это лучше. Предположим, что-то вроде

sig Car {
    dameges: set Damage
}

У вас есть возможность использовать

abstract sig Damage {}
sig MajorDamage, MinorDamage extends Damage {}

vs

enum Damage {
    MajorDamage, MinorDamage
}

В первом случае мы можем придумать модель с разными атомами MinorDamage (MinorDamage0, MinorDamage1, ...), связанными с автомобилями, а во втором случае у вас всегда будет только один MinorDamage, на который могут ссылаться разные автомобили.

В этом случае может иметь смысл использовать форму abstract sig + extend (поскольку вы можете решить отслеживать разные элементы MinorDamage или MajorDamage).

С другой стороны, если вы хотите иметь currentState: set State, лучше использовать

enum State {Damaged, Parked, Driven}

чтобы сопоставить концепцию, чтобы иметь ровно три State, к которым может относиться каждый Car. Таким образом, в Visualizer вы можете спроецировать свою модель ровно на одно из состояний, и она выделит все Car, связанные с этим состоянием. Конечно, вы не можете сделать это с конструкцией abstract + extend, потому что проецирование на MajorDamage0 выделит только Car, связанное с этим Damage, и ничего больше.

Итак, в заключение, это действительно зависит от того, что вы должны делать.

Кроме того, имейте в виду, что если у вас есть перечисление, состоящее из X элементов, и выполните

run some_predicate for Y

где Y ‹ X, Alloy вообще не создает экземпляров. Итак, в нашем последнем примере у нас не может быть Y ‹ 3.

И последнее замечание: перечисления не всегда появляются в визуализаторе, если вы используете кнопку Magic Layout, но, как я уже говорил ранее, вы можете «проецировать» свою модель на перечисление и переключаться между различными элементами перечисления.