Как оценить предикат в исходном коде Alloy?

У меня есть предикат в моей модели Alloy с именем LS, который получает экземпляр sig с именем st. Я пытаюсь оценить этот предикат для экземпляра st с именем st$0 в исходном коде. Я могу найти решение типа A4Solution, называемое ans. Но я не знаю, как я могу оценить этот предикат в этом решении.


alloy
person Fathiyeh    schedule 10.03.2014    source источник
comment
пожалуйста, опубликуйте скелетный код, который у вас уже есть, и тогда я смогу помочь вам реализовать недостающие части.   -  person Aleksandar Milicevic    schedule 10.03.2014

Ответы (1)


arrow_upward
1
arrow_downward

Вот как вы можете в целом оценивать предикаты с помощью API.

String fileName = "<file path to your alloy model>";
Module world = CompUtil.parseEverything_fromFile(rep, null, fileName);
A4Options opt = new A4Options();
opt.solver = A4Options.SatSolver.SAT4J;

// run the first command for the sake of this example
Command cmd = world.getAllCommands().get(0);
A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), cmd, opt);

// evaluate the first defined function/predicate applied to the first defined Sig
Func func = world.getAllFunc().get(0);
Sig sig = world.getAllSigs().get(0);
System.out.println(sol.eval(func.call(sig)));
person Aleksandar Milicevic    schedule 12.03.2014