edu.mit.csail.sdg.alloy4compiler.ast
Class Command

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.Browsable
      edu.mit.csail.sdg.alloy4compiler.ast.Command

public final class Command
extends Browsable

Immutable; reresents a "run" or "check" command.

Invariant: expects == -1, 0, or 1

Invariant: overall >= -1

Invariant: bitwidth >= -1

Invariant: maxseq >= -1

Invariant: maxstring >= -1

Field Summary

ConstList<Sig>	additionalExactScopes This stores a list of Sig whose scope shall be considered "exact", but we may or may not know what its scope is yet.
int	bitwidth The integer bitwidth (0 or higher) (Or -1 if it was not specified).
boolean	check true if this is a "check"; false if this is a "run".
int	expects The expected answer (either 0 or 1) (Or -1 if there is no expected answer).
Expr	formula The formula associated with this command.
java.lang.String	label The label for the command; it is just for pretty-printing and does not have to be unique.
int	maxseq The maximum sequence length (0 or higher) (Or -1 if it was not specified).
int	maxstring The number of String atoms to allocate (0 or higher) (Or -1 if it was not specified).
int	overall The overall scope (0 or higher) (Or -1 if there is no overall scope).
Command	parent If nonnull, it means this command depends on this parent command.
Pos	pos The position in the original file where this command was declared; never null.
ConstList<CommandScope>	scope The list of scopes.

Constructor Summary

Command(boolean check, int overall, int bitwidth, int maxseq, Expr formula)
Constructs a new Command object.

Command(Pos pos, java.lang.String label, boolean check, int overall, int bitwidth, int maxseq, int expects, java.lang.Iterable<CommandScope> scope, java.lang.Iterable<Sig> additionalExactSig, Expr formula, Command parent)
Constructs a new Command object.

Method Summary

Command	change(ConstList<CommandScope> scope) Constructs a new Command object where it is the same as the current object, except with a different scope.
Command	change(Expr newFormula) Constructs a new Command object where it is the same as the current object, except with a different formula.
Command	change(Sig... additionalExactScopes) Constructs a new Command object where it is the same as the current object, except with a different list of "additional exact sigs".
Command	change(Sig sig, boolean isExact, int newScope) Constructs a new Command object where it is the same as the current object, except with a different scope for the given sig.
Command	change(Sig sig, boolean isExact, int startingScope, int endingScope, int increment) Constructs a new Command object where it is the same as the current object, except with a different scope for the given sig.
java.util.Set<java.lang.String>	getAllStringConstants(java.lang.Iterable<Sig> sigs) Return a modifiable copy of the set of all String constants used in this command or in any facts embedded in this command.
ConstList<Sig>	getGrowableSigs() Helper method that returns true iff this command contains at least one growable sig.
java.lang.String	getHTML() Returns the description (as HTML) to show for this node.
CommandScope	getScope(Sig sig) Helper method that returns the scope corresponding to a given sig (or return null if the sig isn't named in this command)
java.util.List<? extends Browsable>	getSubnodes() Returns a list of subnodes for this node.
Pos	pos() Returns a Pos object representing the position of this Expr.
Pos	span() Returns a Pos object representing the entire span of this Expr and all its subexpressions.
java.lang.String	toString() Returns a human-readable string that summarizes this Run or Check command.

Methods inherited from class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

make, make, make, make, showAsTree

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

parent

public final Command parent

If nonnull, it means this command depends on this parent command.

pos

public final Pos pos

The position in the original file where this command was declared; never null.

label

public final java.lang.String label

The label for the command; it is just for pretty-printing and does not have to be unique.

check

public final boolean check

true if this is a "check"; false if this is a "run".

overall

public final int overall

The overall scope (0 or higher) (Or -1 if there is no overall scope).

bitwidth

public final int bitwidth

The integer bitwidth (0 or higher) (Or -1 if it was not specified).

maxseq

public final int maxseq

The maximum sequence length (0 or higher) (Or -1 if it was not specified).

maxstring

public final int maxstring

The number of String atoms to allocate (0 or higher) (Or -1 if it was not specified).

expects

public final int expects

The expected answer (either 0 or 1) (Or -1 if there is no expected answer).

formula

public final Expr formula

The formula associated with this command.

scope

public final ConstList<CommandScope> scope

The list of scopes.

additionalExactScopes

public final ConstList<Sig> additionalExactScopes

This stores a list of Sig whose scope shall be considered "exact", but we may or may not know what its scope is yet.

Constructor Detail

Command

public Command(boolean check,
               int overall,
               int bitwidth,
               int maxseq,
               Expr formula)
        throws ErrorSyntax

Constructs a new Command object.

Parameters:

check - - true if this is a "check"; false if this is a "run"

overall - - the overall scope (0 or higher) (-1 if no overall scope was specified)

bitwidth - - the integer bitwidth (0 or higher) (-1 if it was not specified)

maxseq - - the maximum sequence length (0 or higher) (-1 if it was not specified)

formula - - the formula that must be satisfied by this command

Throws:

ErrorSyntax

Command

public Command(Pos pos,
               java.lang.String label,
               boolean check,
               int overall,
               int bitwidth,
               int maxseq,
               int expects,
               java.lang.Iterable<CommandScope> scope,
               java.lang.Iterable<Sig> additionalExactSig,
               Expr formula,
               Command parent)

Constructs a new Command object.

Parameters:

pos - - the original position in the file (must not be null)

label - - the label for this command (it is only for pretty-printing and does not have to be unique)

check - - true if this is a "check"; false if this is a "run"

overall - - the overall scope (0 or higher) (-1 if no overall scope was specified)

bitwidth - - the integer bitwidth (0 or higher) (-1 if it was not specified)

maxseq - - the maximum sequence length (0 or higher) (-1 if it was not specified)

expects - - the expected value (0 or 1) (-1 if no expectation was specified)

scope - - a list of scopes (can be null if we want to use default)

additionalExactSig - - a list of sigs whose scope shall be considered exact though we may or may not know what the scope is yet

formula - - the formula that must be satisfied by this command

Method Detail

toString

public final java.lang.String toString()

Returns a human-readable string that summarizes this Run or Check command.

Overrides:

toString in class java.lang.Object

change

public Command change(Expr newFormula)

Constructs a new Command object where it is the same as the current object, except with a different formula.

change

public Command change(ConstList<CommandScope> scope)

Constructs a new Command object where it is the same as the current object, except with a different scope.

change

public Command change(Sig... additionalExactScopes)

Constructs a new Command object where it is the same as the current object, except with a different list of "additional exact sigs".

change

public Command change(Sig sig,
                      boolean isExact,
                      int newScope)
               throws ErrorSyntax

Constructs a new Command object where it is the same as the current object, except with a different scope for the given sig.

Throws:

ErrorSyntax

change

public Command change(Sig sig,
                      boolean isExact,
                      int startingScope,
                      int endingScope,
                      int increment)
               throws ErrorSyntax

Constructs a new Command object where it is the same as the current object, except with a different scope for the given sig.

Throws:

ErrorSyntax

getScope

public CommandScope getScope(Sig sig)

Helper method that returns the scope corresponding to a given sig (or return null if the sig isn't named in this command)

getGrowableSigs

public ConstList<Sig> getGrowableSigs()

Helper method that returns true iff this command contains at least one growable sig.

getAllStringConstants

public java.util.Set<java.lang.String> getAllStringConstants(java.lang.Iterable<Sig> sigs)
                                                      throws Err

Return a modifiable copy of the set of all String constants used in this command or in any facts embedded in this command.

Throws:

Err

pos

public final Pos pos()

Returns a Pos object representing the position of this Expr.

Overrides:

pos in class Browsable

span

public final Pos span()

Returns a Pos object representing the entire span of this Expr and all its subexpressions.

Overrides:

span in class Browsable

getHTML

public java.lang.String getHTML()

Returns the description (as HTML) to show for this node.

Specified by:

getHTML in class Browsable

getSubnodes

public java.util.List<? extends Browsable> getSubnodes()

Returns a list of subnodes for this node.

Specified by:

getSubnodes in class Browsable