我正在生成相当多的合金规格（*.als 文件）。对于我试图解决的中等规模问题，我生成了 1536 个 *.als 文件。为了节省运行所有这些文件的时间，我使用了 Java 并发 API（特别是ExecutorCompletionService with Future） 跑步n并行合金命令，其中n是机器上可用逻辑核心的数量（在我的例子中为 4，对于具有超线程的 2 个 CPU）。
在这种情况下，有时会发生命令冻结并且在“合理”延迟内不返回任何结果的情况，我将其固定为 5 秒，因为每个 *.als 相当简单。
我不清楚
- Alloy 是否真的可以在这样的并发/并行上下文中使用？ （我希望这是可能的，因为我的命令依赖于不同的
Module)
- 如何中断/停止“冻结”命令？我的程序可以检测这些冻结的命令，然后忽略它们，最后重新安排它们进行预定义（最大）的尝试次数。好消息是，我总是设法运行这 1536 个命令，通常是在多次尝试之后。坏消息是，在所有这些 Alloy 命令完成后，我通常会“冻结”我的 PC（即最多有 4 个内核运行到 100%）（请注意，我的程序（Eclipse 插件）此时不会终止）并继续执行）。杀死 JVM“解冻”我的电脑，可能表明“冻结”的 Alloy 仍在运行......
对于代码，我写了一些丑陋的技巧来尝试在遇到冻结问题时进行恢复。但基本上，它看起来像（更多细节 https://github.com/SINTEF-9012/diva/blob/master/diva.model.simulation/src/diva/helpers/DivaHelper.java):
for(MyClass c : myClasses) {
AlloyWrapper worker = new AlloyWrapper(c, ...);
tasks.add(worker);
ecs.submit(worker);
}
我确定了执行器 ecs 的大小，以便它应该使用机器上可用的所有核心/物理线程。
至于 AlloyWrapper，它是这样做的（更多细节 https://github.com/SINTEF-9012/diva/blob/master/diva.model.simulation/src/diva/alloy/AlloyWrapper.java):
Allow 包装器基本上为 Alloy 生成输入（基于 MyClass 中包含的信息）并调用
Module world = CompUtil.parseEverything_fromFile(null, null, input.getAbsolutePath());
solution = TranslateAlloyToKodkod.execute_command(NOP, world.getAllReachableSigs(), world.getAllCommands().get(0), opt);
如果您需要更多信息，请告诉我。
