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

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

All Implemented Interfaces:

Remote, StateEngine.Engine

Enclosing class:

ModelCheck

public class ModelCheck.Engine

extends Object

implements StateEngine.Engine

The view presented to the model-checker.

Method Summary

StateEngine.Popped	backtrack(Boolean value) Backtrack from the current state, setting its valuation as we go.
StateEngine.Execed	execute(boolean reset, int op, int quant, int gb, boolean ctl, int bad, int good, boolean dfs) Try to perform a transition.
int[]	getGBDepths(int index) Obtain the good and bad depth parameters from the state at the given stack depth.
int	getPropositionDescriptor() Get the integer describing the proposition valuation.
StateEngine.Popped	pop() Pop a state off the top of the stack.
void	push(int op, int quant, int gb, boolean ctl, int bad, int good, boolean dfs) Push the current state on the stack.
int	stackDepth() What is the current stack depth (path length)?
Boolean	visited(int op, boolean dfs) Have we seen the current state before, and if so, what was its valuation?

Methods inherited from class java.lang.Object

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

Method Detail

backtrack

public StateEngine.Popped backtrack(Boolean value)
                             throws StateEngine.CannotBacktrack

Description copied from interface: StateEngine.Engine

Backtrack from the current state, setting its valuation as we go.

Specified by:

backtrack in interface StateEngine.Engine

Following copied from interface: uk.ac.man.cs.rainbow.wvmc.StateEngine.Engine

Parameters:

value - The valuation for the state we are backtracking out of.

Returns:

The state we are backtracking into.

Throws:

CannotBacktrack - If the stack is empty.

execute

public StateEngine.Execed execute(boolean reset,
                                  int op,
                                  int quant,
                                  int gb,
                                  boolean ctl,
                                  int bad,
                                  int good,
                                  boolean dfs)
                           throws RainbowException

Description copied from interface: StateEngine.Engine

Try to perform a transition.

Specified by:

execute in interface StateEngine.Engine

Following copied from interface: uk.ac.man.cs.rainbow.wvmc.StateEngine.Engine

Parameters:

reset - Can't remember what this does right now... :^)

op - The current temporal operator. States are only equal when their corresponding temporal operators are equal too.

quant - The current path quantifier. Does not affect state equality.

gb - The good loop/bad loop flag. Does not affect state equality.

ctl - The CTL-style formula flag. Does not affect state equality.

bad - The bad loop depth indicator. Does not affect state equality.

good - The good loop depth indicator. Does not affect state equality.

dfs - Whether the second (depth first) search is happening. States are only equal when this flag is equal too.

Returns:

A value indicating whether another transition was possible from the current state, and if so, whether the state the transition leads to has been seen before (on the path or otherwise) or whether it is completely new.

Throws:

RainbowException - If the state generator fails somehow. An example of the sort of problem that might be reported through this mechanism is an unchecked division by zero or a bizarre state mismatch.

getGBDepths

public int[] getGBDepths(int index)

Description copied from interface: StateEngine.Engine

Obtain the good and bad depth parameters from the state at the given stack depth.

Specified by:

getGBDepths in interface StateEngine.Engine

Following copied from interface: uk.ac.man.cs.rainbow.wvmc.StateEngine.Engine

Parameters:

depth - What depth on the stack should the depth parameters be read from.

Returns:

An array with (at least) two elements, the first of which is the new bad depth, and the second of which is the new good depth.

getPropositionDescriptor

public int getPropositionDescriptor()

Description copied from interface: StateEngine.Engine

Get the integer describing the proposition valuation. Note that this means you are limited to at most 32 propositions, but this turns out not to be a problem in practise!

Specified by:

getPropositionDescriptor in interface StateEngine.Engine

pop

public StateEngine.Popped pop()

Description copied from interface: StateEngine.Engine

Pop a state off the top of the stack.

Specified by:

pop in interface StateEngine.Engine

Throws:

RainbowError - If there isn't a state to pop back into - this should never happen in an uncontrolled fashion!

push

public void push(int op,
                 int quant,
                 int gb,
                 boolean ctl,
                 int bad,
                 int good,
                 boolean dfs)

Description copied from interface: StateEngine.Engine

Push the current state on the stack.

Specified by:

push in interface StateEngine.Engine

Following copied from interface: uk.ac.man.cs.rainbow.wvmc.StateEngine.Engine

Parameters:

op - The current temporal operator. States are only equal when their corresponding temporal operators are equal too.

quant - The current path quantifier. Does not affect state equality.

gb - The good loop/bad loop flag. Does not affect state equality.

ctl - The CTL-style formula flag. Does not affect state equality.

bad - The bad loop depth indicator. Does not affect state equality.

good - The good loop depth indicator. Does not affect state equality.

dfs - Whether the second (depth first) search is happening. States are only equal when this flag is equal too.

stackDepth

public int stackDepth()

Description copied from interface: StateEngine.Engine

What is the current stack depth (path length)?

Specified by:

stackDepth in interface StateEngine.Engine

visited

public Boolean visited(int op,
                       boolean dfs)

Description copied from interface: StateEngine.Engine

Have we seen the current state before, and if so, what was its valuation?

Specified by:

visited in interface StateEngine.Engine

Following copied from interface: uk.ac.man.cs.rainbow.wvmc.StateEngine.Engine

Parameters:

op - The current temporal operator. States are only equal when their corresponding temporal operators are equal too.

dfs - Whether the second (depth first) search is happening. States are only equal when this flag is equal too.

Returns:

null if the state has never been seen before, and a Boolean object otherwise.