edu.mit.csail.sdg.alloy4compiler.sim
Class SimInstance

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.VisitReturn<java.lang.Object>
      edu.mit.csail.sdg.alloy4compiler.sim.SimInstance

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

Mutable; represents an instance.

Field Summary

Module

root The root module associated with this instance.

Constructor Summary

SimInstance(Module root, int bitwidth, int maxseq)
Construct a new simulation context with the given bitwidth and the given maximum sequence length.

SimInstance(SimInstance old)
Construct a deep copy of this instance (except that it shares the same root Module object as the old instance)

Method Summary

void	addCallback(Func predicateOrFunction, SimCallback callback) Register a callback.
boolean	cform(Expr x) Convenience method that evalutes x and casts the result to be a boolean.
int	cint(Expr x) Convenience method that evalutes x and cast the result to be a int.
SimTupleset	cset(Expr x) Convenience method that evalutes x and cast the result to be a tupleset
boolean	deleteAtom(SimAtom atom) Delete an atom from all sigs/fields/skolem...
boolean	equal(Expr a, Expr b) Helper method that evaluates the formula "a = b"
boolean	hasAtom(SimAtom atom) Returns true if the given atom is an Int atom, or String atom, or is in at least one of the sig.
void	init(ExprVar var, SimTupleset value) Initializes the given var to be associated with the given unary value; should only be called at the beginning.
void	init(Sig.Field field, SimTupleset value) Initializes the given field to be associated with the given unary value; should only be called at the beginning.
void	init(Sig sig, SimTupleset value) Initializes the given sig to be associated with the given unary value; should only be called at the beginning.
boolean	isIn(Expr a, Expr b) Helper method that evaluates the formula "a in b"
boolean	isIn(SimTuple a, Expr b) Helper method that evaluates the formula "a in b" where b.mult==0
SimAtom	makeAtom(Sig sig) Create a fresh atom for the given sig, then return the newly created atom.
static SimInstance	read(Module root, java.lang.String filename, java.util.List<ExprVar> vars) Construct a new simulation context by reading the given file.
java.lang.String	validate(Module world) Checks whether this instance satisfies every fact defined in the given model.
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.
SimTupleset	visit(Sig.Field x) Visits a Field node.
SimTupleset	visit(Sig x) Visits a Sig node.
boolean	wasOverflow()
void	write(java.lang.String filename) Write the bitwidth, maxseq, set of all atoms, and map of all sig/field/var into the given file.

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

Field Detail

root

public final Module root

The root module associated with this instance.

Constructor Detail

SimInstance

public SimInstance(Module root,
                   int bitwidth,
                   int maxseq)
            throws Err

Construct a new simulation context with the given bitwidth and the given maximum sequence length.

Throws:

Err

SimInstance

public SimInstance(SimInstance old)
            throws Err

Construct a deep copy of this instance (except that it shares the same root Module object as the old instance)

Throws:

Err

Method Detail

wasOverflow

public boolean wasOverflow()

write

public void write(java.lang.String filename)
           throws java.io.IOException

Write the bitwidth, maxseq, set of all atoms, and map of all sig/field/var into the given file.

Throws:

java.io.IOException

read

public static SimInstance read(Module root,
                               java.lang.String filename,
                               java.util.List<ExprVar> vars)
                        throws Err,
                               java.io.IOException

Construct a new simulation context by reading the given file.

Throws:

Err

java.io.IOException

addCallback

public void addCallback(Func predicateOrFunction,
                        SimCallback callback)

Register a callback.

hasAtom

public boolean hasAtom(SimAtom atom)

Returns true if the given atom is an Int atom, or String atom, or is in at least one of the sig.

makeAtom

public SimAtom makeAtom(Sig sig)
                 throws Err

Create a fresh atom for the given sig, then return the newly created atom.

Throws:

ErrorAPI - if attempting to add an atom to an abstract sig with children, or a builtin sig, or a subset sig.

Err

deleteAtom

public boolean deleteAtom(SimAtom atom)
                   throws Err

Delete an atom from all sigs/fields/skolem...

The resulting instance may or may not satisfy all facts, and should be checked for consistency.

Returns true if at least one sig/field/var changed its value as a result of this deletion.

Throws:

ErrorAPI - if attempting to delete from "Int".

Err

init

public void init(Sig sig,
                 SimTupleset value)
          throws Err

Initializes the given sig to be associated with the given unary value; should only be called at the beginning.

The resulting instance may or may not satisfy all facts, and should be checked for consistency.

Throws:

Err

init

public void init(Sig.Field field,
                 SimTupleset value)
          throws Err

Initializes the given field to be associated with the given unary value; should only be called at the beginning.

The resulting instance may or may not satisfy all facts, and should be checked for consistency.

Throws:

Err

init

public void init(ExprVar var,
                 SimTupleset value)
          throws Err

Initializes the given var to be associated with the given unary value; should only be called at the beginning.

The resulting instance may or may not satisfy all facts, and should be checked for consistency.

Throws:

Err

cform

public boolean cform(Expr x)
              throws Err

Convenience method that evalutes x and casts the result to be a boolean.

Returns:

the boolean - if x evaluates to a boolean

Throws:

ErrorFatal - - if x does not evaluate to a boolean

Err

cint

public int cint(Expr x)
         throws Err

Convenience method that evalutes x and cast the result to be a int.

Returns:

the int - if x evaluates to an int

Throws:

ErrorFatal - - if x does not evaluate to an int

Err

cset

public SimTupleset cset(Expr x)
                 throws Err

Convenience method that evalutes x and cast the result to be a tupleset

Returns:

the tupleset - if x evaluates to a tupleset

Throws:

ErrorFatal - - if x does not evaluate to a tupleset

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(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(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(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(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(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 SimTupleset visit(Sig x)
                  throws Err

Visits a Sig node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

visit

public SimTupleset 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(ExprQt x)
                       throws Err

Visits an ExprQt node.

Specified by:

visit in class VisitReturn<java.lang.Object>

Throws:

Err

isIn

public boolean isIn(SimTuple a,
                    Expr b)
             throws Err

Helper method that evaluates the formula "a in b" where b.mult==0

Throws:

Err

equal

public boolean equal(Expr a,
                     Expr b)
              throws Err

Helper method that evaluates the formula "a = b"

Throws:

Err

isIn

public boolean isIn(Expr a,
                    Expr b)
             throws Err

Helper method that evaluates the formula "a in b"

Throws:

Err

validate

public java.lang.String validate(Module world)

Checks whether this instance satisfies every fact defined in the given model.

Parameters:

world - - this must be the root of the Alloy model

Returns:

an empty String if yes, nonempty String if no