uk.ac.man.cs.rainbow.wvmc
Class Formula

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.wvmc.Formula
All Implemented Interfaces:
Cloneable, Constants

public class Formula
extends Object
implements Constants, Cloneable

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

FALSE

public static final Formula FALSE
Boolean falsehood.

TRUE

public static final Formula TRUE
Boolean truth.
Constructor Detail

Formula

protected Formula()
Use the subclasses or constants instead. This is only visible for subclassing purposes.
See Also:
FALSE, TRUE
Method Detail

init

protected void init()
Initialise the fields of the class to known (blank) values.

isBoolean

public final boolean isBoolean()
Is the formula a literal true or false?

isTrue

public final boolean isTrue()
Is the formula a literal true?

getBoolean

public static Formula getBoolean(boolean bval)
Convert a Java boolean into a CTL* boolean.

getBoolean

public static Formula getBoolean(Boolean bval)
Convert a Java Boolean object into a CTL* boolean.

prtTL

public String prtTL()
Render the formula operator.

prtTL

public static String prtTL(Formula f)
Render a formula's operator.
Parameters:
f - The formula whose operator is to be rendered.

toString

public String toString()
Render the formula operator.
Overrides:
toString in class Object

isLeaf

public boolean isLeaf()
Is this formula a leaf-formula? Leaf formulas are either boolean true/false or a proposition.

setIndexValue

public void setIndexValue(Formula index)

getLeft

public Formula getLeft()
                throws WVMCException
Get the left subexpression.

getRight

public Formula getRight()
                 throws WVMCException
Get the right subexpression.

getLQuant

public int getLQuant()
              throws WVMCException
Get the left quantifier.

getRQuant

public int getRQuant()
              throws WVMCException
Get the right quantifier.

getQi

protected int getQi()
Get the "weight" of the formula. Used as part of a heuristic to try to make sensible counterexamples be generated before more complex ones.

clone

public Object clone()
Anyone is allowed to clone CTL* formulas.
Overrides:
clone in class Object