1

私は現在、Alloy Analyzer API を使用してプログラムを作成していますが、奇妙な動作が発生しています。具体的には、ファイルを開いて解析し (CompUtil.parseEverything を使用)、新しいコマンドを作成し、解析したファイルに対して TranslateAlloyToKodkod.execute_command を呼び出し、MiniSat と UNSAT コアを使用して新しく作成したコマンドを呼び出すと、正常に動作します。ただし、後で実行すると、私のプログラムは 2 番目の入力ファイルを解析し (これも 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)

なぜこれが2回目にスローされ、最初にスローされないのか、誰にも分かりますか?

要約すると、次のようなものがあります。

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?
4

2 に答える 2

1

この動作を再現しようとしましたが、できませんでした。MiniSat バイナリを LD_LIBRARY_PATH 環境変数に追加しないと、最初に を呼び出したときに、あなたが言及した例外が発生しますexecute_command。LD_LIBRARY_PATH を構成した後、例外は発生しません。

LD_LIBRARY_PATH を構成するには:

(1) Eclipse を使用している場合は、ソース フォルダーの 1 つを右クリックし、[ビルド パス] -> [ビルド パスの構成] を選択し、[ソース] タブで [ネイティブ ライブラリの場所] が MiniSat があるフォルダーを指していることを確認します。バイナリが存在します。

(2) シェルから実行する場合は、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
于 2012-08-11T01:37:30.133 に答える
0

私の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 を設定しました)。

于 2014-11-06T17:54:52.107 に答える