alloy - 为 Alloy 提供 "pool"自定义字符串

Question

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

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

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

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

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

Answer 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”。