Alloy API приводит к ошибке java.lang.UnsatisfiedLinkError

В настоящее время я использую Alloy Analyzer 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?

java api alloy
person Jan Gorzny    schedule 10.08.2012    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Я пытался воспроизвести это поведение, но не смог. Если я не добавлю двоичные файлы MiniSat в переменную среды LD_LIBRARY_PATH, я получу исключение, о котором вы упомянули, в самый первый раз, когда я вызываю execute_command. После настройки LD_LIBRARY_PATH исключение не возникает.

Чтобы настроить LD_LIBRARY_PATH:

(1) при использовании Eclipse вы можете щелкнуть правой кнопкой мыши одну из ваших исходных папок, выбрать «Путь сборки» -> «Настроить путь сборки», затем на вкладке «Источник» убедитесь, что «Местоположение собственной библиотеки» указывает на папку, в которой находится MiniSat. бинарники проживают.

(2) при запуске из оболочки просто добавьте путь к папке с бинарниками 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
person Aleksandar Milicevic    schedule 11.08.2012
comment
Идеальный; метод затмения сработал! Спасибо. До сих пор странно, что у меня был один успешный вызов метода без исключения, но пока он работает, я доволен. Спасибо. - person Jan Gorzny; 13.08.2012
comment
Возможно, первая модель (someFile.als) была тривиально (не)удовлетворительной, и в этом случае Kodkod не нужно запускать базовый SAT-решатель, поэтому ошибка не возникает. - person Aleksandar Milicevic; 13.08.2012

arrow_upward
0
arrow_downward

Я использую 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 нужна целочисленная модель, которая находится в файле сплава4.2.jar в папке /models/util/. Но когда я запускаю приложение, оно пытается напрямую найти файл util/Integer.als. Это вызывает исключение. Можно ли исправить эту проблему?

Кроме того, я также попытался поместить сплав 4.2.jar в проект плагина eclipse и запустить свое приложение как приложение eclipse (запустив мое приложение как плагин). С решателем по умолчанию у приложения вообще нет проблем. Но когда я переключаюсь на MiniSatProverJNI, возникает проблема, упомянутая здесь (я установил сплав4.2.jar в качестве пути к классам).

person wxlfrank    schedule 06.11.2014