Alloy api Lösung gesetzt

Question

ich dieses einfache Modell in Alloy geschrieben haben:

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 

Wenn ich dies mit der Legierung Analysator GUI laufen heißt es:

Kein Gegenbeispiel gefunden. Behauptung kann gültig sein. 11ms.

Aber wenn ich das gleiche Modell mit der API in meinem Java-Programm führen Sie es zurück:

--- --- ERGEBNIS

unerfüllbar.

Und nicht einmal 1 Lösungen wird angezeigt.

Kann mir jemand helfen, das Problem zu erkennen?

geht hier den Code in Java unter Verwendung der 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(); 
      } 

Dank

Answer 1

In beiden Fällen keine Gegenbeispiele zu finden sind.

Beachten Sie, dass der über den Methodenaufruf loaded_model.getAllCommands().get(0) erhaltene Befehl check a for 3 lautet. Mit anderen Worten, Sie bitten Alloy, nach Gegenbeispielen zu suchen.

Wenn Sie eine Instanz erhalten möchten, die Ihren Bedingungen entspricht - also kein Gegenbeispiel -, sollten Sie einen Befehl mit dem Schlüsselwort run anstelle von check verwenden.