1

我目前正在使用 Alloy Analyzer API 来构建程序，并获得了一些特殊的行为。具体来说，如果我打开一个文件并解析它（使用 CompUtil.parseEverything），然后创建一个新命令并在解析的文件上调用 TranslateAlloyToKodkod.execute_command，并使用带有 UNSAT 核心的 MiniSat 新创建的命令，它运行良好。但是，稍后在执行中，我的程序解析第二个输入文件（也使用 CompUtil.parseEverything），获取另一个世界，发出一个新命令，然后我尝试再次调用 TranslateAlloyToKodkod.execute_command，它会引发以下错误：

ERROR: class edu.mit.csail.sdg.alloy4.ErrorFatal: The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)

有谁知道为什么这是第二次抛出，但不是第一次？

总而言之，我有类似以下内容：

Module someWorld = CompUtil.parseEverything_fromFile(rep, null, "someFile.als");
//For the following, "sig" is a sig in someWorld.getAllReachableSigs();
Command command = sig.not();
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.MiniSatProverJNI;
A4Solution ans = 
    TranslateAlloyToKodkod.execute_command(rep, someWorld, command, options);
//No thrown error
Module someOtherWorld = CompUtil.parseEverything_fromFile(rep, null, "someOtherFile.als");
//For the following, "sig" is a sig in someOtherWorld.getAllReachableSigs();
Command commandTwo = sig.not();
A4Solution ansTwo = 
    TranslateAlloyToKodkod.execute_command(rep, someOtherWorld, commandTwo, options);
//Thrown error above. Why?
4

2 回答 2

1

我试图重现这种行为，但我不能。如果我不将 MiniSat 二进制文件添加到 LD_LIBRARY_PATH 环境变量中，我会在我第一次调用execute_command. 配置 LD_LIBRARY_PATH 后，异常不会发生。

要配置 LD_LIBRARY_PATH：

(1) 如果使用 Eclipse，您可以右键单击其中一个源文件夹，选择 Build Path -> Configure Build Path，然后在“Source”选项卡上确保“Native library location”指向 MiniSat 所在的文件夹二进制文件驻留。

(2) 如果从 shell 运行，只需将带有 MiniSat 二进制文件的文件夹的路径添加到 LD_LIBRARY_PATH，例如export LD_LIBRARY_PATH=alloy/extra/x86-linux:$LD_LIBRARY_PATH.

这是我正在运行的确切代码，一切正常

public static void main(String[] args) throws Exception {
    A4Reporter rep = new A4Reporter();

    A4Options options = new A4Options();
    options.solver = A4Options.SatSolver.MiniSatProverJNI;
    
    Module someWorld = CompUtil.parseEverything_fromFile(rep, null, "someFile.als");
    Command command = someWorld.getAllCommands().get(0);
    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, someWorld.getAllReachableSigs(), command, options);
    System.out.println(ans);
    
    Module someOtherWorld = CompUtil.parseEverything_fromFile(rep, null, "someOtherFile.als");
    Command commandTwo = someOtherWorld.getAllCommands().get(0);
    A4Solution ansTwo = TranslateAlloyToKodkod.execute_command(rep, someOtherWorld.getAllReachableSigs(), commandTwo, options);
    System.out.println(ansTwo);
}

“someFile.als”是

sig A {}
run { some A } for 4

和“someOtherFile.als”

sig A {}
run { no A } for 4
于 2012-08-11T01:37:30.133 回答
0

I use alloy4.2.jar as a library in my eclipse plugin project.

A4Reporter rep = new A4Reporter();
Module world = CompUtil.parseEverything_fromFile(rep, null, "civi.als");
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.SAT4J;
options.skolemDepth = 1;

When I use SAT4J, the default solver, the problem mentioned here will not show up. But another exception comes out. The reason is that my civi.als file need Integer model, which located in alloy4.2.jar under the folder /models/util/. But when I run the application, it tries to find the file util/Integer.als directly. That causes the exception. Is it possible to fix that problem?

Besides, I also tried to put the alloy4.2.jar in eclipse plugin project and run my application as an eclipse application (running my application as a plugin). With the default solver, the application has no problem at all. But when I switch to MiniSatProverJNI, the problem mentioned here comes out (I have set the alloy4.2.jar as classpath).

于 2014-11-06T17:54:52.107 回答