|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |