Returns true if this sig is a toplevel sig (meaning: it is UNIV, or it is a non-subset sig with parent==UNIV)

Load the given image file from an accompanying JAR file, and return it as an Icon object.

Returns an unmodifiable empty map.

Returns the nodes. @return this.nodes

Returns the number of clauses in this solver. @return #this.clauses

Returns a formula stating that this relation is a partial function with the specified domain and range. @return {f: Formula | f <=> this in domain->ra

Returns product[X][Y]. @return product[X][Y]

Retains only the elements in this set that are contained in the specified set. @ensures this.ints' = this.ints & { i: int | c.contains(i) } @return th

Sets the specified index to the given value. @requires value in this.factory.components @ensures this.elements'[index] = value @throws NullPointerExc

Returns this.translated. @return this.translated

Returns the universe from which the tuples in this instance are drawn. @return this.universe

Will be called for all visit methods. If it returns true then null is returned otherwise the normal visit method is called. @param x the expr that is

Helper method that returns true if the given attribute value in the given XML node is equal to "yes"

Returns a tuple set that contains all tuples in the specified area of the n-dimensional space, where n is the arity of the argument tuples. For examp

Sets the value at the specified index to the given value; returns the value previously at the specified position. It performs no index or null checkin

Returns an encoding of sequence lookup using relational join, where seq is a sequence (binary relation from integers to values) and idx is an integer.

Returns an encoding of sequence lookup using relational join, where seq is a sequence (binary relation from integers to values) and idx is an integer.

Returns the filename.

Returns null if the attribute doesn't exist, or is malformed.

Implementation of the CLR insertion algorithm. @requires no z.key & this.nodes.key @ensures this.nodes' = this.nodes + z

Returns an Int that represents the given number using this.intEncoding. @return { i: Int | [[i]] = number && i.encoding && this.intEncoding && i.facto

Returns the layer that this node is in.

Returns the translation logging level (0, 1, or 2), where 0 means logging is not performed, 1 means only the translations of top level formulas are lo

Returns the number of primary variables allocated during translation. Primary variables represent the tuples of relations in this.bounds that have di

Returns the relation representing the atoms which are ordered by this.relation. @return this.ordered

This terminates the subprocess, and prevent any further results from reaching the parent's callback handler.

Returns sum[X][Y]. @return sum[X][Y]

Whether the solver should run in unbounded mode. Will require an appropriate {@link UnboundedSolver solver} that is able to handle such execution mode

Returns an unmodifiable view of this Bounds object. @return an unmodifiable view of his Bounds object.

Returns this.variable. @return this.variable

Returns true if n has already been visited with the current value of the negated flag; otherwise returns false. @ensures records that n is being visit

Returns the expression corresponding to the given sig.

Removes any messages written in "red" style.

Returns the indices of the axioms that form the unsatisfiable core of this trace. @return { i: int | no this.elts[i].antecedents and this.elts[i] in t

Return the body of this predicate/function. <br> If the user has not called setBody() to set the body, <br> then the default body is "false" (if this

Returns the String that will be displayed in the GUI to represent this value.

Assuming layout() has been called, this returns the left edge.

If type==univ, return null; otherwise, return a nonnull AlloyType object representing its super type. <br> (In particular, if "type" does not exist in

Return the entire text.

Returns a map whose key set is the unsatisfiable subset of the top-level conjunctions of this.log.formula as given by {@linkplain #core() this.core()}

Returns the formula (this implies x) <p> this and x must both be formulas

Returns the ith input to this gate. @return this.inputs[i] @requires 0 <= i < size @throws IndexOutOfBoundsException i < 0 || i >= #this.inputs

Returns a new iterator over the given array of items. The iterator is backed by the given array. The contents of the array are not modified by the it

Returns the entry with the largest index. If the sequence is empty, returns null. @return {e: IndexedEntry | e.index = max(this.entries.E) &&

Write a clickable link into the log window.

Write "msg" in red style (with automatic line wrap).

Returns a BooleanMatrix with the given dimensions and this as the factory for its non-FALSE components. The returned matrix can store any value from

Construct a new JMenu and add it to an existing JMenuBar. <p> Note: every time the user expands then collapses this JMenu, we automatically enable all

@ensures adds newline plus this.indent spaces to this.tokens

Returns the formula (no this) <p> this must be a set or a relation

Push a state number onto the stack.

Parse the XML element into an AlloyInstance. <p> The list of sigs, if not null, will be used as the sigs (and their fields) that we expect to exist; <

Returns true if there is a satisfying assignment for this.clauses. Otherwise returns false. If this.clauses are satisfiable, the satisfying assignmen

Dumps the Kodkod solution into String.

Returns a DOT representation of this graph.

Make a new width value, set new current preferred size and size, and try to get this component repainted. Currently all listener events incur this, wh

Validate the given filename to see if it is a valid Alloy XML instance file.

Write the given array of bytes into this byte buffer.

Accepts the given visitor and returns the result. @see kodkod.ast.Node#accept(kodkod.ast.visitor.ReturnVisitor)

Returns a new matrix such that an entry in the returned matrix represents a conjunction of the corresponding entries in this and other matrix. The ef

Use the platform's preferred file chooser to ask the user to select a file. <br> Note: if it is a save operation, and the user didn't include an exten

Caches the given replacement for the specified node, if the node is a syntactically shared expression, int expression or declaration with no free vari

Returns cartesian_product2[A][B] @return cartesian_product2[A][B]

Returns its immediate children sigs (not including NONE) <p> Note: if this==UNIV, then this method will throw an exception, since we don't keep track

@return 0->lit

Returns the formula (this==x) <p> this and x must be expressions with the same arity, or both be integer expressions

Return an unmodifiable list of all commands in this module.

Return the list of fields as a unmodifiable list of declarations (where you can see which fields are declared to be disjoint)

Returns the Icon that will be displayed in the GUI to represent this value, when used with the given palette.

This method terminates the caller's process.

Returns the expression (this intersects x) <p> this and x must be expressions with the same arity

Returns a new type { A&B | A is in this, and B is in that } <p> ReturnValue.is_int == false <br> ReturnValue.is_bool == false <p> If this.size()==0, o

If this is loneOf/oneOf/someOf/exactlyOf expression, return loneOf/oneOf/someOf/exactlyOf, otherwise returns setOf.

Returns the number of dimensions in this Dimensions object. @return this.n

@return e.pre

Returns this.quantifier. @return this.quantifier

Returns the set of all relations bound by this Bounds. The returned set does not support the add operation. It supports removal iff this is not an unm

Regenerate the comboboxes and the graph.

Resolves this expression if ambiguous. (And if t.size()>0, it represents the set of tuples whose presence/absence is relevant to the parent expression