瞭解謂詞

Question

有人可以幫我用下面的例子理解斷言：

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）有人可以向我展示一些合金代碼，它使用上面的代碼，並通過代碼闡明謂詞的含義。

我只是想了解我們如何使用上述謂詞。

Answer 1

直到您在命令中調用謂詞或函數以查找示例或反例時，纔會發生「發生」。

Answer 2

首先，使用正確的術語，當謂詞爲真時不會發生任何事情;它更像另一種方式，一個實例（一組原子分配）滿足（或不）某種條件，使得謂詞爲真（或錯誤）。

此外，您的型號不完整，因爲Color（其中應該包含名爲Red的屬性）的sig聲明沒有。

我假設你想用含紅綠燈十字路口世界建模，如果是的話，我會用以下模型：

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位整數的位寬，這樣我就不會在大集合中使用＃運算符時發生溢出。

當您執行此操作時，您將得到一個實例，其中至少有一個結點大部分爲紅燈，它將在可視化工具中標記爲$j。

希望這會有所幫助。

Answer 3

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返回，其中Predicate將始終約束約束分析器，使其只在您返回時才返回紅燈運行Predicate「mostlyRed」。

並注意多樣性「孤獨」你添加到謂詞的身體只能在設定的A和B之間的差異後評估（我認爲）進行了評估，以確保的至多一個原子返回紅色。我希望我的解釋有幫助。我會歡迎積極的批評。謝謝