|
||||||||||
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.UnaryOp
public class UnaryOp
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.
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 |
---|
public static final int NOT
public static final int EX
public static final int AX
public static final int EG
public static final int AG
public static final int EF
public static final int AF
private static final boolean[] temporalOp
private static final int[] binding
public static final int MAXBINDING
private int op
private Formula f
private static final java.lang.String[] representation
Constructor Detail |
---|
public UnaryOp(int op, Formula f)
op
- the code of the operationf
- the subformulaMethod Detail |
---|
public static int binding(int op)
op
- the operation
binding
public ROBDD toROBDD(Context context)
toROBDD
in class Formula
context
- the context
IncorrectUseException
- if formula contains temporal
operators or unknown operators are encountered in
the formulapublic ROBDD toROBDD(Model model)
toROBDD
in class Formula
model
- the model
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 |