de.upb.swt.mcie.formulas
Class Formula

java.lang.Object
  extended by de.upb.swt.mcie.formulas.Formula
Direct Known Subclasses:
BinaryOp, Constant, UnaryOp, Variable

public abstract class Formula
extends java.lang.Object

Implements the common structure of all formulas. In particular, it provides methods for checking whether it is a state formula, a transition formula or a temporal formula.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
protected  boolean step
          Flag indication that the formula contains primed variables.
protected  boolean temporal
          Flag indicating that the formula contains temporal operators.
 
Constructor Summary
Formula()
           
 
Method Summary
abstract  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.
abstract  ROBDD toROBDD(Context context)
          Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula.
abstract  ROBDD toROBDD(Model model)
          Returns the ROBDD representation of the set of all states satisfying the formula.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

temporal

protected boolean temporal
Flag indicating that the formula contains temporal operators. Note that this does not mean that the formula is a temporal formula, because it could contain primed variables (in that case the formula is neither a state formula nor a transition formula nor a temporal formula).


step

protected boolean step
Flag indication that the formula contains primed variables. Note that this does not mean that the formula is a step formula, because it could contain temporal operators (in that case the formula is neither a state formula nor a transition formula nor a temporal formula).

Constructor Detail

Formula

public Formula()
Method Detail

toROBDD

public abstract ROBDD toROBDD(Context context)
Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula. Note that the formula must not contain temporal operators; if it does, this will result in an exception.

Parameters:
context - the context
Returns:
the ROBDD representing the set of states

toROBDD

public abstract ROBDD toROBDD(Model model)
Returns the ROBDD representation of the set of all states satisfying the formula. Temporal operators are interpreted in the model. For state formulas and transition formulas, only the context of the model is relevant. In the latter case, the result is the same as calling method toROBDD(Context).

Parameters:
model - the model
Returns:
the ROBDD representing the set of states

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).

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 (the formula my contain primed variables, but it need not).

Returns:
true if the formula is a step formula; false otherwise

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.

Returns:
true if the formula is a state formula; false otherwise

addChangedVariables

public abstract 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.

Parameters:
changeset - the changeset