问题标签 [alloy]

我在合金网站上读到签名定义了一个集合。鉴于此定义，我试图理解以下合金代码：

如果签名实际上定义了一个集合，那么为什么我们在签名定义中有这么多参数，因为集合是一元关系？如果我错了，如何解释这个定义。

有人可以使用以下示例帮助我理解谓词：

我对上述代码有以下问题：

1) 如果上述谓词为真，会发生什么？

2）如果它是假的会发生什么？

3）谁能给我看一些合金代码，使用上面的代码并通过代码阐明谓词的含义。

我只是想了解我们如何使用上述谓词。

鉴于以下定义：

我很好奇在关系addr : Name -> some Addr中，第二列中名称的多重性是什么。此外，以下是否可能

我试图了解 j 是否可以在第二列中多次出现

我在一本书中看到了以下定义：

在哪里

在玩过合金分析仪后，我意识到这和

我很好奇将 Book 指定为参数有什么好处，而不是使用量词的第二种方法？

我知道合金中谓词的使用，但我对下面的描述有点惊讶：

有人可以向我解释上述内容。

我想知道为什么这个模型不一致？我们可以在 shaves 中有以下元组。

shaves = {(man,man)} sig Man {shaves: set Man} one sig Barber extends Man {}

Barber.shaves 将产生 0 个元组。在这种情况下，事实应该是有效的。那么为什么允许告诉我我的模型不一致？

非常感谢对此的一些建议。

假设我有一个简单的模型如下： sig P{r:some P} sig Q{} run {} for 2 P, 2 Q

这里有谁知道合金如何生成对称破坏谓词以减少该模型的实例数量？

我正在阅读有关合金中高阶量化的内容，并看到以下内容：lone p: some X| F
现在，如果关键字“some”修改 p 或​​ X，我感到困惑。这是否意味着 X 应该是非空的，或者是否意味着 p 的基数应该 >=1。

在下面

下面是什么意思？它与签名定义有什么关系？这是 sig 的关系吗？

我有一个非常令人费解的问题。我似乎找不到这个谓词的实例。下面是代码。

为什么 getin 没有实例？我已经跟踪了代码，基本的跟踪应该是这样的：init -> 朝向 -> unlockopen -> getin。

这些前面的谓词中的每一个都应该满足后续谓词中的约束。那么，为什么我可以获得除 getin 之外的其余谓词的实例？

非常感谢对此的一些指导。