合金API導致java.lang.UnsatisfiedLinkError中

我目前使用的合金分析儀API構建的程序，並獲得一些特殊的行爲。特別是，如果我打開一個文件，分析它（使用CompUtil.parseEverything），然後作出一個新的命令，並呼籲TranslateAlloyToKodkod.execute_command在解析文件，並使用與MINISAT核心UNSAT新創建的命令，它運行良好。但是，後來在執行時，我的程序會解析第二個輸入文件（也使用CompUtil.parseEverything），獲取另一個世界，創建一個新命令，然後嘗試再次調用TranslateAlloyToKodkod.execute_command，它會引發以下錯誤：合金API導致java.lang.UnsatisfiedLinkError中

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?

來源

2012-08-10 Jan Gorzny

我試圖重現此問題，但我不能。如果我沒有將MiniSat二進制文件添加到LD_LIBRARY_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

來源

2012-08-11 01:37:30

完美;日食方法奏效！謝謝。對我來說，我仍然有一個奇怪的例子，那就是我沒有一個例外，但是隻要它有效，我就很高興。謝謝。 – 2012-08-13 06:59:04

可能是第一個模型（「someFile。als「）是平凡（不可）滿足的，在這種情況下，Kodkod不需要運行底層的SAT求解器，所以不會發生錯誤。 – 2012-08-13 19:11:30

我在我的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文件需要Integer模型，它位於文件夾/ models/util /下的alloy4.2.jar中。但是當我運行該應用程序時，它會直接找到文件util/Integer.als。這會導致異常。有沒有可能解決這個問題？

此外，我還試圖把在Eclipse插件項目alloy4.2.jar和運行我的應用程序作爲Eclipse應用程序（運行我的應用程序作爲一個插件）。使用默認求解器，應用程序完全沒有問題。但是當我切換到MiniSatProverJNI時，這裏提到的問題出來了（我已經將alloy4.2.jar設置爲類路徑）。

來源

2014-11-06 17:54:52 wxlfrank

合金API導致java.lang.UnsatisfiedLinkError中

回答

相關問題