在合金方面需要帮助答案

【问题标题】：Need help in Alloy在合金方面需要帮助
【发布时间】：2013-12-01 13:26:22
【问题描述】：

这是一个合金的例子，我发现我想用 3 个谓词、3 个事实、3 个对象和 3 个断言来制作它，有人可以帮我吗？我是 Alloy 的新手，需要一些即时帮助。

abstract sig Color {}

one sig Red,Yellow,Green extends Color {}

sig Light {
color: Color
}

sig Junction {
lights : set Light
}

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

// 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
Light = Junction.lights
no y,x:Junction | y!=x and some y.lights & x.lights

}

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`

【问题讨论】：

标签： alloy

【解决方案1】：

在 Alloy 中，您只能为模型中每个 sig 的对象（原子）数量提供范围。您在模型中显式编写的谓词、函数和断言，Alloy Analyzer 不会以任何方式“扩展”它们，也无法对其进行量化，因此为它们提供单独的范围是没有意义的。

【讨论】：