5

Alloy 4 文法では、署名宣言 (およびその他のいくつかのもの) にprivateキーワードを含めることができます。また、仕様に次の形式の列挙宣言を含めることもできます。

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

言語リファレンスには、(私が知る限り)privateキーワードまたはenum構成要素の意味が記述されていません。

利用可能なドキュメントはありますか? それとも、将来の仕様のために予約されている構文として文法にありますか?

4

2 に答える 2

3

これは、これら 2 つのキーワードに関する私の非公式な理解です。

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キーワードは、sig にprivate属性がある場合、そのラベルが同じモジュール内で非公開であることを意味します。同じことがプライベート フィールドとプライベート関数にも当てはまります。

于 2012-08-16T18:57:11.943 に答える
1

enum以前に受け入れられた回答に加えて、特に標準との主な違いについて、Alloy on s での1 週間の経験から得られたいくつかの有用な洞察を追加したいと思いsigます。

を使用abstract sig + extendすると、同じ概念に対応するセットが多数存在するモデルが作成されます。たぶん、例がそれをより明確にすることができます。次のようなものとします

sig Car {
    dameges: set Damage
}

使用する選択肢があります

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

対

enum Damage {
    MajorDamage, MinorDamage
}

最初のケースでは、車に関連付けられたさまざまな MinorDamage アトム (MinorDamage0、MinorDamage1、...) を持つモデルを考え出すことができますが、2 番目のケースでは、異なる車が参照できる MinorDamage は常に 1 つだけです。

この場合、abstract sig + extendフォームを使用することにはある程度の意味があります (さまざまな MinorDamage または MajorDamage 要素を追跡することを決定できるため)。

一方、currentState: set Stateを使用したい場合は、

enum State {Damaged, Parked, Driven}

State概念をマッピングして、それぞれCarが参照できる正確に 3 つを持つようにします。このように、 では、Visualizerモデルを 1 つの状態だけに投影することを決定でき、Carこの状態に関連付けられているすべての がハイライト表示されます。もちろん、コンストラクトでそれを行うことはできませんabstract + extend。投影すると、それに関連するものMajorDamage0だけが強調表示され、それ以外は何も強調表示されないためです。CarDamage

結論として、それは本当にあなたがしなければならないことにかかっています。

また、X要素で構成された列挙型を持っている場合、実行することに注意してください

run some_predicate for Y

Y < X の場合、Alloy はインスタンスをまったく生成しません。したがって、最後の例では、Y < 3 を持つことはできません。

最後の注意として、マジック レイアウト ボタンを使用する場合、列挙型が常にビジュアライザーに表示されるわけではありませんが、前述したように、モデルを列挙型に「投影」して、列挙型のさまざまな要素を切り替えることができます。

于 2016-11-06T07:54:37.233 に答える