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

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

All Implemented Interfaces:

Constants

public class Checker

extends Object

implements Constants

The model checker. Creating an instance of this class produces a model checker for a particular CTL* formula, which can then be checked over a state space represented by a particular state generation engine.

Field Summary

static int	CTL_STAR_NNF Used to indicate that the parser should treat the input string as CTL* in negation normal form.
static int	LTL Used to indicate that the parser should treat the input string as LTL.

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

Checker(String formula, int language)
Create a new model checker.

Method Summary

boolean	check(StateEngine.Engine engine) Check the temporal model against a state generator.
static void	main(String[] args) Basic test code.
String	render(int operator) Convert an operator index into its string form.

Methods inherited from class java.lang.Object

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

Field Detail

CTL_STAR_NNF

public static final int CTL_STAR_NNF

Used to indicate that the parser should treat the input string as CTL* in negation normal form.

See Also:

SpecParse.parse(AutomataBuilder,String)

LTL

public static final int LTL

Used to indicate that the parser should treat the input string as LTL.

See Also:

SpecParse.parseLTL(AutomataBuilder,String)

Constructor Detail

Checker

public Checker(String formula,
               int language)
        throws ParseException,
               WVMCException

Create a new model checker.

Parameters:

formula - The formula to check.

language - What language is the formula expressed in?

Throws:

ParseException - If the input string is not a valid formula.

WVMCException - If the state graph is too large.

See Also:

AutomataBuilder, Examiner, Formula, TemporalModel, CTL_STAR_NNF, LTL

Method Detail

check

public boolean check(StateEngine.Engine engine)
              throws WVMCException,
                     RainbowException,
                     RemoteException

Check the temporal model against a state generator.

Parameters:

engine - The state generation engine to check against.

Throws:

WVMCException - When an unexpected internal error happens.

RainbowException - If the state generator fails.

See Also:

Formula, TemporalModel

render

public String render(int operator)

Convert an operator index into its string form.

Parameters:

operator - The index into the internal table of graph nodes.

Returns:

A string representation of the graph node in question.

main

public static void main(String[] args)
                 throws Exception

Basic test code.