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

首先，使用正确的术语，当谓词为真时，什么都不会发生；相反，它更像是一个实例（将原子分配给集合）满足（或不满足）某些条件，从而使谓词为真（或假）。

此外，您的模型不完整，因为没有sig声明Color（应该包括一个名为 的属性Red）。

我假设您想模拟一个包含交通信号灯的十字路口的世界，如果是这样，我将使用以下模型：

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在可视化工具中标记为。

希望这可以帮助。

于 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)
}

在您给出的示例中，谓词的简单含义是；

从函数 redligths 返回的集合 A（在本例中为关系 (j.lights) 和另一个集合 B 之间的差异，其中 Predicate 将始终约束约束分析器在运行 Predicate 时仅返回红光”多为红色”。

请注意，您添加到谓词主体的多重性“孤独”仅在评估集合 A 和 B 之间的差异（如我所假设的）之后评估，以确保最多返回一个红色原子。我希望我的解释是有帮助的。我会欢迎积极的批评。谢谢

于 2013-01-14T11:31:22.303 回答