Как перечислить все решения?

Question

Я хочу использовать анализатор сплавов для перечисления всех решений из предиката в заданной области. С помощью этой функции можно использовать сплав? Если это возможно, как вызвать его из командной строки?

Спасибо

Answer 1

Вот код, который делает это. В этом примере вы пишете обычный файл модели сплава (где вы указываете область) и используете этот код для его запуска, т. Е. Перечисляете все решения для каждой команды, присутствующей в файле модели.

public void run(String filename) { 
    A4Reporter rep = new A4Reporter(); 
    Module world = CompUtil.parseEverything_fromFile(rep, null, filename); 
    A4Options options = new A4Options(); 
    options.solver = A4Options.SatSolver.SAT4J; 
    // options.symmetry = 0; // optionally turn off symmetry breaking 
    for (Command command: world.getAllCommands()) { 
     // Execute the command 
     A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options); 
     while (sol.satisfiable()) { 
      System.out.println("[Solution]:"); 
      System.out.println(sol.toString()); 
      sol = sol.next(); 
     } 
    } 
} 

Answer 2

Да, сплав действительно позволяет Вам перечислить все «возможное» решение в конечной Вселенной. Но он использует алгоритм нарушения симметрии (SB), чтобы разбить все симметрии (ну, большинство из них). Таким образом, вы не сможете перечислять все возможные решения. С другой стороны, даже вы можете отключить SB, вы можете получить значительное количество экземпляров для своей модели. В конечном итоге это закончится, но вы просто не знаете, когда и это действительно зависит от вашего объема. Я помню, что внутри файлов jar (ExampleUsingTheCompiler.java и ExampleUsingTheAPI) есть примеры использования API для вызова сплава, и вы можете использовать его для перечисления ваших решений.