8

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

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

我不清楚

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

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

for(MyClass c : myClasses) {    
    AlloyWrapper worker = new AlloyWrapper(c, ...);
    tasks.add(worker);
    ecs.submit(worker);
}

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

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

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

Module world = CompUtil.parseEverything_fromFile(null, null, input.getAbsolutePath());
solution = TranslateAlloyToKodkod.execute_command(NOP, world.getAllReachableSigs(), world.getAllCommands().get(0), opt);

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

4

0 回答 0