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

Packages that use Formula
uk.ac.man.cs.rainbow.wvmc Classes implementing a model-checker. 
uk.ac.man.cs.rainbow.wvmc.parser CTL*-NNF and LTL parsers. 
 

Uses of Formula in uk.ac.man.cs.rainbow.wvmc
 

Fields in uk.ac.man.cs.rainbow.wvmc declared as Formula
static Formula Formula.FALSE
          Boolean falsehood.
static Formula Formula.TRUE
          Boolean truth.
 

Methods in uk.ac.man.cs.rainbow.wvmc that return Formula
 Formula TemporalModel.check()
          Check whether the model and this formula-derived automaton correspond.
static Formula Formula.getBoolean(boolean bval)
          Convert a Java boolean into a CTL* boolean.
static Formula Formula.getBoolean(Boolean bval)
          Convert a Java Boolean object into a CTL* boolean.
 Formula Formula.getLeft()
          Get the left subexpression.
 Formula Formula.getRight()
          Get the right subexpression.
 Formula AutomataBuilder.buildWholeTable(Formula f, boolean inBuchi)
           
 Formula AutomataBuilder.makeTLNode(int op, Formula l, Formula r)
           
 Formula AutomataBuilder.makeTLNode(int op, Formula f)
           
 Formula AutomataBuilder.makeAndOr(int op, Formula l, Formula r)
           
 Formula AutomataBuilder.checkPropList(int realIdx, boolean isNot)
           
 Formula FormulaSet.getHead()
          The head formula of this set.
 

Methods in uk.ac.man.cs.rainbow.wvmc with parameters of type Formula
static String Formula.prtTL(Formula f)
          Render a formula's operator.
 void Formula.setIndexValue(Formula index)
           
static void Examiner.examineFormula(Formula f, int maxfs)
           
 void AutomataBuilder.outputLatexFromCTL(String name, Formula f, Formula originalF, int props)
           
 Formula AutomataBuilder.buildWholeTable(Formula f, boolean inBuchi)
           
 Formula AutomataBuilder.makeTLNode(int op, Formula l, Formula r)
           
 Formula AutomataBuilder.makeTLNode(int op, Formula f)
           
 Formula AutomataBuilder.makeAndOr(int op, Formula l, Formula r)
           
 boolean FormulaSet.present(Formula f)
          Is the given formula present in this set?
static boolean FormulaSet.present(FormulaSet set, Formula f)
          Is the given formula present in the given set?
 FormulaSet FormulaSet.add(Formula f)
          Add the given formula to this set.
static FormulaSet FormulaSet.add(FormulaSet set, Formula f)
          Add the given formula to the given set.
 

Constructors in uk.ac.man.cs.rainbow.wvmc with parameters of type Formula
FormulaSet(Formula head, FormulaSet tail)
          Create a new linked list node.
 

Uses of Formula in uk.ac.man.cs.rainbow.wvmc.parser
 

Methods in uk.ac.man.cs.rainbow.wvmc.parser that return Formula
 Formula FormPair.getFormula1()
           
 Formula FormPair.getFormula2()
           
static Formula SpecParse.parse(AutomataBuilder builder, String s)
          Parse the given string and build a formula with the given construction engine.
static Formula SpecParse.parseLTL(AutomataBuilder builder, String s)
          Parse the given string and build an LTL formula with the given construction engine.
 Formula SpecParse.Ltl()
          Parse an LTL formula, optionally followed by a ".".
 Formula SpecParse.LtlUntil(boolean negated)
          Parse an LTL formula fragment consisting of a series of fragments separated by until operators.
 Formula SpecParse.LtlWhile(boolean negated)
          Parse an LTL formula fragment consisting of a series of fragments separated by while operators.
 Formula SpecParse.LtlImplied(boolean negated)
          Parse an LTL formula fragment consisting of an optional implication between fragments.
 Formula SpecParse.LtlOr(boolean negated)
          Parse an LTL formula fragment consisting of a series of fragments separated by or operators.
 Formula SpecParse.LtlAnd(boolean negated)
          Parse an LTL formula fragment consisting of a series of fragments separated by and operators.
 Formula SpecParse.LtlMonadic(boolean negated)
          Parse an LTL formula fragment consisting of a list of monadic operators and a proposition or parenthesized formula.
 Formula SpecParse.CtlStarSpec()
          Parse a CTL* formula, optionally followed by a ".".
 Formula SpecParse.CtlSpec()
          A CTL* formula.
 Formula SpecParse.CtlComplexSpec()
          A complex CTL* formula fragment.
 Formula SpecParse.CtlUQuant(boolean isAll, Formula u)
          CTL* formula fragment.
 Formula SpecParse.CtlXQuant(boolean isAll)
          A CTL* formula with a path quantifier and a next operator in front.
 Formula SpecParse.CtlFGQuant(boolean isAll, int i)
          A CTL* formula with a path quantifier and a sometime/always operator in front.
 Formula SpecParse.CtlQuantified(boolean isAll)
          A quantified CTL* formula.
 Formula SpecParse.CtlSimpleSpec()
          Simple components of a CTL* formula.
 Formula SpecParse.CtlUNum()
          A proposition with underlines round it.
 

Methods in uk.ac.man.cs.rainbow.wvmc.parser with parameters of type Formula
 Formula SpecParse.CtlUQuant(boolean isAll, Formula u)
          CTL* formula fragment.
 

Constructors in uk.ac.man.cs.rainbow.wvmc.parser with parameters of type Formula
FormPair(Formula formula1, Formula formula2)