问题标签 [alloy]

使用 Alloy API，可以从合金文件中获取 CompModule，其中包含您需要的所有内容，以便使用给定的合金模块。

这很容易使用： CompUtil.parseEverything_fromFile(...)

我现在的问题如下。有没有办法从 CompModule 到合金语言？或者从符号列表和事实到合金模型。（我想我可以蛮力进行，但我想知道是否存在实用程序。）

谢谢你的支持 ！

干杯

我们如何将 Event-Condition-Action 规则转换为 Alloy ( http://alloy.mit.edu/alloy/ )

我使用合金创建了一个简单版本的链表。现在我想创建一个可以在其中执行插入和删除的链表。我刚开始用合金编码。现在我在使用函数和实用程序等复杂操作时遇到了麻烦。如果我能得到一些关于如何使用实用程序和函数以及如何在合金中实际执行插入和删除的示例。我会很感激你的帮助。

我想从链接列表中删除一个元素并将其推送到堆栈上。我试图编写这段代码。我正在编写将元素推入堆栈的代码，但它给出了错误。该代码在注释中。

//双向链表

//堆

我已经尝试过这段代码（在评论中）将元素插入堆栈。但这没有给出任何实例发现错误。

我是合金新手。我需要合金串联和并联电路的帮助。我为串联电路建模了一个图，但是当我省略串联的自循环时，它也不起作用，它也只显示了该系列的一个实例。我必须显示开关何时打开，串联灯泡打开......所以它们是状态的签名，并且 On 和 Off 扩展状态..

我的代码是：

I am trying to create a list of coins which denote a value.suppose 9 rs will contain a sequence 5->2->2 . 8rs will have 5rs->2rs->1rs. 7rs will have 5->2 . The coins can be of the type 10Rs, 5rs, 2rs,1rs. Here in this code tenr implies list of coins of value ten and tenrs implies coin of ten rs. How can I create such a list? I've been trying but all in vain . Also when I execute and click on show it shows multiple coins assigned to a single coin node. Any help will be appreciated. Actually I am trying to use it in a vending machine. I checked your code and I am currently trying to implement it . I am also providing my code for vending machine.

Vending machine

我创建了一台自动售货机，它工作正常。交易完成后，我想从商品数量中减去 1。我在代码中提供了注释以供理解。忽略pred Chocolate中的一些评论。不知何故，我试图减去，但它不会。我不知道似乎是什么问题。任何帮助表示赞赏。

我经历了一个问题陈述，例如：外科医生必须对三名患者进行手术，但只有两副手套。不得有交叉污染：外科医生不得接触任何患者的血液，任何患者不得接触其他患者的血液。外科医生需要两只手才能工作。她是怎么做到的？在 Alloy 中表达这个问题，并使用分析器找到解决方案。

我已经声明了几个签名，但我坚持声明需要事实和谓词。谁能帮我吗？我的代码是：

\thanx 提前

我正在生成很多合金规格（*.als 文件）。对于我试图解决的中等规模问题，我生成了 1536 个 *.als 文件。为了节省运行所有这些文件的时间，我使用 Java 并发 API（特别是ExecutorCompletionServicewith Future）并行运行n 个Alloy 命令，其中n是机器上可用逻辑内核的数量（在我的例子中是 4 个，用于 2 个 CPU使用超线程）。

在这种情况下，有时会发生命令冻结并且在“合理”延迟内不返回任何结果，我将其固定为 5 秒，因为每个 *.als 都相当简单。

我不清楚

• 如果合金实际上可以在这样的并发/并行上下文中使用？（我希望这是可能的，因为我的命令依赖于 distincts Module）
• 如何中断/停止“冻结”命令？我的程序可以检测到这些冻结的命令，然后忽略它们，最后重新安排它们以进行预定义的（最大）尝试次数。好消息是，我总是设法运行那些 1536 命令，通常是在几次尝试之后。坏消息是，在所有这些 Alloy 命令完成后，我通常会“冻结”我的 PC（即最多 4 个内核运行高达 100%）（请注意，我的程序（一个 Eclipse 插件）此时不会终止并继续执行）。杀死 JVM “解冻”我的电脑，可能表明“冻结”的合金仍在运行......

对于代码，我写了一些丑陋的技巧来尝试在遇到冻结问题时恢复。但基本上，它看起来像（更多细节）：

我确定了执行程序 ecs 的尺寸，以便它应该使用机器上可用的所有内核/物理线程。

至于 AlloyWrapper，它会这样做（更多细节）：

Allow 包装器基本上为 Alloy 生成输入（基于 MyClass 中包含的信息）并调用

如果您需要更多信息，请告诉我。

我很难理解 Alloy 4 中谓词和函数之间的区别。我已经阅读了软件抽象中的第 4.5.2 节，但我仍然不清楚。有人可以帮我理解吗？