我目前使用的合金分析仪API构建的程序，并获得一些特殊的行为。 特别是，如果我打开一个文件，分析它（使用CompUtil.parseEverything），然后作出一个新的命令，并呼吁TranslateAlloyToKodkod.execute_command在解析文件，并使用与MINISAT核心UNSAT新创建的命令，它运行良好。 然而，在后来的执行，我的程序分析第二个输入文件（也使用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?
我试图重现此问题，但我不能。 如果我不MINISAT二进制文件添加到PATH环境变量，我得到你提到的我第一次调用异常execute_command 。 配置LD_LIBRARY_PATH后，异常不会发生。
要配置LD_LIBRARY_PATH：
（1）如果使用Eclipse，您可以在源文件夹中的一个单击鼠标右键，选择构建路径 - >配置构建路径，那么“源”选项卡上，确保“本机库位置”点到一个文件夹中MINISAT二进制文件驻留。
（2）如果从shell中运行，只需添加的文件夹路径与MINISAT二进制文件LD_LIBRARY_PATH，例如，像export LD_LIBARRY_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
我用alloy4.2.jar在我的Eclipse插件项目库。
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文件需要整数模型，位于alloy4.2.jar文件夹/模型/ UTIL /下。 但是，当我运行应用程序，它会尝试直接找到UTIL / Integer.als文件。 这导致异常。 是否有可能解决这一问题？
此外，我还试图把在Eclipse插件项目alloy4.2.jar和运行我的应用程序作为Eclipse应用程序（运行我的应用程序作为一个插件）。 使用默认的求解器，应用程序有没有问题。 但是，当我切换到MiniSatProverJNI，这里提到的问题出来（我已经设置了alloy4.2.jar的类路径）。
