edu.mit.csail.sdg.alloy4compiler.translator
Class TranslateAlloyToKodkod

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.VisitReturn<java.lang.Object>
      edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod

public final class TranslateAlloyToKodkod
extends VisitReturn<java.lang.Object>

Translate an Alloy AST into Kodkod AST then attempt to solve it using Kodkod.

Method Summary

static java.lang.Object	alloy2kodkod(A4Solution sol, Expr expr) Translate the Alloy expression into an equivalent Kodkod Expression or IntExpression or Formula object.
static A4Solution	execute_command(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
static A4Solution	execute_commandFromBook(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
java.lang.Object	visit(ExprBinary x) Visits an ExprBinary node.
java.lang.Object	visit(ExprCall x) Visits an ExprCall node.
java.lang.Object	visit(ExprConstant x) Visits an ExprConstant node.
java.lang.Object	visit(ExprITE x) Visits an ExprITE node.
java.lang.Object	visit(ExprLet x) Visits an ExprLet node.
java.lang.Object	visit(ExprList x) Visits an ExprList node.
java.lang.Object	visit(ExprQt x) Visits an ExprQt node.
java.lang.Object	visit(ExprUnary x) Visits an ExprUnary node.
java.lang.Object	visit(ExprVar x) Visits an ExprVar node.
java.lang.Object	visit(Sig.Field x) Visits a Field node.
java.lang.Object	visit(Sig x) Visits a Sig node.

Methods inherited from class edu.mit.csail.sdg.alloy4compiler.ast.VisitReturn

visit, visit, visit, visitThis

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

execute_command

public static A4Solution execute_command(A4Reporter rep,
                                         java.lang.Iterable<Sig> sigs,
                                         Command cmd,
                                         A4Options opt)
                                  throws Err

Based on the specified "options", execute one command and return the resulting A4Solution object.

Parameters:

rep - - if nonnull, we'll send compilation diagnostic messages to it

sigs - - the list of sigs; this list must be complete

cmd - - the Command to execute

opt - - the set of options guiding the execution of the command

Returns:

null if the user chose "save to FILE" as the SAT solver, and nonnull if the solver finishes the entire solving and is either satisfiable or unsatisfiable.

If the return value X is satisfiable, you can call X.next() to get the next satisfying solution X2; and you can call X2.next() to get the next satisfying solution X3... until you get an unsatisfying solution.

Throws:

Err

execute_commandFromBook

public static A4Solution execute_commandFromBook(A4Reporter rep,
                                                 java.lang.Iterable<Sig> sigs,
                                                 Command cmd,
                                                 A4Options opt)
                                          throws Err

Based on the specified "options", execute one command and return the resulting A4Solution object.

Note: it will first test whether the model fits one of the model from the "Software Abstractions" book; if so, it will use the exact instance that was in the book.

Parameters:

rep - - if nonnull, we'll send compilation diagnostic messages to it

sigs - - the list of sigs; this list must be complete

cmd - - the Command to execute

opt - - the set of options guiding the execution of the command

Returns:

null if the user chose "save to FILE" as the SAT solver, and nonnull if the solver finishes the entire solving and is either satisfiable or unsatisfiable.

If the return value X is satisfiable, you can call X.next() to get the next satisfying solution X2; and you can call X2.next() to get the next satisfying solution X3... until you get an unsatisfying solution.

Throws:

Err

alloy2kodkod

public static java.lang.Object alloy2kodkod(A4Solution sol,
                                            Expr expr)
                                     throws Err

Translate the Alloy expression into an equivalent Kodkod Expression or IntExpression or Formula object.

Parameters:

sol - - an existing satisfiable A4Solution object

expr - - this is the Alloy expression we want to translate

Throws:

Err

visit

public java.lang.Object visit(ExprITE x)
                       throws Err

Visits an ExprITE node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprLet x)
                       throws Err

Visits an ExprLet node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprConstant x)
                       throws Err

Visits an ExprConstant node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprUnary x)
                       throws Err

Visits an ExprUnary node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprVar x)
                       throws Err

Visits an ExprVar node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(Sig.Field x)
                       throws Err

Visits a Field node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(Sig x)
                       throws Err

Visits a Sig node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprCall x)
                       throws Err

Visits an ExprCall node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprList x)
                       throws Err

Visits an ExprList node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprBinary x)
                       throws Err

Visits an ExprBinary node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public java.lang.Object visit(ExprQt x)
                       throws Err

Visits an ExprQt node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err