1

次の例を使用して、誰かが述語を理解するのを手伝ってくれませんか。

sig Light{}
sig LightState { color: Light -> one Color}
sig Junction {lights: set Light}
fun redLigths(s:LightState) : set Light{ s.color.Red}
pred mostlyRed(s:LightState, j:Junction){
    lone j.lights - redLigths(s)
}

上記のコードについて、以下の質問があります。

1）上記の述語が真の場合はどうなりますか？

2）それが偽の場合はどうなりますか？

3）誰かが上記のコードを使用し、コードを通じて述語の意味を明確にする少しの合金コードを見せてもらえますか？

上記の述語をどのように使用するかを理解しようとしています。

4

3 に答える 3

3

例または反例を見つけるためにコマンドで述語または関数を呼び出すまで、何も「起こりません」。

于 2012-11-14T15:16:57.017 に答える
3

まず、正しい用語を使用します。述語が真の場合、「何も起こりません」。逆の場合と同様に、インスタンス（セットへのアトムの割り当て）は、ある条件を満たし（または満たさず）、述語をtrue（またはfalse）にします。

また、 （という属性を含める必要がある）のsig宣言がないため、モデルは不完全です。ColorRed

信号機を含む交差点のある世界をモデル化する場合は、次のモデルを使用します。

abstract sig Color {}

one sig Red,Yellow,Green extends Color {}

sig Light {
    color: Color
}

sig Junction {
    lights : set Light
}

// This is just for realism, make sure each light belongs to exactly one junction
fact {
    Light = Junction.lights
    no x,y:Junction | x!=y and some x.lights & y.lights
}

fun count[j:Junction, c:Color] : Int { 
    #{x:Light | x in j.lights and x.color=c}
}

pred mostly[j:Junction, c:Color] {
    no cc:Color | cc!=c and count[j,cc]>=count[j,c]
}

run{
    some j:Junction | mostly[j,Red]
} for 10 Light, 2 Junction, 10 int

上記を見て、私は＃演算子を使用してセット内の原子の数をカウントしています。また、＃演算子を使用してオーバーフローに遭遇しないように、整数に10のビット幅を指定しています。大きなセット。

これを実行すると、ほとんどが赤信号である少なくとも1つのジャンクションを持つインスタンスが取得さ$jれ、ビジュアライザーでマークされます。

お役に立てれば。

于 2012-11-14T21:36:50.527 に答える
0 
sig Light{}
sig LightState { color: Light -> one Color}
sig Junction {lights: set Light}
fun redLigths(s:LightState) : set Light{ s.color.Red}
pred mostlyRed(s:LightState, j:Junction){
lone j.lights - redLigths(s)
}

あなたが与えた例で述語が単に意味することは次のとおりです。

セット A (この場合はリレーション (j.lights)) と別のセット B の違いは、関数 redligths から返されます。述語は、述語を実行したときに制約アナライザーを常に制約し、赤い光のみを返すようにします。ほとんど赤」。

そして、述語の本体に追加した多重度 " lone " は、セット A と B の差 (私が想定したように) が評価された後にのみ評価され、最大で 1 つの赤のアトムが返されることを確認することに注意してください。私の説明がお役に立てば幸いです。肯定的な批判を歓迎します。ありがとう

于 2013-01-14T11:31:22.303 に答える