|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object | +--uk.ac.man.cs.rainbow.wvmc.Formula
A CTL* formula fragment.
Field Summary | |
static Formula |
FALSE
Boolean falsehood. |
static Formula |
TRUE
Boolean truth. |
Fields inherited from interface uk.ac.man.cs.rainbow.wvmc.Constants |
A, AND, AU, AV, AX, BAD_LOOP, E, EU, EV, EX, Existential, Expand, False, GOOD_LOOP, LOOP_STATE, MAX_BUCHI_TABLE, MAX_TABLE, NEW_STATE, NO_MORE_SUCCS, NOT_LOOP, NUMOPS, OLD_STATE, opToName, OR, q_0, q_1, q_10, q_11, q_12, q_13, q_14, q_15, q_2, q_3, q_4, q_5, q_6, q_7, q_8, q_9, quantToName, True, U, Universal, V, X |
Constructor Summary | |
protected |
Formula()
Use the subclasses or constants instead. |
Method Summary | |
Object |
clone()
Anyone is allowed to clone CTL* formulas. |
static Formula |
getBoolean(boolean bval)
Convert a Java boolean into a CTL* boolean. |
static Formula |
getBoolean(Boolean bval)
Convert a Java Boolean object into a CTL* boolean. |
Formula |
getLeft()
Get the left subexpression. |
int |
getLQuant()
Get the left quantifier. |
protected int |
getQi()
Get the "weight" of the formula. |
Formula |
getRight()
Get the right subexpression. |
int |
getRQuant()
Get the right quantifier. |
protected void |
init()
Initialise the fields of the class to known (blank) values. |
boolean |
isBoolean()
Is the formula a literal true or false? |
boolean |
isLeaf()
Is this formula a leaf-formula? Leaf formulas are either boolean true/false or a proposition. |
boolean |
isTrue()
Is the formula a literal true? |
String |
prtTL()
Render the formula operator. |
static String |
prtTL(Formula f)
Render a formula's operator. |
void |
setIndexValue(Formula index)
|
String |
toString()
Render the formula operator. |
Methods inherited from class java.lang.Object |
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
public static final Formula FALSE
public static final Formula TRUE
Constructor Detail |
protected Formula()
FALSE
,
TRUE
Method Detail |
protected void init()
public final boolean isBoolean()
public final boolean isTrue()
public static Formula getBoolean(boolean bval)
public static Formula getBoolean(Boolean bval)
public String prtTL()
public static String prtTL(Formula f)
f
- The formula whose operator is to be rendered.public String toString()
toString
in class Object
public boolean isLeaf()
public void setIndexValue(Formula index)
public Formula getLeft() throws WVMCException
public Formula getRight() throws WVMCException
public int getLQuant() throws WVMCException
public int getRQuant() throws WVMCException
protected int getQi()
public Object clone()
clone
in class Object
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |