de.upb.swt.mcie.formulas
Class Variable

java.lang.Object
  extended by de.upb.swt.mcie.formulas.Formula
      extended by de.upb.swt.mcie.formulas.Variable

public class Variable
extends Formula

Implements a variable in a formula. It represents the name and the information whether it is a primed or unprimed variable.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
private  java.lang.String name
          The identifier (name) of this variable.
private  boolean primed
          Tells whether the variable is primed or not.
 
Fields inherited from class de.upb.swt.mcie.formulas.Formula
step, temporal
 
Constructor Summary
Variable(java.lang.String name, boolean primed)
          Constructs a variable.
 
Method Summary
 void addChangedVariables(ChangeSet changeset)
          Adds all variables that occur primed within the formula to the given change set.
 boolean isStateFormula()
          Checks whether the formula is a state formula.
 boolean isStepFormula()
          Checks whether the formula is a step formula.
 boolean isTemporalFormula()
          Checks whether the formula is a temporal formula.
 ROBDD toROBDD(Context context)
          Returns the ROBDD that represents the set of all states in which this formula is valid.
 ROBDD toROBDD(Model model)
          Returns the ROBDD that represents the set of all states in which this formula is valid.
 java.lang.String toString()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

name

private java.lang.String name
The identifier (name) of this variable.


primed

private boolean primed
Tells whether the variable is primed or not.

Constructor Detail

Variable

public Variable(java.lang.String name,
                boolean primed)
Constructs a variable.

Parameters:
name - the identifier (name) of the variable
primed - indicates whether the variable is primed or not
Method Detail

isTemporalFormula

public boolean isTemporalFormula()
Checks whether the formula is a temporal formula. A formula is a temporal formula, if it does not contain primed variables (the formula my contain temporal operators, but it need not).

Overrides:
isTemporalFormula in class Formula
Returns:
true if the formula is a temporal formula; false otherwise

isStepFormula

public boolean isStepFormula()
Checks whether the formula is a step formula. A formula is a step formula, if it does not contain temporal operators. This is always true for variables.

Overrides:
isStepFormula in class Formula
Returns:
true

isStateFormula

public boolean isStateFormula()
Checks whether the formula is a state formula. A formula is a state formula, if it contains neither temporal operators nor primed variables.

Overrides:
isStateFormula in class Formula
Returns:
true if the formula is a state formula; false otherwise

toROBDD

public ROBDD toROBDD(Context context)
Returns the ROBDD that represents the set of all states in which this formula is valid. For a variable, this is a quite simple ROBDD that consists of one internal node and is obtained from the method createVariable of class ROBDDs.

Specified by:
toROBDD in class Formula
Parameters:
context - the context, in which the ROBDD should be generated
Returns:
the ROBDD

toROBDD

public ROBDD toROBDD(Model model)
Returns the ROBDD that represents the set of all states in which this formula is valid. For a variable, this is a quite simple ROBDD that consists of one internal node and is obtained from the method createVariable of class ROBDDs.

Specified by:
toROBDD in class Formula
Parameters:
model - the model (only its context is relevant)
Returns:
the ROBDD

addChangedVariables

public void addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. Note that the unprimed versions are added to the change set.

Specified by:
addChangedVariables in class Formula
Parameters:
changeset - the changeset

toString

public java.lang.String toString()
Overrides:
toString in class java.lang.Object