问题标签 [alloy]

我正在编写一个简单的合金代码，但我不明白我怎么能说最多一个 A 与 pD 相关联（所以最多是一或零）。所以我写了下面的代码，但断言没有给出没有 D 的 P1 实例的反例。你能帮我吗？我如何定义我的事实，即在最多有一个 pD 实例的情况下，我可以看到一个反例p 与它的 D 没有任何联系。

去年我使用了合金，我可以设置 Int 位宽写入的范围，例如“5 Int”，正如以下答案所建议的那样： 在合金中运行命令范围

但是，我今年再次下载了Alloy 4.1.1，如果我写了

我现在得到

有什么改变？我应该如何设置位宽？

我正在为 Java 的一个子集做一个合金元模型。

下面我们有一些签名：

在 Java 语言中，如果该方法不是私有方法，我们只能调用类内部的方法（通过该类的实例化）。我试图通过以下签名在我的合金模型中表示此限制：

因此，alloy 中的 ConstructorMethodInvocation 签名试图表示 java 中的构造，如 new A().x()。另外，方法 x() 只有在它不是类 A 的私有方法时才能被调用。所以，为了避免调用类 id_Class 的私有方法，我设置了以下限制（在 ConstructorMethodInvocation 签名中）：

（this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)

然而，尽管有这个限制，求解器仍坚持生成实例（用于 ConstructorMethodInvocation），其中 cmethodInvoked 是 id_Class 的私有方法。同样的情况也发生在 ConstructorFieldInvocation 上。

有人看到我做错了吗？

如何在合金中建模模算子？

我想尝试合金来证明任何 4 的倍数都可以被 2 整除....

这是我的代码..

这不编译

我可以在显示模型时隐藏已使用的签名（当我执行“pred show{} run show for 8”行时）？对于已使用的签名，我的意思是没有箭头连接的签名。

例如：

抽象信号 TypeMessage{}

一个 sig RichiestaLogin, RichiestaRegistrazione, RichiestaShell

不深入我的代码的细节，有一些我使用消息类型的实例和其他使用它们的实例，因此一些实例保持未连接。我不会在我的模型图中显示这些实例未连接。

如果我有以下格式的合金模型

如果我想制定一个规则，让每个玩家可以有 1 到 3 个位置。有没有办法创建这样的预测或事实来做到这一点？

谢谢，

我是合金新用户，我试图在谓词中声明

There is a y in Y for each x in X

但是当我这样写时：

all x : X | all y : Y | one y

我只有一个 y 代表整个 X

我期望的是，如果有 3 x，就会有 3 y。我不想使用基数比较，因为我尝试对态射进行建模。

有人能帮我吗？

提前致谢。

我有一个合金模型，它有 2 个具有相同名称的关系的签名。

当我尝试访问这些关系 throw join 时，求解器会抛出我：

有没有办法明确指定我想访问belongTo组件的关系而不是端口一，当我这样做时：

和 m 是模型？

谢谢。

我有以下描述一群人的合金模型。简化问题。这是一个示例代码片段。

所以现在我们在一个组中有两个人。接下来我想对组中的人添加一些限制。例如，我希望一个小组中的两个人始终有一个团队负责人和一个团队成员。我使用以下事实来做到这一点：

现在我遇到了一个阻碍我前进的问题。我正在寻找的理想模型是，如果一个小组的国家是“美国”，那么团队负责人的职位是“US_TL”，团队成员的职位是“US_TM”。如果国家是“UK”，那么队长的位置是“UK_TL”，团队成员的位置是“UK_TM”，以此类推。

我试图添加类似的东西：

但是预测显然有问题，模型无法为我生成正确的解决方案。您能帮我找出模型中的问题吗？

我一直在研究 ASP，并且想知道这两种方法之间的关系，因为它们都在后端使用 SATsolvers。尽管文献中很少或没有重叠。我很欣赏两者的简单比较。

（CS StackExchange 上也有人问过这个问题

https://cs.stackexchange.com/questions/14633/why-is-alloy-not-an-answer-set-programming-system

)