de.upb.swt.mcie.formulas
Class BinaryOp

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

public class BinaryOp
extends Formula

Implements a binary operation in a formula. It consists of an operation (resp. its code) and a reference to the left and right 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.

Note that an application should never ever use the values directly for referring to an operation. Rather they should use the constants defined here!

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
static int AND
          Code for the AND operation.
static int AR
          Code for the CTL operator AR.
static int AU
          Code for the CTL operator AU.
private static int[] binding
          Table that defines the binding priority of each operator.
static int EQU
          Code for the EQUivalence operation, which is the same as EQUality.
static int ER
          Code for the CTL operator ER.
static int EU
          Code for the CTL operator EU.
static int IMP
          Code for the IMPlication operation.
private  Formula left
          The left subformula.
static int MAXBINDING
          The maximum binding level of all binary operations.
private  int op
          The code of the binary operation as defined by the constants in this class.
static int OR
          Code for the OR operation.
private static java.lang.String[] representation
          String representation of the different operators.
private  Formula right
          The right subformula.
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
BinaryOp(int op, Formula f1, Formula f2)
          Constructs a formula starting with a binary operation from the operation and its two subformulas.
 
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 respectively the set of transitions 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

AND

public static final int AND
Code for the AND operation.

See Also:
Constant Field Values

OR

public static final int OR
Code for the OR operation.

See Also:
Constant Field Values

IMP

public static final int IMP
Code for the IMPlication operation.

See Also:
Constant Field Values

EQU

public static final int EQU
Code for the EQUivalence operation, which is the same as EQUality.

See Also:
Constant Field Values

EU

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

See Also:
Constant Field Values

AU

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

See Also:
Constant Field Values

ER

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

See Also:
Constant Field Values

AR

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

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. Binding priority 0 should be left for unary operators. In principle binary operators can have binding priority 0 too. Negative binding priorities, however, are not allowed.


MAXBINDING

public static final int MAXBINDING
The maximum binding level of all binary 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 binary operation as defined by the constants in this class.


left

private Formula left
The left subformula.


right

private Formula right
The right subformula.


representation

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

Constructor Detail

BinaryOp

public BinaryOp(int op,
                Formula f1,
                Formula f2)
Constructs a formula starting with a binary operation from the operation and its two subformulas.

Parameters:
op - the operation
f1 - the left subformula
f2 - the right 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 respectively the set of transitions satisfying the formula. Temporal operators are interpreted in the Kripke structure. 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 toROBDD(Context).

Specified by:
toROBDD in class Formula
Parameters:
context - the context in which the formula is evaluated to an ROBDD
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. 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 toROBDD(Context).

Specified by:
toROBDD in class Formula
Parameters:
model - the Kripke structure
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