Alloy : 限制一个字符串字段的值

Question

让下面这个简单的Alloy代码。

sig somme{
f : one Ax1,
g: one Ax2,
}
let Ax1= String
let Ax2= "Spain" + "Italy"

我想把字段f的值限制在 "意大利"，所以我写了一个谓词。

pred show{
 Ax1= "Italy"
}
run show

但这并不奏效（我没有实例）。

所以我的问题是，我如何才能做到不在公理中硬编码，而是在事实或谓词中有更多的灵活性（我可能想写第二个谓词来创建只使用西班牙的实例）？

先谢谢你。

Answer 1

Ax1是一个 宏观你用的是 let. 你是把它当做编程语言的全局变量来用的。Alloy没有变量，绝对不是全局变量。变量的作用是关系，定义在 领域 在 标志. 要使用一个 "新鲜 "变量，最好的方法是用它创建一个谓词。

pred show[ ax1 : String ] {
     ax1 = "Italy"
}
run show

也就是说，用String原子来做这件事是个很糟糕的主意 That said, it is a terrible idea to use String atoms for this. Alloy与整数的关系很复杂，但它与String的关系更糟糕。String的原子是你程序中所有的字符串，你不能轻易排除。长此以往，几乎都会失败。就用sigs吧。

enum Country { Italy, Spain, France, Netherlands }

pred show[ ax1 : Country ] {
     ax1 = Italy
}
run show

Answer 2

你的show谓词是不一致的，因为你把Ax1定义为所有Strings的集合。将所有字符串的集合限制为 "意大利"(Ax1 = "Italy")不符合 let Ax2= "Spain" + "Italy"

为什么不直接将Ax1和Ax2定义为字符串？

sig Somme{
  f : one String,
  g: one String,
}{
  f = "Italy"
}


pred show{
   //little hack to define a set of Strings usable by your model
   "Italy" +"Spain" in univ
}

run show

如果你想了解更多关于使用String的信息，可以查看这个问题的答案。关于无约束字符串的错误.

你也可以听从Peter的建议，定义国家的概念（用enum或老式的签名方式）。如果你有兴趣制作一个系统的抽象，一般都会这么做。