了解合金中的谓词答案

【问题标题】：Understanding predicates in alloy了解合金中的谓词
【发布时间】：2012-11-14 09:19:23
【问题描述】：

有人可以使用以下示例帮助我理解谓词吗：

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) 谁能给我看一下使用上面代码的合金代码，并通过代码阐明谓词的含义。

我只是想了解我们如何使用上述谓词。

【问题讨论】：

这是作业吗？不会以任何方式隐瞒信息，只是想知道:)
没有。我想在短时间内捡起合金。因此，认为使用 Stack Overflow 是一个好主意，因为他们的网站说 SO 是询问合金相关信息的最佳场所
老板打来电话，抱歉耽搁了，我正在准备答复:) 但需要一段时间。
太棒了。我在等待。发布了另一个关于集合的简单问题。请帮忙。信号 A { 相对 : 设置 B }。 set 是否引用 0 或更多。还是指1个或多个

标签： alloy

【解决方案1】：

在您调用命令中的谓词或函数以查找示例或反例之前，什么都不会“发生”。

【讨论】：

如果没有这样的实例满足谓词会发生什么。另外，您能否使用上面的示例给我一些可运行的合金代码，以便我可以尝试不同的东西。
在 mostRed 的定义中，set 是指（0 或更多）还是指（1 或更多）？

【解决方案2】：

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

此外，您的模型不完整，因为没有 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。

希望这会有所帮助。

【讨论】：

【解决方案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)
}

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

从函数 redligths 返回的集合 A（在本例中为关系 (j.lights)）与另一个集合 B 之间的区别，其中 Predicate 将始终约束约束分析器在您运行时仅返回红光谓词“mostlyRed”。

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

【讨论】：