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

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

我不清楚

  • 如果Alloy实际上可以在这样的并发/并行上下文中使用？ （我希望有可能，因为我的命令依赖于区分 Module ）

  • 如何中断/停止"frozen"命令？我的程序可以检测这些冻结的命令，然后忽略它们，最后重新安排它们进行预定义（最大）次数的尝试 . 好消息是，我总是设法运行这些1536命令，通常是经过多次尝试 . 坏消息是，在所有这些Alloy命令完成后，我通常最终得到了我的PC（即最多有4个核心运行达到100％）（请注意，我的程序（Eclipse插件）不会在此时终止并继续执行） . 杀死JVM "unfreeze"我的电脑，可能表明"frozen"合金仍在运行......

对于代码，我写了一些丑陋的技巧，试图在我遇到冻结问题时恢复 . 但基本上，它看起来像（more details）：

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

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

至于AlloyWrapper，它会这样做（more details）：

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

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

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

alloy