合金 API 导致 java.lang.UnsatisfiedLinkError [英] Alloy API resulting in java.lang.UnsatisfiedLinkError
问题描述
我目前正在使用 Alloy Analyzer API 来构建一个程序,并获得了一些特殊的行为.具体来说,如果我打开一个文件并解析它(使用 CompUtil.parseEverything),然后创建一个新命令并在解析的文件上调用 TranslateAlloyToKodkod.execute_command 和使用带有 UNSAT 核心的 MiniSat 新创建的命令,它运行良好.但是,稍后在执行时,我的程序解析第二个输入文件(也使用 CompUtil.parseEverything),获取另一个世界,创建一个新命令,然后我再次尝试调用 TranslateAlloyToKodkod.execute_command,它抛出以下错误:
I'm currently using the Alloy Analyzer API to build a program, and getting some peculiar behavior. Specifically, if I open a file and parse it (using CompUtil.parseEverything), then make a new Command and call TranslateAlloyToKodkod.execute_command on the parsed file and newly created command using MiniSat with UNSAT core, it runs fine. However, later in execution, my program parses a second input file (also using CompUtil.parseEverything), gets another world, makes a new command, and then I try to call TranslateAlloyToKodkod.execute_command again, it throws the following error:
错误:类 edu.mit.csail.sdg.alloy4.ErrorFatal:找不到所需的 JNI 库:java.lang.UnsatisfiedLinkError:java.library.path 中没有 minisatproverx5edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)
有谁知道为什么这是第二次抛出而不是第一次抛出?
Does anyone have any idea why this is thrown the second time, but not the first?
总而言之,我有类似的东西:
To summarize, I have something similar to the following:
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 二进制文件添加到 LD_LIBRARY_PATH 环境变量,我会收到您在第一次调用 execute_command
时提到的异常.配置 LD_LIBRARY_PATH 后,异常不会发生.
I tried to reproduce this behavior, but I couldn't. If I don't add MiniSat binaries to the LD_LIBRARY_PATH environment variable, I get the exception you mentioned the very first time I invoke execute_command
. After configuring LD_LIBRARY_PATH, the exception doesn't happen.
配置 LD_LIBRARY_PATH:
To configure LD_LIBRARY_PATH:
(1) 如果使用 Eclipse,您可以右键单击源文件夹之一,选择 Build Path -> Configure Build Path,然后在Source"选项卡上确保Native library location"指向一个文件夹MiniSat 二进制文件所在的位置.
(1) if using Eclipse, you can right-click on one of your source folders, choose Build Path -> Configure Build Path, then on the "Source" tab make sure that "Native library location" points to a folder in which MiniSat binaries reside.
(2) 如果从 shell 运行,只需将包含 MiniSat 二进制文件的文件夹的路径添加到 LD_LIBRARY_PATH,例如,类似于 export LD_LIBARRY_PATH=alloy/extra/x86-linux:$LD_LIBRARY_PATH
.
(2) if running from the shell, just add the path to a folder with MiniSat binaries to LD_LIBRARY_PATH, e.g., something like export LD_LIBARRY_PATH=alloy/extra/x86-linux:$LD_LIBRARY_PATH
.
这是我正在运行的确切代码,一切正常
Here is the exact code that I was running, and everything worked
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"是
with "someFile.als" being
sig A {}
run { some A } for 4
和someOtherFile.als"
and "someOtherFile.als"
sig A {}
run { no A } for 4
这篇关于合金 API 导致 java.lang.UnsatisfiedLinkError的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!