uk.ac.man.cs.rainbow.deadlock
Class ModelCheck

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.deadlock.ModelCheck

public class ModelCheck

extends Object

Checks a transition system against a CTL* formula. The transition system is based on a state machine (defined by RASM) that produces states on the fly. The CTL* formula is compiled into an automaton and traversed by WVMC.

See Also:

StateEnumerator, Checker

Inner Class Summary

class	ModelCheck.AutoState The state of the model checker automata.
class	ModelCheck.Engine The view presented to the model-checker.
static interface	ModelCheck.Evaluator Provides a proposition evaluation service to the model checker.
class	ModelCheck.Major The major state of the model checker.
class	ModelCheck.Minor The minor state of the model checker.

Constructor Summary

ModelCheck(StateEnumerator enumerator, String formula)
Create a system that can check a system against a CTL* formula.

Method Summary

boolean	checkModel() Check the state engine against the temporal formula.
ModelCheck.AutoState	getAutomataState(int index) Get the state of the model checker at the given step.
ModelCheck.Evaluator	getEvaluator() What proposition evaluator is the model checker using?
int	getLastLoopDepth() At what depth was the last loop?
StateEngine	getResultingStateEngine() Get the state of the state explorer on check completion.
String	opString(ModelCheck.AutoState a) Render the given major state as a string.
void	setEvaluator(ModelCheck.Evaluator propEval) Set the proposition evaluator for this model checker.

Methods inherited from class java.lang.Object

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

Constructor Detail

ModelCheck

public ModelCheck(StateEnumerator enumerator,
                  String formula)
           throws RainbowException,
                  ParseException

Create a system that can check a system against a CTL* formula.

Parameters:

enumerator - The system (expressed as a state-space enumerator) to check the formula against.

formula - A CTL* formula in negation-normal form.

Throws:

RainbowException - If the system fails to initialise the internal state engine.

ParseException - If the formula parameter does not describe a CTL* formula in negation-normal form.

Method Detail

checkModel

public boolean checkModel()
                   throws WVMCException,
                          RainbowException

Check the state engine against the temporal formula.

Throws:

WVMCException - If the model check fails somehow.

RainbowException - If the state engine fails somehow.

opString

public String opString(ModelCheck.AutoState a)

Render the given major state as a string. Note that this does more than just return the value of the operator in question.

See Also:

Checker.render(int)

getLastLoopDepth

public int getLastLoopDepth()

At what depth was the last loop?

Returns:

The depth of the last loop, or -1 if the last execute action did not result in a loop.

getResultingStateEngine

public StateEngine getResultingStateEngine()

Get the state of the state explorer on check completion.

Returns:

If the model check has completed, this returns the state engine that the system finished up with. Returns null otherwise.

getAutomataState

public ModelCheck.AutoState getAutomataState(int index)

Get the state of the model checker at the given step.

Parameters:

index - Which step to get the state from.

Throws:

NullPointerException - If the index is out of range.

setEvaluator

public void setEvaluator(ModelCheck.Evaluator propEval)

Set the proposition evaluator for this model checker.

getEvaluator

public ModelCheck.Evaluator getEvaluator()

What proposition evaluator is the model checker using?