alloy - 如何在合金中使用 : x in {1, 2,4,5,7,8}？

我是合金初学者!

我想执行，例如:

run {all x: {2,3,4,5}, y: {1,2,3,4} | x > y and x + y <=10}

如何解决合金中的上述约束？

非常感谢!

最佳答案

您可以添加约束来强制规定，如果 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]

另请注意，当您请求区间 [-16,15] 内的所有整数组合满足给定条件时，此谓词是不一致的。

编辑

您实际上可以使用 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.

请注意，相同的注释适用于该命令(即不一致)

关于alloy - 如何在合金中使用 : x in {1, 2,4,5,7,8}？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/34428124/