为 Alloy 提供自定义字符串的“池”答案

【问题标题】：Provide Alloy with a "pool" of custom Strings为 Alloy 提供自定义字符串的“池”
【发布时间】：2015-02-08 11:07:12
【问题描述】：

我对使用 Alloy 的 String 类型很感兴趣（特别是因为它允许使用特殊字符）。我注意到为了将给定的字符串添加到实例中，将其包含在表达式中就足够了。例如

fact stringInsert{
   none!="a"+"b"+"c"
}

将导致在任何生成的实例中创建原子“a”、“b”和“c”。

现在我的问题是，有没有办法声明一个字符串池，定义所有可能出现在可满足实例中的字符串原子，但其数量尊重给定范围并且可以进一步限制？

例如，如果我们将上述事实视为声明一个字符串原子池 {"a","b","c"}，我希望从使用这个池的模型执行中获得实例2 的全局范围仅包含这三个字符串“a”、“b”和“c”中的两个。

【问题讨论】：

我猜这个功能不支持，但我问一下以防万一。 :-)
所以池中的各个具体字符串被视为使用 lone sig something-or-other extends String 声明的？（起初我认为“任何个人都必须声明为one，但lone 将允许您想要的范围限制。）
问题是你不能扩展字符串签名。此外，如果您想要字符串 ":" ，您将如何将 : 放入签名声明中？
是的，重点。因此，“好像”这个短语就是这样声明的......
我误读了你的评论，我的错，是的，完全是“好像”:)

标签： alloy

【解决方案1】：

您只能为String 声明一个确切范围，例如，

run {} for 3 but exactly 5 String

目前不可能只给出字符串的上限，例如for 5 String，并要求 Alloy 找到最多 5 个字符串的解决方案（关于其他约束）。因此，如果您尝试在上面的示例中将 String 的范围设置为 2，您仍将获得模型中声明的所有 3 个字符串文字（“a”、“b”、“c”），这与字符串一致文字是扩展抽象 String sig 的“one sigs”；另一方面，如果将范围设置为 5，Alloy 将生成 2 个额外的字符串原子，“String$0”和“String$1”。

【讨论】：

这就是我“害怕”的。