问题标签 [alloy]

假设我执行以下操作：

ordering/first 有什么价值？它是未定义的吗？您是否需要使用模块别名来消除歧义？

我有这个合金模型

这不会为我生成任何实例。我在 x' 状态下添加关系 c1->c2 并再次删除它，出于某种原因它不允许我这样做。

不久前，我获得了软件抽象的第二版，当我需要重新记忆如何拼写elems函数的名称时，我想“哦，很好，我可以查看新版本，而不是试图阅读我难以辨认的手写第一版结尾文件中的注释。”

但我在索引中找不到“seq”或“elems”或任何其他辅助函数的名称，也没有seq在附录 B 的语言参考中看到任何提及该关键字的内容。

以下一项或多项似乎很可能是这种情况；哪个？

• 我错过了一些东西。（什么哪里？）
• 附录 B 中没有涵盖该seq关键字，因为严格来说，它不像set其他一元运算符那样是关键字。（请说明！）
• 在第二版出版后，Alloy 4 中增加了对序列的支持，因此需要通过参考快速指南中关于 Alloy 4 中新特性的讨论和网站上的Alloy 4 语法来扩充本书。（啊，好的。页面很慢，位很快。）
• 其他 ...

我想，为了在这里提出一个普遍有用的问题，我要问的是：Alloy Analyzer 4.2（或任何 4.*）实现的语言与软件抽象第二版中定义的语言之间到底有什么关系？

我的问题很简单，但我找不到解决方案。

我正在尝试使用 : 形式的命令打开一个模块open ../folder/module，但这会导致语法错误。如何纠正？

ps：这两个模块必须在一个单独的文件夹中，并且这些文件夹必须是“兄弟文件夹”（一个不能包含在另一个文件夹中）

谢谢和干杯！

我想使用 Alloy Analyzer 从给定范围内的谓词中枚举所有解决方案。Alloy 是否支持此功能？如果可以，如何从命令行调用它？

谢谢

假设我的模块中有一个与 sig B 相关的 sig A。

现在想象一下，我们有几个实例：

和

我想表示 B$1 和 B$2 是等价的（在某些条件下），因此只会生成这个实例A$1 -> B , A$2 -> B.

一种解决方案可能是在声明 sig B 时使用关键字“one”，但在我的情况下它不起作用，因为 B 有多个字段，使得 B 原子不一定等效。简而言之，只有当它们的字段具有相同的值时，2 个原子才是等价的。

理想情况下，我想删除 B. 的编号，但仍然可以有几个原子 B 。

我有一个合金模型，其中包含以下内容：

如何使两个签名相等？

考虑以下合金模型：

我理解为什么，当 I 时run show for 7，该模型的所有实例都有 7 个签名 C 原子。（嗯，这不太正确。我知道有序签名将始终具有范围允许的尽可能多的原子，因为 util/ordering 告诉我是这样。但这与为什么不完全相同。）

但是为什么这个模型的实例没有任何签名 B 的原子？这是为 util/ordering 执行的特殊处理的副作用吗？（有意？无意？） util/ordering 是否仅适用于顶级签名？

或者还有其他我想念的事情吗？

在这个模型中，这是抽象的，我真的很想给 B 和 C 的联合起一个像 A 这样的名字，我真的希望 C 是有序的，我真的希望 B 是无序的并且非空。目前，我似乎能够实现其中任何两个目标；有没有办法同时管理这三个？

[附录：我注意到指定run show for 3 but 3 B, 3 C确实实现了我的三个目标。相比之下，run show for 2 but 3 B根本不产生任何实例。也许我需要更好地理解范围规范的语义。]

使用网站上当前可用的最新合金分析器（4.2 构建日期：2012-09-25）我意识到，当我/**/像这样将代码放在两个之间时，分析器似乎忽略了代码（尽管编辑器/**/ <some code> /**/似乎<some code>正确解析代码）。

例如，在以下代码片段中，fact分析器会忽略 的声明：

只要我在 之间放置一个空格/**/，即 ，/* */代码就会按预期运行。

// .. 同样的方式项目 4 到 10

是否可以选择 n 个（使得 n = 1 到 10）个项目，以使所选项目的价格总和最小？

对于 n=3 个项目，结果应该是 item1、item2 和 item3。

如果可能的话如何用合金写这个东西？

非常感谢您的友好回复。