How to enumerate all solutions?

Question

I want to use Alloy Analyzer to enumerate all solutions from a predicate within a given scope. Do Alloy support this feature? If it can, how to call it from command line?

Thank you

Answer 1

Here is the code that does that. In this example, you write a regular Alloy model file (where you specify the scope) and use this code then to run it, i.e., enumerate all solutions for each command present in the model file.

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

Yes, Alloy does allow you to enumerate all 'possible' solutions within a finite universe. But, it uses a symmetry breaking (SB) algorithm to break all the symmetries (well, most of them). Thus, you won't be able to enumerate every single possible solutions. On the other hand, even you can switched off SB, you may get a considerable number of instances for your model. It will terminate eventually, but you just don't know when and it really depends on your scope. I remember that inside jar files (ExampleUsingTheCompiler.java and ExampleUsingTheAPI), there are examples about using APIs to invoke alloy, and you can use that to enumerate your solutions.