问题标签 [alloy]

调用

方法返回一个A4Soluiton对象，我们可以通过next()方法对其进行迭代，直到它到达一个 unsatisfiable( )的反例。通过这种方式，我们可以计算求解器的反例总数。

我的问题是，是否可以直接从A4Solution对象中知道反例的总数而无需遍历它。

非常感谢您的回复。

我有以下合金模型，但我不确定如何将其转换为合金 Java API。

我知道我们可以使用A.addField("B", Expr)添加属性，但是我应该在Expr参数中输入什么来使它代表Ints？

谢谢

我尝试了 Alloy4 的以下片段，发现自己对 util/Natural 模块的行为感到困惑。评论更详细地解释了意外情况。我希望有人能解释为什么会发生这种情况。

我建立了一个合金模型，它成功地列举了我想要的所有解决方案。每个解决方案都是一个 A4Solution 对象。

每个实例的输出应该是一个简单的 Java POJO 对象，如下例所示：

我的 Alloy 模型基本上生成了上述 4 个字段的所有可能组合。

我的问题是 A4Solution 对象很复杂，如何解析对象并将生成的字段存储到上面的 POJO 中？

谢谢

我发现自己试图总结一组自然值。运行简单模型时，我对以下行为感到困惑。

（假设以下代码在 util/natural 的副本中，所以导入了 ord）

然后，在导入我的 util/natural 副本的模块中：

为什么更改 Natural 的范围会以这种方式影响结果？

我正在构建一个简单的合金来生成简单的 Java Pojo 对象，并且该 pojo 的某些字段是布尔值。我现在使用下面的机制来实现这个功能

这会起作用，但是每次我引入一个新的布尔字段时，我都必须修改布尔事实以确保该值是“真”或“假”。有没有最佳实践来做到这一点？就像我们 Alloy 对整数所做的那样？

我有一个合金模型，它需要有一些规则，比如

所以我想设置一个规则，这样每当实例选择美国时，它也会选择美元和纽约。如果它选择 USD，那么它将选择 US 和 NewYork，这意味着国家、地点和货币将被组合在一起。我试图使用以下事实来做到这一点，但它不起作用。事实有什么缺陷，有什么办法吗？

我在 Alloy 上做了一些工作，所以我对它有一些了解。然而，很多速记并没有真正涵盖任何地方。我想知道的是在下面的例子中：

我想确保最终的 Proc 始终是 Begin（目前它也可以是 Action）。

有很多方法可以手写。我在下面包含了一个，当包含它时，可以确保最终的 Proc（即不在域中的）始终是 Begin。

但是，我喜欢使用 (Proc - Remove) 的简写，例如因为它使事情更容易阅读，这意味着 Remove 不能从另一个 Proc 链接到。我希望我已经解释得很好。我认为会有一个非常明显的答案，但我想不出它是什么。请问有什么想法吗？

如何获取合金中字符串的长度？

如果我想说密码必须至少有 8 个字符，我该如何表示该字符串的长度？

我的密码签名是：

sig 密码{ 密码：一个字符串 }

我正在尝试在 Alloy 中构造一个递归函数。根据丹尼尔杰克逊书中显示的语法，这是可能的。我的功能是：

但是求解器声称该调用auxiliaryToAvoidCyclicRecursion[idTarget, mRet]是这样说的：