小编bmo*_*rin的帖子

我生成了很多合金规范(*.als文件).对于我试图解决的中等问题,我生成了1536*.als文件.为了节省时间运行的所有这些文件,我使用的Java并发API(特别是ExecutorCompletionService与Future)来运行ñ合金并联,其中命令Ñ是可用的逻辑核心的机器上的号码(在我的情况4中,2个CPU使用HyperThreading).

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

我不清楚

• 如果Alloy实际上可以在这样的并发/并行上下文中使用？(我希望有可能,因为我的命令依赖于区别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);

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