nz.ac.waikato.modeljunit
Class Model

java.lang.Object
  nz.ac.waikato.modeljunit.Model

Direct Known Subclasses:

TimedModel

public class Model
extends java.lang.Object

This class is a wrapper around a user-supplied EFSM model. It uses reflection to find all the actions and guards of the model. It allows a tester class (see Tester and its subclasses) to check the guards, call the actions and keep track of the current state. It also provides a general listener facility that can be used to print progress messages, record model coverage metrics etc.

To use this wrapper, you write a special EFSM class (see FsmModel) that models part of the behaviour of your SUT, then pass an instance of that class to the constructor of this class. Then you can pass an instance of this class to one of the Tester subclasses, such as RandomTester, in order to generate/execute test sequences. However, many of those classes provide a convenience constructor that creates this Model wrapper for you.

TODO: cache the guard evaluations? This would give a small efficiency gain and would avoid calling the listeners several times for the same guard.

Field Summary

protected java.util.ArrayList<java.lang.reflect.Method>	fsmActions_ All the @Action methods of fsmClass_.
protected FsmModel	fsmModel_ The implementation under test (null means none yet).
protected java.util.ArrayList<Transition>	fsmSequence_ Current test sequence TODO: decide whether this needs to be builtin or a listener.
protected java.lang.Object	fsmState_ The current state of the implementation under test.
protected java.io.Writer	output_ Output device used for messages and warnings.
protected static java.lang.Object[]	VOID_ARGS An empty array of objects.

Constructor Summary

Model(FsmModel model)
Constructs an EFSM model from the given FsmModel object.

Method Summary

ModelListener	addListener(ModelListener listen) Add a listener.
ModelListener	addListener(java.lang.String name) Add one of the predefined model listeners or coverage metrics.
boolean	doAction(int index) Try to take the given Action from the current state.
void	doReset() Reset the FSM to its initial state.
void	doReset(java.lang.String reason) Reset the FSM to its initial state.
int	enabled(int index) Is Action number 'index' enabled? Returns 0 if Action number 'index' is disabled, or a positive number if it is enabled.
java.util.BitSet	enabledGuards() Return a fresh BitSet of all actions that are enabled in the current state.
java.lang.String	getActionName(int index) Returns the name of the given Action.
int	getActionNumber(java.lang.String name) Looks up an Action by name and returns its number.
java.lang.Object	getCurrentState() Returns the current state of the implementation under test.
GraphListener	getGraphListener() Get the GraphListener for this model.
ModelListener	getListener(java.lang.String name) Get a listener by name, or null if that name is unused.
java.util.Set<java.lang.String>	getListenerNames() The set of names of all the current coverage metrics and listeners
java.lang.Object	getModel() Returns the model object that is begin tested.
java.lang.Class	getModelClass() Returns the FSM class that is the test model.
java.lang.String	getModelName() Returns the name of the FSM class that is the test model.
int	getNumActions() The total number of Actions.
java.io.Writer	getOutput() The current output stream, which is used for messages and warnings.
boolean	getTesting() True means we are generating real tests.
static java.lang.String	getVersion() The version of ModelJUnit
boolean	isEnabled(int index) Is Action number 'index' enabled? Returns true if Action number 'index' is enabled.
boolean	isInitialState() True iff the current state is the initial state.
boolean	isTerminal() True iff the current state is a terminal state.
protected void	loadModelClass(java.lang.Class fsm) Loads the given class and finds its @Action methods.
void	notifyDoneGuard(java.lang.Object state, int action, boolean enabled, int value) Sends a doneGuard event to all listeners
void	notifyDoneReset(java.lang.String reason, boolean testing) Sends a doneReset event to all listeners
void	notifyDoneTransition(int action, Transition tr) Sends a doneTransition event to all listeners
void	notifyFailure(TestFailureException ex) Sends a failure event to all listeners.
void	notifyStartAction(java.lang.Object state, int action, java.lang.String name) Sends a startAction event to all listeners
void	printMessage(java.lang.String msg) Print a message to the current output writer (see getOutput()).
void	printWarning(java.lang.String msg) Prints a warning message to the current output writer.
void	removeAllListeners() Remove all coverage listeners.
ModelListener	removeListener(java.lang.String name) Remove a coverage listener by name.
java.io.Writer	setOutput(java.io.Writer output) Sets the current output stream.
boolean	setTesting(boolean testing) Sets the testing flag.

Methods inherited from class java.lang.Object

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

Field Detail

fsmModel_

protected FsmModel fsmModel_

The implementation under test (null means none yet).

fsmActions_

protected java.util.ArrayList<java.lang.reflect.Method> fsmActions_

All the @Action methods of fsmClass_.

fsmState_

protected java.lang.Object fsmState_

The current state of the implementation under test.

fsmSequence_

protected java.util.ArrayList<Transition> fsmSequence_

Current test sequence TODO: decide whether this needs to be builtin or a listener.

VOID_ARGS

protected static final java.lang.Object[] VOID_ARGS

An empty array of objects.

output_

protected java.io.Writer output_

Output device used for messages and warnings.

Constructor Detail

Model

public Model(FsmModel model)

Constructs an EFSM model from the given FsmModel object.

Parameters:

model -

Method Detail

getVersion

public static final java.lang.String getVersion()

The version of ModelJUnit

getActionNumber

public int getActionNumber(java.lang.String name)

Looks up an Action by name and returns its number. The resulting number can be used to execute an action (see doAction(int)) or to check the guard of the action (see isEnabled(int)).

Parameters:

name - The name of an Action.

Returns:

The number of the action (>= 0), else -1.

getModelClass

public java.lang.Class getModelClass()

Returns the FSM class that is the test model.

getModelName

public java.lang.String getModelName()

Returns the name of the FSM class that is the test model.

getModel

public java.lang.Object getModel()

Returns the model object that is begin tested.

getCurrentState

public java.lang.Object getCurrentState()

Returns the current state of the implementation under test.

getActionName

public java.lang.String getActionName(int index)

Returns the name of the given Action.

getNumActions

public int getNumActions()

The total number of Actions.

getTesting

public boolean getTesting()

True means we are generating real tests. False means we are just exploring the model, so the FsmModel does not really need to connect to the SUT. This flag is passed to each reset of the FsmModel.

setTesting

public boolean setTesting(boolean testing)

Sets the testing flag. Returns its previous value.

getOutput

public java.io.Writer getOutput()

The current output stream, which is used for messages and warnings.

setOutput

public java.io.Writer setOutput(java.io.Writer output)

Sets the current output stream.

Parameters:

output -

Returns:

the old output stream

loadModelClass

protected void loadModelClass(java.lang.Class fsm)

Loads the given class and finds its @Action methods. This method must be called before any fsm traversals are done.

doReset

public void doReset()

Reset the FSM to its initial state. This is equivalent to doReset("User",testing), because it corresponds to a user-requested reset.

doReset

public void doReset(java.lang.String reason)

Reset the FSM to its initial state. This also calls the doneReset(reason, testing) method of all the listeners. TODO: enhance it so that it gives no-guards-enabled and guards-not-deterministic warnings in the initial state.

Parameters:

reason - Why the reset was performed (an adjective).

isInitialState

public boolean isInitialState()

True iff the current state is the initial state. (Note that the result is false before the first reset, since the initial and current state are unknown until then).

Returns:

true if current state is the initial state.

isEnabled

public boolean isEnabled(int index)

Is Action number 'index' enabled? Returns true if Action number 'index' is enabled. That is, if enabled(index) > 0.

enabled

public int enabled(int index)

Is Action number 'index' enabled? Returns 0 if Action number 'index' is disabled, or a positive number if it is enabled. Missing guard methods return 1, while boolean guard methods return 1 when true and 0 when false.

Parameters:

index - Index into the fsmActions_ array.

Returns:

The `enabledness' of this Action.

enabledGuards

public java.util.BitSet enabledGuards()

Return a fresh BitSet of all actions that are enabled in the current state. Callers are free to mutate the result.

isTerminal

public boolean isTerminal()

True iff the current state is a terminal state. That is, if there are no transitions out of it. Note that the terminal status of a given state may depend upon the path taken to reach that state, so on one run a state may be terminal, whereas on another run it may not be.

Returns:

true iff getCurrentState() is a terminal state.

doAction

public boolean doAction(int index)

Try to take the given Action from the current state. Returns true if the Action was taken, false if it was disabled.

Parameters:

index - Index into the fsmTransitions array.

Returns:

True if taken, false if it is disabled.

addListener

public ModelListener addListener(ModelListener listen)

Add a listener. The listener name is used to identify it and retrieve it. If a listener by the same name is already present, then this new listener will be ignored. This means that if you add the same listener multiple times, the first instance is the one that will continue to be used. (So you get more of the graph or coverage statistics recorded).

Returns:

The listener that will be used.

addListener

public ModelListener addListener(java.lang.String name)

Add one of the predefined model listeners or coverage metrics. For example, if name is "transition coverage", then a TransitionCoverage metric will be added to this model, and returned. However, if this model already has a listener by this name, then that listener will be returned and no new listener will be added.

Parameters:

name - The informal lowercase name of a Listener object.

Returns:

The listener that will actually be used.

Throws:

java.lang.RuntimeException - if name is not a known kind of listener.

removeListener

public ModelListener removeListener(java.lang.String name)

Remove a coverage listener by name.

Returns:

the ModelListener that was removed (null if it was not present).

removeAllListeners

public void removeAllListeners()

Remove all coverage listeners.

getGraphListener

public GraphListener getGraphListener()

Get the GraphListener for this model. This is equivalent to getListener("graph"), with a cast of the resulting listener to a GraphListener.

Returns:

null if this model has no graph listener.

getListener

public ModelListener getListener(java.lang.String name)

Get a listener by name, or null if that name is unused.

Parameters:

name - The name of a listener.

Returns:

null if name is not mapped to any listener.

getListenerNames

public java.util.Set<java.lang.String> getListenerNames()

The set of names of all the current coverage metrics and listeners

notifyDoneReset

public void notifyDoneReset(java.lang.String reason,
                            boolean testing)

Sends a doneReset event to all listeners

notifyDoneGuard

public void notifyDoneGuard(java.lang.Object state,
                            int action,
                            boolean enabled,
                            int value)

Sends a doneGuard event to all listeners

notifyStartAction

public void notifyStartAction(java.lang.Object state,
                              int action,
                              java.lang.String name)

Sends a startAction event to all listeners

notifyDoneTransition

public void notifyDoneTransition(int action,
                                 Transition tr)

Sends a doneTransition event to all listeners

notifyFailure

public void notifyFailure(TestFailureException ex)

Sends a failure event to all listeners. If one or more listeners throw a TestFailureException, then this method throws that exception, after all listeners have been informed of the failure.

Throws:

TestFailureException - if a listener throws it.

printWarning

public void printWarning(java.lang.String msg)

Prints a warning message to the current output writer.

printMessage

public void printMessage(java.lang.String msg)

Print a message to the current output writer (see getOutput()). This automatically adds a newline on the end of msg. It does a flush after each call, so that messages appear promptly.