Alloyの 'private'キーワードの意味は？ 'enum'宣言の意味ですか？

Question

Alloy 4 grammarは、署名宣言（およびその他のもの）にprivateというキーワードを付けることを許可します。また、仕様は（私の知る限り）privateキーワードまたはenum構造のいずれかの意味を説明していない形

enum nephews { hughie, louis, dewey } 
enum ducks { donald, daisy, scrooge, nephews } 

The language referenceの列挙宣言を含めることができことができます。

マニュアルはありますか？あるいは、彼らは将来の仕様のために予約されている構文として文法に入っていますか？

Answer 1

これは私がこれらの2つのキーワードを非公式に理解したものです。

enum nephews { hughie, louis, dewey } 

privateキーワードはSIGがprivate属性を持っている場合、そのラベルは、同じモジュール内のプライベートであることを意味

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 
} 

と意味的に等価です。プライベートフィールドとプライベート関数についても同様です。

Answer 2

これまでの承認済みの回答に加えて、enumの合金に関する1週間の経験から得た有用な洞察、特に標準のsigの主な違いを追加したいと思います。

abstract sig + extendを使用する場合は、同じ概念に対応するセットが多数あるモデルを作成します。たぶん、例がそれをより明確にするかもしれない。

sig Car { 
    dameges: set Damage 
} 

よう と仮定気にいらあなたは

我々は異なるMinorDamage原子（MinorDamage0、とモデルwiht考え出すことができる最初のケースで

enum Damage { 
    MajorDamage, MinorDamage 
} 

対

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

を使用するための選択肢を持っていますMinorDamage1、...）はCarsに関連付けられ、後者の場合は、常に異なるCarsが参照できるMinorDamageが1つしかありません。

フォームを使用すると、（この場合、MinorDamageまたはMajorDamageの別の要素を追跡することができるので）意味があります。一方

、あなたはcurrentState: set Stateを持つようにしたい場合は、ちょうど3 StateがそれぞれCarが参照できるためにどのようにするために、コンセプトをマッピングするために

enum State {Damaged, Parked, Driven} 

を使用するより良いかもしれません。このように、Visualizerでは、あなたのモデルを正確に1つの状態に投影することができ、この状態に関連付けられているCarをすべて強調表示します。もちろん、MajorDamage0に投影すると、そのDamageに関連付けられたCarのみが強調表示され、それ以外は表示されないため、abstract + extend構成ではそのことはできません。

結論として、本当にあなたがしなければならないことに依存しています。

はまた、あなたがXの要素によって構成さ列挙型を持っているとあればY < Xは、合金はまったくのインスタンスを生成しない

run some_predicate for Y 

を実行していることに注意してください。 最後の例では、Yを使用できません。

最後に、マジックレイアウトボタンを使用すると、ビジュアライザに列挙型が常に現れるとは限りませんが、前に列挙型にモデルを「投影」し、列挙型のさまざまな要素を切り替えることができます。