Mutable; this class encapsulates the customizable options of the Alloy-to-Kodkod translator. @modified [electrum] electrod smv solvers; decompose str

@modified [electrum] added decompose strategy option

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. @modified [electrum] incrementally builds a solution by

This helper class contains helper routines for writing an A4Solution object out as an XML file. @modified [electrum] prints full trace instance into

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.

A KK encoding of ALG195+1.p from http://www.cs.miami.edu/~tptp/ @author Emina Torlak

@author emina

A KK encoding of ALG197+1.p from http://www.cs.miami.edu/~tptp/ @author Emina Torlak

A KK encoding of ALG212+1.p from http://www.cs.miami.edu/~tptp/ @author Emina Torlak

Indicates that a solving or evaluation task has been aborted. @author Emina Torlak

<p>A depth first collector. Subclasses should override the methods in which detection is performed to return the appropriate set. For example, a Vari

<p>A depth first detector. Subclasses should override the methods in which detection is performed to return TRUE. For example, a Variable detector co

A skeletal implementation of the IntCollection interface. @author Emina Torlak

A skeletal implementation of the IntSet interface. @author Emina Torlak

A skeletal implementation of the IntVector interface. @specfield length: int @specfield elements: [0..size) ->one int @author Emina Torlak

Stores common fields and methods for the ascending and descending iterators.

A depth first replacer. The default implementation returns the tree to which it is applied. Reference equality is used to determine if two nodes are

A skeleton implementation of the {@link Reporter} interface. The default implementation for each method has an empty body.s @author Emina Torlak @modi

The most general relational constraint solver interface, independent of the underlying technology (bounded vs. unbounded) and functionalities (tempora

A skeletal implementation of the SparseSequence interface. The class provides an implementation for the <code>isEmpty</code>, <code>putAll</code>, <co

Implements a depth first traversal of the kodkod AST. @author Emina Torlak @modified Eduardo Pessoa, Nuno Macedo // [HASLab] temporal model finding

KK encoding of mondex/a.als together with mondex/common.als. @author Emina Torlak

Represents the acyclic predicate. The predicate states that the given <code>relation</code> is acyclic. @specfield relation: Relation @invariant name

Adaptive Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level. Specifically, let C be a core that is

This class is the main class for the JAR. Its name is the name shown in the GUI on MacOS, so do not change it. <p> This class is an entry point and sh

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

Class for globally accessible things.

Since the Alloy code is used for many different situations, we do not assume we know how the world looks like. This class uses the AlloyMain annotatio

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

A central class for general graphic support functions in Alloy that have no good other place

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. @modified [electr

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

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. @mo

A node annotated with information about structural sharing in its ast/dag. The class also provides utility methods for collecting various information

An immutable set of integers, stored in a sorted array. @specfield ints: set int @author Emina Torlak

A mutable implementation of the <tt>IntVector</tt> interface. Implements all optional IntVector operations. In addition to implementing the <tt>IntV

An unmodifying iterator over an array.

An implementation of a sparse sequence based on an array. This implementation can be used only when the indices of the sequence are known in advance.

A Stack implementation based on an array. @author Emina Torlak

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>

An ascending iterator over an array.

An iterator that returns the elements of this int set in the ascending order. @author Emina Torlak

An iterator that returns the entries in this sequence in the ascending order of indices. @author Emina Torlak

Implementation of an ascending iterator over (a subset of) this set.

An iterator that traverses this sequence in the ascending order. @author Emina Torlak

An iterator that traverses the ints in this set in the ascending order. @author Emina Torlak

Wrapper for a method that generates boolean values out of existing gates, using AND and OR operators. @author Emina Torlak

A unary relation representing a reified atom. @author [AlloyTools]

Immutable; represents attributes that can be associated with Signatures and some other AST objects. @modified [electrum] added a new attribute AST ob

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

A kodkod encoding of bigconfig.als: <pre> module internal/bigconfig abstract sig Site {} sig HQ, Sub extends Site {} sig Router { site: Site,

A kodkod encoding of bigconfig.als: <pre> module internal/bigconfig abstract sig Site {} sig HQ, Sub extends Site {} sig Router { site: Site,

A relational {@link kodkod.ast.Expression expression} with two children. @specfield left: Expression @specfield right: Expression @specfield op: Expr

A {@link kodkod.ast.Formula formula} with two children. @specfield left: Formula @specfield right: Formula @specfield op: FormulaOperator @invariant

A logic gate with two inputs. @invariant #this.inputs = 2 @invariant digest = sum(inputs.digest(this.op))

A binary integer expression such as x + y. @specfield left: IntExpression @specfield right: IntExpression @specfield op: IntOperator @specfield op.bin

A temporal {@link kodkod.ast.Formula formula} with two children. @specfield left: Formula @specfield right: Formula @specfield op: TemporalOperator @

This corresponds to the Block structure described in the paper.

Relational Kodkod encoding of the BlockedNQueensProblem. The files should be supplied in the same format as those at http://asparagus.cs.uni-potsdam.d

Relational Kodkod encoding of the BlockedNQueensProblem. The files should be supplied in the same format as those at http://asparagus.cs.uni-potsdam.d

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

Transforms a boolean circuit into a formula in conjunctive normal form. @specfield factory: {@link BooleanFactory} @specfield roots: some factory.comp

An accumulator for easy construction of gates with multiple inputs. An accumulator cannot be combined with other boolean values using BooleanFactory m

A simple action tied to a boolean preference

A boolean constant, true or false. The integer label of the true and false constants are Integer.MAX_VALUE and -Integer.MAX_VALUE, respectively. The

A factory for creating {@link kodkod.engine.bool.BooleanValue boolean values}, {@link kodkod.engine.bool.BooleanMatrix matrices}, and {@link kodkod.en

A non-constant boolean value with zero or more inputs. @specfield op: Operator @specfield size: int @specfield inputs: [0..size) -> one BooleanFormula

<p>An n-dimensional matrix of {@link kodkod.engine.bool.BooleanValue boolean values}. Boolean matrices are indexed using flat integer indeces. For ex

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