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

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.wvmc.AutomataBuilder

All Implemented Interfaces:

Constants

public class AutomataBuilder

extends Object

implements Constants

Buchi-automata construction site. You're never going to get an instance of this class (it is completely encapsulated within the code that uses it, so it exists primarily for documentation only...

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

Method Summary

Formula	buildWholeTable(Formula f, boolean inBuchi)
Formula	checkPropList(int realIdx, boolean isNot)
boolean	getDualFlag()
int	getPropCount()
protected void	initSpec()
Formula	makeAndOr(int op, Formula l, Formula r)
Formula	makeTLNode(int op, Formula f)
Formula	makeTLNode(int op, Formula l, Formula r)
void	outputLatexFromCTL(String name, Formula f, Formula originalF, int props)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

getDualFlag

public boolean getDualFlag()

outputLatexFromCTL

public void outputLatexFromCTL(String name,
                               Formula f,
                               Formula originalF,
                               int props)
                        throws IOException

buildWholeTable

public Formula buildWholeTable(Formula f,
                               boolean inBuchi)

makeTLNode

public Formula makeTLNode(int op,
                          Formula l,
                          Formula r)

makeTLNode

public Formula makeTLNode(int op,
                          Formula f)

makeAndOr

public Formula makeAndOr(int op,
                         Formula l,
                         Formula r)

getPropCount

public int getPropCount()

initSpec

protected void initSpec()

checkPropList

public Formula checkPropList(int realIdx,
                             boolean isNot)