合金 API 导致 java.lang.UnsatisfiedLinkError答案

【问题标题】：Alloy API resulting in java.lang.UnsatisfiedLinkError合金 API 导致 java.lang.UnsatisfiedLinkError
【发布时间】：2023-03-04 11:18:01
【问题描述】：

我目前正在使用 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?

【问题讨论】：

标签： java api alloy

【解决方案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

【讨论】：

完美；日食方法奏效了！谢谢。对我来说，我毫无例外地成功调用了该方法仍然很奇怪，但只要它有效，我就很高兴。谢谢。
可能是第一个模型 ("someFile.als") 是微不足道 (un) 可满足的，在这种情况下 Kodkod 不需要运行底层 SAT 求解器，因此错误不会'不会发生。

【解决方案2】：

我在我的eclipse插件项目中使用alloy4.2.jar作为库。

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;

当我使用默认求解器SAT4J时，这里提到的问题不会出现。但是出现了另一个例外。原因是我的 civi.als 文件需要整数模型，它位于 /models/util/ 文件夹下的alloy4.2.jar 中。但是当我运行应用程序时，它会尝试直接查找文件 util/Integer.als。这会导致异常。有没有可能解决这个问题？

此外，我还尝试将alloy4.2.jar 放入eclipse 插件项目中，并将我的应用程序作为eclipse 应用程序运行（将我的应用程序作为插件运行）。使用默认求解器，应用程序完全没有问题。但是当我切换到MiniSatProverJNI时，这里提到的问题就出现了（我已经将alloy4.2.jar设置为classpath）。

【讨论】：