uk.ac.man.cs.rainbow.wvmc
Interface StateEngine.Engine

All Superinterfaces:

Remote

All Known Implementing Classes:

ModelCheck.Engine, Explorer

Enclosing class:

StateEngine

public static interface StateEngine.Engine

extends Remote

All state generators look like this. Or at least they do 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 depth) 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?

Method Detail

stackDepth

public int stackDepth()
               throws RemoteException

What is the current stack depth (path length)?

getPropositionDescriptor

public int getPropositionDescriptor()
                             throws RemoteException

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!

visited

public Boolean visited(int op,
                       boolean dfs)
                throws RemoteException

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

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.

getGBDepths

public int[] getGBDepths(int depth)
                  throws RemoteException

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

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.

push

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

Push the current state on the stack.

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.

pop

public StateEngine.Popped pop()
                       throws RemoteException

Pop a state off the top of the stack.

Returns:

The state we are popping into.

backtrack

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

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

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,
                                  RemoteException

Try to perform a transition.

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.