Returns the index in this vector of the last occurrence of the specified element, or -1 if this vector does not contain this element. @return element

If the given node has already been visited and its replacement cached, the cached value is returned. Otherwise, null is returned. @return this.cache[

@return true if the given expression should be parenthesized when a child of a compound parent

@return true if the given expression should be parenthesized when a child of a compound parent

Removes from this set all of its elements that are contained in the specified set. @ensures this.ints' = this.ints - { i: int | c.contains(i) } @retur

Returns an expression whose meaning is the singleton set containing the atom that represents the integer given by this integer expression. The effect

Returns a String representation of this position value.

Returns the Y coordinate of the center of the node.

Returns this.defCond @return this.defCond

Return an unmodifiable empty list.

Prints the given solution using the given options to the console

Returns the relation to which this predicate applies. @return this.relation

@ensures this.tokenize' = (parenthesize => concat [ this.tokens, "(", tokenize[child], ")" ] else concat [ this.tokens, tokenize[

@ensures this.tokenize' = (parenthesize => concat [ this.tokens, "(", tokenize[child], ")" ] else concat [ this.tokens, tokenize[

Returns true if exists at least one (k, v) mapping where (k==null ? key==null : k.equals(key))

Returns the else-expression. @return this.elseExpr

Given a node, return its name (if no name has been chosen, then make a new name)

{@inheritDoc}

Returns the then-expression. @return this.thenExpr

Popup the given error message.

Returns the if-condition. @return this.condition

Tests whether the specified object reference is a key in this fixed map. @return key in this.keys

Commits all outstanding writes (if the messages are buffered).

Retrieves the cached translation for the given node, if any. Otherwise returns null. @return the cached translation for the given node, if any. Otherw

Constructs an ExprVar variable with the EMPTY type @param pos - the original position in the source file (can be null if unknown) @param l

Returns a primitive solver factory used to generate {@link kodkod.engine.PrimitiveSolver primitive solvers}. @return a primitive solver factory

Returns the least sound upper bound on the value of expr @return the least sound upper bound on the value of expr

Converts the given accumulator into an immutable boolean value and adds it to this.components. This method requires that all of g's inputs are in this

Write a list of Strings into a PrintWriter, where strs[2n] are written as-is, and strs[2n+1] are XML-encoded. <p> For example, if you call encodeXML(o

Returns the size of the list.

Returns a tree based implementation of BooleanAccumulator. The addInput operation executes in O(lg n) time where n is the number of gate inputs. @retu

Caches the given value for the specified node, if this is a caching visitor, and returns it. @ensures n in this.cached => this.cache' = this.cache ++

Returns true if the elements of c are a subset of this set. @return { i: int | c.contains(i) } in this.ints @throws NullPointerException c = null

Returns the expression (this.x) <p> 1. this must be a set or relation <p> 2. x must be a set or relation <p> 3. at most one of them can be a unary set

Write "msg" in bold style.

If n has been visited and a value for it cached, the cached value is returned. Otherwise null is returned. @return this.cache[n]

If n has been visited and a value for it cached, the cached value is returned. Otherwise null is returned. @return this.cache[n]

Returns a new, empty, modifiable set. @return a new, empty, modifiable set.

Returns the declaration that constrains this variable to be bound to a subset of the elements in the given expression: 'this: set expr'. @return {d:

Sets the symmetryBreaking option to the given value.

Returns an array containing all of the elements in this set in the ascending order. @return an array containing all of the elements in this set in th

Returns true if this node has already been visited. Otherwise returns false. @return true if this node has already been visited.

Returns an Int that represents the bitwise conjunction of this and the given Int. @requires this.factory = other.factory @return an Int that represent

Make a graphical button @param label - the text to show beneath the button @param tip - the tooltip to show when the mouse hovers over the button @pa

Converts an existing tuple set into an identical tuple set with a different universe. @param tset the existing tuple set from the old univ

Remove the "NOP" in front of an expression (if any).

Convenience method that generates a type error with "msg" as the message, and includes the left and right bounding types in the message.

Returns the parent type of the AlloySet.

Return the number of parameters.

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

Returns true if the XML element has the given attribute.

Construct the n-ary tuple; throws an exception if the given list is empty.

Throws an IOException with the given msg, and associate with it the current line and column location.

Returns the outcome of the attempt to find a model for this.formula. If the outcome is SATISFIABLE or TRIVIALLY_SATISFIABLE, a satisfying instance can

This value is used to display this type in the Visualizer's customization screen.

Returns the comprehension expression constructed from this formula and the given declarations. @requires all d: decls.decls[int] | decl.variable.arity

Return the list containing UNIV, SIGINT, SEQIDX, STRING, NONE, and all sigs defined in this module or a reachable submodule.

Returns the current (possibly projected) model.

Returns the y position at the given point 0 <= t <= 1

Make a JLabel, then call Util.make() to apply a set of attributes to it. @param attributes - see {@link edu.mit.csail.sdg.alloy4.OurUtil#make

Returns an unmodifiable view of the list of nodes in the given layer (0..#layer-1); return an empty list if no such layer.

Construct the set containing integers between min and max (inclusively).

Create a new type consisting of the given set of entries, set of arities, and the given is_int/is_bool values; <p> Precondition: entries and arities m

Return the next token, or <code>null</code> on end-of-file.

Sets the reporter. @param reporter a reporter.

Returns the variable in this declaration. @return this.variable

Adds the given value to this.components and returns the result. Specifically, if the addition of the value causes the gate to evaluate to op.shortCir

Ensures that this solver logically contains the given clause, and returns true if this.clauses changed as a result of the call. No reference to the sp

Returns the arity of this tuple.

If {@code this.solver.solve()} is true, returns an interpretation of the CNF solution as a mapping from Relations to sets of Tuples. The returned ins

If the list if nonempty, arbitrarily return one of the item, otherwise throw ArrayIndexOutOfBoundsException.

Set the background color.

Changes the current color.

Convenience method that generates a type warning with "msg" as the message, and includes the left and right bounding types in the message.

Convenience method that evaluates x and casts the result to be a boolean. @return the boolean - if x evaluates to a boolean @throws ErrorFatal - if x

Returns an expression that combines this and the given integer expression using the specified operator. @requires op.binary() @return {e: IntExpressio

Returns the amount of space we need to reserve on the right hand side for the self edges (0 if this has no self edges now)

Returns the formula (this in x) <p> this must be a set or relation <p> x must be a set or relation or multiplicity constraint <p> this and x must have

Returns a sparse sequence view of this.intBound. The returned sequence is not modifiable. @return a sparse sequence view of this.intBound

Assign the given attributes to the given JComponent, then return the JComponent again. <p> If <b>Font</b> x is given in the list, we call obj.setFont(

Returns the formula (not this) <p> this must be a formula

Query the Bounds object to find the lower/upper bound; throws ErrorFatal if expr is not Relation, nor a {union, product} of Relations.

Returns an unmodifiable sorted set of all AlloyType(s) in this model.

Returns the x position at the given point 0 <= t <= 1