我是合金初学者！
我想表演，例如：
run {all x: {2,3,4,5}, y: {1,2,3,4} | x > y and x + y <=10}
如何解决 Alloy 中的上述约束？
非常感谢！
D.M
如果x和y的值在您希望的区间内，则可以添加约束来强制执行给定属性 .
此外，您需要注意操作符用于set union . 如果 x=4 和 y=5 ，则 x+y 将产生： {4,5} . 您需要调用 add[x,y] 内置函数来执行添加 .
x=4
y=5
x+y
{4,5}
add[x,y]
总而言之，这是你的约束 .
run {all x,y:Int | (x >1 and x <6 and y > 0 and y <5 ) implies x > y and add[x,y] <=10} for 5 Int
注意命令末尾的 for 5 Int ，它告诉分析器它应该在分析中考虑可以在5位内表示的整数，即[-16,15]
for 5 Int
另请注意，当您请求区间[-16,15]中的所有整数组合满足给定条件时，此谓词不一致 .
EDIT
你可以使用let在Alloy中声明“变量” . （在局部变量的另一个结构内部和全局变量的外部）
在您的示例中，您可以编写：
let X= 2+3+6+8+12+17+18+20 let Y= 3+5+6+8+10
记住那是一个集合联合运算符
您的命令可能是：
run {all x :X,y:Y | x > y and add[x,y] <=10} for 6 Int.
请注意，相同的注释适用于此命令（即它不一致）
1 回答
如果x和y的值在您希望的区间内，则可以添加约束来强制执行给定属性 .
此外，您需要注意操作符用于set union . 如果
x=4和y=5，则x+y将产生：{4,5}. 您需要调用add[x,y]内置函数来执行添加 .总而言之，这是你的约束 .
注意命令末尾的
for 5 Int，它告诉分析器它应该在分析中考虑可以在5位内表示的整数，即[-16,15]另请注意，当您请求区间[-16,15]中的所有整数组合满足给定条件时，此谓词不一致 .
EDIT
你可以使用let在Alloy中声明“变量” . （在局部变量的另一个结构内部和全局变量的外部）
在您的示例中，您可以编写：
记住那是一个集合联合运算符
您的命令可能是：
请注意，相同的注释适用于此命令（即它不一致）