de.upb.swt.mcie.formulas
Class UnaryOp

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

public class UnaryOp
extends Formula

Implements the unary operation in a formula. It consists of an operation (resp. its code) and a reference to the subformula. The codes for the different operators are defined as constants in this class. Moreover, there is an array defining for each operator, whether it is a temporal operator or not, and there is an array defining the binding priorities for the different operators.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
static int AF
          Code for the CTL operator EF.
static int AG
          Code for the CTL operator AG.
static int AX
          Code for the CTL operator AX.
private static int[] binding
          Table that defines the binding priority of each operator.
static int EF
          Code for the CTL operator EF.
static int EG
          Code for the CTL operator EG.
static int EX
          Code for the CTL operator EX.
private  Formula f
          The subformula.
static int MAXBINDING
          The maximum binding level of all unary operations.
static int NOT
          Code for the negation operator.
private  int op
          The code of the operation.
private static java.lang.String[] representation
          String representation of the different operators.
private static boolean[] temporalOp
          Table that defines for each operator whether it is a temporal operator or not.
 
Fields inherited from class de.upb.swt.mcie.formulas.Formula
step, temporal
 
Constructor Summary
UnaryOp(int op, Formula f)
          Constructs a unary operation from the code of the operation and its subformula.
 
Method Summary
 void addChangedVariables(ChangeSet changeset)
          Adds all variables that occur primed within the formula to the given change set.
static int binding(int op)
          Returns the binding level of this operation.
 ROBDD toROBDD(Context context)
          Returns the ROBDD representation of the set of all states satisfying the formula.
 ROBDD toROBDD(Model model)
          Returns the ROBDD representation of the set of all states satisfying the formula.
 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

NOT

public static final int NOT
Code for the negation operator.

See Also:
Constant Field Values

EX

public static final int EX
Code for the CTL operator EX.

See Also:
Constant Field Values

AX

public static final int AX
Code for the CTL operator AX.

See Also:
Constant Field Values

EG

public static final int EG
Code for the CTL operator EG.

See Also:
Constant Field Values

AG

public static final int AG
Code for the CTL operator AG.

See Also:
Constant Field Values

EF

public static final int EF
Code for the CTL operator EF.

See Also:
Constant Field Values

AF

public static final int AF
Code for the CTL operator EF.

See Also:
Constant Field Values

temporalOp

private static final boolean[] temporalOp
Table that defines for each operator whether it is a temporal operator or not.


binding

private static final int[] binding
Table that defines the binding priority of each operator. Lowest value means highest binding priority. Currently, all unary operators have binding level 0, i.e. unary operators have higher binding priority than all binary operators. In principle, unary operators can have a binding priority that is lower than that of a binary operation. But, this results in quite unusual bindings. So, this should be avoided. Negative binding priorities are not allowed.


MAXBINDING

public static final int MAXBINDING
The maximum binding level of all unary operations. The parser needs to know the maximum for proper operation; this should be the maximum of the values given above.

See Also:
Constant Field Values

op

private int op
The code of the operation.


f

private Formula f
The subformula.


representation

private static final java.lang.String[] representation
String representation of the different operators.

Constructor Detail

UnaryOp

public UnaryOp(int op,
               Formula f)
Constructs a unary operation from the code of the operation and its subformula.

Parameters:
op - the code of the operation
f - the subformula
Method Detail

binding

public static int binding(int op)
Returns the binding level of this operation.

Parameters:
op - the operation
Returns:
its binding level
See Also:
binding

toROBDD

public ROBDD toROBDD(Context context)
Returns the ROBDD representation of the set of all states satisfying the formula. The formula must be a step formula, because temporal formulas cannot be interpreted in a context only.

Specified by:
toROBDD in class Formula
Parameters:
context - the context
Returns:
the ROBDD representing the set of states
Throws:
IncorrectUseException - if formula contains temporal operators or unknown operators are encountered in the formula

toROBDD

public ROBDD toROBDD(Model model)
Returns the ROBDD representation of the set of all states satisfying the formula. Temporal operators are interpreted in the Kripke structure.

Specified by:
toROBDD in class Formula
Parameters:
model - the model
Returns:
the ROBDD representing the set of states
Throws:
IncorrectUseException - if unknown operators are encountered in the formula

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