Alloy api solution set

Question

I have this simple model written in Alloy:

module login

sig Email {}
sig Password {}

sig User {
    login: one Login
}

sig Login {
    email: one Email,
    password: one Password,
    owner: one User,
}

fact {
    all u:User | u.login.owner = u
}

assert a {
    all l:Login | one l.owner
    all u:User | one u.login.email
    all u:User | u.login.owner = u
}

check a for 3

If I run this with the alloy analyser GUI it says:

No counterexample found. Assertion may be valid. 11ms.

But if I run the same model with the API in my java program it returns:

---OUTCOME---

Unsatisfiable.

And not even 1 solutions is shown.

Can anyone help me to detect the problem?

Here goes the code in java using the API:

A4Reporter rep = new A4Reporter();

            try {

                Module loaded_model = CompUtil.parseEverything_fromFile(rep, null, model.getModelpath());
                A4Options options = new A4Options();
                options.solver = A4Options.SatSolver.SAT4J;
                Command cmd = loaded_model.getAllCommands().get(0);

                A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, loaded_model.getAllReachableSigs(), cmd, options);
                System.out.println(sol.toString());
                while (sol.satisfiable()) {
                    System.out.println("[Solution]:");
                    System.out.println(sol.toString());
                    sol = sol.next();
                }
                
            } catch (Err e){
                e.printStackTrace();
            }

Thanks

Answer 1

In both cases no counter-examples are found.

Be aware that the command obtained via the method call loaded_model.getAllCommands().get(0) is check a for 3 in other words, you ask Alloy to look for counter examples.

If you would like to obtain an instance satisfying your constraints - i.e., not a counter-example - you should use a command containing the keyword run instead of check.