Mutable; this class encapsulates the customizable options of the Alloy-to-Kodkod translator.

This class receives diagnostic, progress, and warning messages from Alloy4. (This default implementation ignores all calls; you should subclass it to

This class stores a SATISFIABLE or UNSATISFIABLE solution. It is also used as a staging area for the solver before generating the solution. Once solve

This helper class contains helper routines for reading an A4Solution object from an XML file.

This helper class contains helper routines for writing an A4Solution object out as an XML file.

Immutable; represents a single Alloy tuple; comparison is by identity rather than by value.

Immutable; represents a collection of Alloy tuples; comparison is by identity rather than by value.

Immutable; represents an Alloy atom in an instance. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; it's the abstract superclass extended by AlloyType, AlloySet, and AlloyRelation. <p><b>Thread Safety:</b> Can be called only by the AWT ev

Immutable; represents an Alloy instance that can be displayed in the visualizer. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; represents an Alloy model. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; it's the abstract superclass extended by both AlloyType and AlloySet. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; represents a set of types to be projected, plus the exact atom chosen for each type to be projected. <p><b>Thread Safety:</b> Can be calle

Immutable; represents an Alloy relation of 2 or higher arity. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; represents an Alloy set in an instance. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; represents an Alloy tuple. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; represents an Alloy toplevel signature or an Alloy subsignature. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

This class abstracts the drawing operations so that we can draw the graph using different frameworks such as Java2D or PDF. <p><b>Thread Safety:</b>

Immutable; represents attributes that can be associated with Signatures and some other AST objects.

This class contains all possible attribute types.

Mutable; this allows you to compute whether a rectangle overlaps with a set of rectangles or not. <p><b>Thread Safety:</b> Can be called only by the

This corresponds to the Block structure described in the paper.

Immutable; this class stores the set of solutions from the book, for teaching purpose, so that users of the tool will see the same illustration as the

A simple action tied to a boolean preference

This reads and writes boolean-valued Java persistent preferences. <p><b>Thread Safety:</b> Safe.

Immutable; this class assigns each sig and field to some Kodkod relation or expression, then set the bounds.

Mutable; represents a rectangle.

This abstract class represents a node that can be browsed in the graphical parse tree viewer.

Mutable; implements a growable array of bytes. <p> This class is more efficient than Java's ByteArrayOutputStream when writing large amount of data,

This reads and writes multi-choice persistent preferences.

Immutable; reresents a "run" or "check" command. <p> <b>Invariant:</b> expects == -1, 0, or 1 <p> <b>Invariant:</b> overall >= -1 <p> <b>Invariant:

Immutable; reresents a scope in a "run" or "check" command. <p> <b>Invariant:</b> sig != null <p> <b>Invariant:</b> endingScope >= startingScope >=

This class sits between the lexer and the parser. <p> Reason: there are 3 sets of "special tokens" that the lexer will not output. But the Parser exp

Autogenerated by JFlex 1.4.1

Mutable; this class represents an Alloy module; equals() uses object identity.

CUP v0.11a beta 20060608 generated parser. @version Sat Jan 31 16:47:48 EST 2015

CUP generated class containing symbol constants.

This class provides convenience methods for calling the parser and the compiler.

This defines a compute() method that takes an Object input and produces a String output.

Immutable; implements a list based on equals(); null values are allowed. @param <T> - the type of element

Immutable; implements a map based on hashCode() and equals(); null key and values are allowed. @param <K> - the type of key @param <V> - the type of

Immutable; implements a set based on hashCode() and equals(); null value is allowed. @param <K> - the type of element

Mutable; this class represents the current typechecking context.

Immutable; this class rearranges the AST to promote as many clauses up to the top level as possible (in order to get better precision unsat core resul

Mutable; represents a connected path. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; this declaration binds a list of names to an expression.

This visitor assumes the input expression is already fully typechecked, and derive a tight bound on the return type.

Provides a way to delay supplying valid choices and a default value

This class demonstrates how to access Alloy4 via the API, by modeling a simple file system.

Mutable; implements a directed graph; null node is allowed. <p> Note: it uses n1==n2 for comparing nodes rather than using n1.equals(n2) @param <N>

Immutable; this defines the set of possible colors. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; this defines the set of possible edge directions. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; this defines the set of possible color palettes. <p><b>Thread Safety:</b> Can be called only by the AWT event thread.

Immutable; this defines the set of possible node shapes (BOX, CIRCLE, ELLIPSE...) <p><b>Thread Safety:</b> Can be called only by the AWT event thread

Immutable; this defines the set of possible line styles (SOLID, DASHED, DOTTED...) <p><b>Thread Safety:</b> Can be called only by the AWT event threa

Mutable; implements a undoable map based on hashCode() and equals(); null key and values are allowed. <p> To be more precise, every key is internal

Immutable; this is the abstract parent class of the various possible errors.

Immutable; this represents an API usage error.

Immutable; this represents a fatal error.

Immutable; this represents a syntax error that should be reported to the user.

Immutable; this represents a type error that should be reported to the user.

Immutable; this represents a nonfatal warning that should be reported to the user.

This defines the list of possible events.

This class demonstrates how to access Alloy4 via the API.

This class demonstrates how to access Alloy4 via the compiler methods.

Immutable; represents a formula or expression. <p> <b>Invariant:</b> pos!=null <br> <b>Invariant:</b> type!=null <br> <b>Invariant:</b> type==EMP

Immutable; represents an illegal node. <p> <b>Invariant:</b> this.type==EMPTY && this.errors.size()==1

Immutable; represents an illegal pred/fun call. <p> <b>Invariant:</b> this.type==EMPTY && this.errors.size()>0

Immutable; represents an illegal relation join. <p> <b>Invariant:</b> this.type==EMPTY && this.errors.size()>0

Immutable; represents an expression of the form (x OP y). <p> <b>Invariant:</b> type!=EMPTY => (this.mult!=1) <p> <b>Invariant:</b> type!=EMPTY =>

Immutable; represents a call. <p> <b>Invariant:</b> type!=EMPTY => (all x:args | x.mult==0)

Immutable; represents an unresolved node that has several possibilities.

Immutable; represents a constant in the AST.

Immutable; represents a custom node. <p> <b>Invariant:</b> this.type==EMPTY && this.errors.size()==1

Immutable; represents a named entity (such as a Field, or a LET or QUANTIFICATION variable, or a function/predicate parameter).

Immutable; represents an if-then-else expression. <p> <b>Invariant:</b> type!=EMPTY => (cond.mult==0 && left.mult==0 && right.mult==0)

Immutable; represents an expression of the form (let a=b | x). <p> <b>Invariant:</b> type!=EMPTY => (var.type.unambiguos() && sub.mult==0)

Immutable; represents disjoint[] or pred/totalOrder[] or (... and ... and ..) and other similar list of arugments. <p> <b>Invariant:</b> type!=EMPTY

Immutable; represents a quantified expression. It can have one of the following forms: <br> <br> ( all a,b:t | formula ) <br> ( no a,b:t | form

Immutable; represents a unary expression of the form "(OP subexpression)" <p> <b>Invariant:</b> type!=EMPTY => sub.mult==0

Immutable; represents a LET or QUANTIFICATION variable in the AST. <p> <b>Invariant:</b> type!=EMPTY => (type==expr.type && !expr.ambiguous)

Mutable; represents a field.