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

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

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();
        }
    }
}

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