de.upb.swt.mcie.formulas
Class Constant

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

public class Constant
extends Formula

Implements a constants, which can be true or false. This is one of the leaf nodes of a formula. Its value is either 0 or 1. Currently, it is possible to instantiate a constant with other values; but it is forbidden anyway.

Author:
Ekkart Kindler, kindler@upb.de
See Also:
TerminalNode

Field Summary
private  int value
          The value of the constant.
 
Fields inherited from class de.upb.swt.mcie.formulas.Formula
step, temporal
 
Constructor Summary
Constant(int value)
          Constructs a constant with the provided value.
 
Method Summary
 void addChangedVariables(ChangeSet changeset)
          Adds all variables that occur primed within the formula to the given change set.
 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 de.upb.swt.mcie.formulas.Formula
isStateFormula, isStepFormula, isTemporalFormula
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

value

private int value
The value of the constant. It should be 0 or 1. Other values are forbidden.

Constructor Detail

Constant

public Constant(int value)
Constructs a constant with the provided value.

Parameters:
value - the value of the constant; it should be 0 or 1
Method Detail

toROBDD

public ROBDD toROBDD(Context context)
Returns the ROBDD that represents the set of all states in which this formula is valid. Either way it is a terminal node (low or high).

Specified by:
toROBDD in class Formula
Parameters:
context - the context
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. Either way it is a terminal node (low or high).

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