uk.ac.man.cs.rainbow.rapa.abstraction
Class Explorer

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.rapa.abstraction.Explorer

All Implemented Interfaces:

Remote, StateEngine.Engine

public class Explorer

extends Object

implements StateEngine.Engine

State-space explorer for abstract states. The printing of debugging messages to trace the search carried out by this class's instances is controlled by the boolean property rainbow.rapa.debugExplorer.

Constructor Summary

Explorer(Abstractor abs)
Create a new state-space explorer without propositions.

Explorer(Abstractor abs, String[] propositions)
Create a new state-space explorer.

Method Summary

StateEngine.Popped	backtrack(Boolean value) Backtrack from the current state, setting its valuation as we go.
boolean	deadlock() Check the abstract state space for deadlock.
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	getExecutionCount()
int[]	getGBDepths(int depth) Obtain the good and bad depth parameters from the state at the given stack depth.
Introspector	getIntrospector() Get the state-introspector for this abstract system.
int	getMaximumDepth()
Transition[]	getPathTransitions()
int	getPropositionDescriptor() Get the integer describing the proposition valuation.
int	getStoreSize()
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)?
String	toString()
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, wait, wait, wait

Constructor Detail

Explorer

public Explorer(Abstractor abs,
                String[] propositions)
         throws ParseException

Create a new state-space explorer.

Parameters:

abs - The abstract state space to be checked.

propositions - The propositions over the abstract state.

Throws:

ParseException - If any of the proposition strings do not describe proper propositions.

Explorer

public Explorer(Abstractor abs)

Create a new state-space explorer without propositions.

Parameters:

abs - The abstract state space to be checked.

Method Detail

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

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

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.

getGBDepths

public int[] getGBDepths(int depth)

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.

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.

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

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

Returns:

The state we are popping into.

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)

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.

deadlock

public boolean deadlock()

Check the abstract state space for deadlock.

Returns:

True if there is a deadlock.

getIntrospector

public Introspector getIntrospector()

Get the state-introspector for this abstract system.

getStoreSize

public int getStoreSize()

getExecutionCount

public int getExecutionCount()

getMaximumDepth

public int getMaximumDepth()

getPathTransitions

public Transition[] getPathTransitions()

toString

public String toString()

Overrides:

toString in class Object