无约束字符串的错误答案

【问题标题】：Bug on unconstrained Strings无约束字符串的错误
【发布时间】：2019-08-15 00:04:20
【问题描述】：

当关系包含不受约束的字符串时，Alloy 似乎存在错误。未找到以下实例：

sig foo{
    bar: String,
    yak: Int
}
pred show[]{one f:foo | f.yak=0}
run show for 1

如果我们将其更改为bar: Int，Alloy 会找到一个具有任意值的实例。

【问题讨论】：

标签： alloy

【解决方案1】：

谢天谢地，这个“众所周知”的错误有一个解决方法。为了使事情起作用，您需要通过在事实或谓词中使用它们来“隐式声明”一些字符串值。

例如，以下签名事实将允许 bar 在 {"a","b","c"} 中获取其值：

sig foo{
   bar: String,
   yak: Int
}{
   bar in "a"+"b"+"c"
}

您还可以定义一个在实例范围内使用的字符串池，如下所示：

fact stringPool{
   none!= "a"+"b"+"c"+"d"+"e"
}

见：

等等……

【讨论】：

【解决方案2】：

感谢您的错误报告。你可以提交issue 吗？

顺便说一句，Alloy 不太支持字符串。一般来说，除非你真的需要它们，否则最好避免使用任何具体类型，并使用抽象类型来做所有事情。大多数整数的使用也不是必需的。

【讨论】：