|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.formulas.Formula
de.upb.swt.mcie.formulas.BinaryOp
public class BinaryOp
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!
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 |
---|
public static final int AND
public static final int OR
public static final int IMP
public static final int EQU
public static final int EU
public static final int AU
public static final int ER
public static final int AR
private static final boolean[] temporalOp
private static final int[] binding
public static final int MAXBINDING
private int op
private Formula left
private Formula right
private static final java.lang.String[] representation
Constructor Detail |
---|
public BinaryOp(int op, Formula f1, Formula f2)
op
- the operationf1
- the left subformulaf2
- the right subformulaMethod Detail |
---|
public static int binding(int op)
op
- the operation
binding
public ROBDD toROBDD(Context context)
toROBDD(Context)
.
toROBDD
in class Formula
context
- the context in which the formula is evaluated
to an ROBDD
IncorrectUseException
- if formula contains temporal
operators or unknown operators are encountered in
the formulapublic ROBDD toROBDD(Model model)
toROBDD(Context)
.
toROBDD
in class Formula
model
- the Kripke structure
IncorrectUseException
- if unknown operators are
encountered in the formulapublic void addChangedVariables(ChangeSet changeset)
addChangedVariables
in class Formula
changeset
- the changesetpublic java.lang.String toString()
toString
in class java.lang.Object
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |