合金API导致java.lang.UnsatisfiedLinkError中 [英] Alloy API resulting in java.lang.UnsatisfiedLinkError

问题描述

我目前使用的合金分析仪API构建的程序，并获得一些特殊的行为。特别是，如果我打开一个文件，分析它（使用CompUtil.parseEverything），然后作出一个新的命令，并呼吁TranslateAlloyToKodkod.execute_command所解析的文件，并使用与MINISAT核心UNSAT新创建的命令，它运行良好。不过，后来在执行中，我的程序分析的第二个输入文件（也使用CompUtil.parseEverything），得到另一个世界，它让一个新的命令，然后我尝试再次调用TranslateAlloyToKodkod.execute_command，它引发以下错误：

错误：类edu.mit.csail.sdg.alloy4.ErrorFatal：所需要的JNI库不能找到：
java.lang.UnsatisfiedLinkError中：在没有的java.library.path minisatproverx5
edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)

没有人有任何想法，为什么这被抛出第二次，但不是第一？

要总结，我有类似下面的内容：

 模块someWorld = CompUtil.parseEverything_fromFile（REP，NULL，someFile.als）;
//对于以下，签名是someWorld.getAllReachableSigs一个签名（）;
Command命令= sig.not（）;
A4Options选项=新A4Options（）;
options.solver = A4Options.SatSolver.MiniSatProverJNI;
A4Solution ANS =
    TranslateAlloyToKodkod.execute_command（REP，someWorld，命令选项）;
//没有抛出错误
模块someOtherWorld = CompUtil.parseEverything_fromFile（REP，NULL，someOtherFile.als）;
//对于以下，签名是someOtherWorld.getAllReachableSigs一个签名（）;
命令commandTwo = sig.not（）;
A4Solution ansTwo =
    TranslateAlloyToKodkod.execute_command（REP，someOtherWorld，commandTwo，期权）;
//时抛出上述错误。为什么？
 




解决方案

我试图重现此问题，但我不能。如果我没有MINISAT二进制文件添加到LD_LIBRARY_PATH环境变量中，我得到的异常你提到的我第一次调用 execute_command 。配置LD_LIBRARY_PATH后，异常不会发生。

要配置LD_LIBRARY_PATH：

（1）如果使用Eclipse，您可以在您的源文件夹上右键单击，选择构建路径 - >配置构建路径，那么源选项卡上，确保本机库的位置指向的文件夹其中MINISAT二进制文件所在的位置。

（2）如果从shell中运行，只是路径添加到一个文件夹MINISAT二进制文件LD_LIBRARY_PATH，例如，像出口LD_LIBARRY_PATH =合金/额外/ x86的Linux上：$ LD_LIBRARY_PATH 。

下面是我正在运行的确切code，和一切工作

 公共静态无效的主要（字串[] args）抛出异常{
    A4Reporter代表=新A4Reporter（）;    A4Options选项=新A4Options（）;
    options.solver = A4Options.SatSolver.MiniSatProverJNI;    模块someWorld = CompUtil.parseEverything_fromFile（REP，NULL，someFile.als）;
    Command命令= someWorld.getAllCommands（）得到（0）;
    A4Solution ANS = TranslateAlloyToKodkod.execute_command（REP，someWorld.getAllReachableSigs（）命令，选项）;
    的System.out.println（ANS）;    模块someOtherWorld = CompUtil.parseEverything_fromFile（REP，NULL，someOtherFile.als）;
    命令commandTwo = someOtherWorld.getAllCommands（）得到（0）;
    A4Solution ansTwo = TranslateAlloyToKodkod.execute_command（REP，someOtherWorld.getAllReachableSigs（），commandTwo，期权）;
    的System.out.println（ansTwo）;
}
 

与someFile.als之中。

  SIG A {}
运行{一些A} 4
 

和someOtherFile.als

  SIG A {}
运行{没有A} 4
 

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:

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)

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?

解决方案

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.

To configure LD_LIBRARY_PATH:

(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) 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);
}

with "someFile.als" being

sig A {}
run { some A } for 4

and "someOtherFile.als"

sig A {}
run { no A } for 4

这篇关于合金API导致java.lang.UnsatisfiedLinkError中的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！