uk.ac.sheffield.vtts.model

Class Machine

java.lang.Object

uk.ac.sheffield.vtts.model.Element

uk.ac.sheffield.vtts.model.Named

uk.ac.sheffield.vtts.model.Annotated

uk.ac.sheffield.vtts.model.Machine

public class Machine
extends Annotated

Machine represents a named finite state Machine. A Machine is a model of a software Service that describes its reactive behaviour, in which actions are either allowed or prohibited in certain states. A Machine models this high-level behaviour as a set of States and expected Transitions linking these States. The number of States depends on the distinct modes in which different subsets of actions are to be allowed. The Transitions model the expected actions allowed in each State, including any anticipated error handling. Missing Transitions represent actions that are ignored in that State, corresponding to null operations. The name of a Machine should correspond to the name of the Service owning the Machine.

Version:

Broker@Cloud 1.0

Author:

Anthony J H Simons

Field Summary

Fields

Modifier and Type	Field and Description
static int	TIMEOUT The timeout for state-space searches, set to five seconds.

Fields inherited from class uk.ac.sheffield.vtts.model.Annotated

notice

Fields inherited from class uk.ac.sheffield.vtts.model.Named

name

Constructor Summary

Constructors

Constructor and Description
Machine() Creates a default finite state Machine.
Machine(java.lang.String name) Creates a named finite state Machine.

Method Summary

Methods

Modifier and Type	Method and Description
boolean	accept(Event event) Reports whether this Machine accepts an Event in its current State.
Machine	addState(State state) Adds a named State to the Machine.
protected Warning	checkDifference(Notice topInfo, Alphabet difference) Checks the difference between the Protocol alphabet and the Machine alphabet.
protected Warning	checkInitialState(Notice topInfo) Checks that this Machine has an initial State.
Warning	checkStateCoverage(Notice topInfo) Checks the coverage of States after simulating this Machine to find the state cover.
protected Warning	checkTargetStates(Notice topInfo) Checks that the Transitions of this Machine refer to properly-named target States.
Warning	checkTransitionCoverage(Notice topInfo) Checks the coverage of Transitions after simulating this Machine with a Language of a given maximum size.
Machine	clear() Resets every State and Transition in this Machine to its unmarked status.
boolean	fireEvent(Event event) Fires an event on this Machine.
Alphabet	getAlphabet() Returns the Alphabet of this Machine.
State	getCurrentState() Returns the current State;
State	getInitialState() Returns the initial State.
State	getState(java.lang.String name) Returns the unique State with the given name.
Language	getStateCover() Calculates the state cover for this Machine.
protected Language	getStateCover(Alphabet alphabet) Calculates the state cover for this Machine.
java.util.Set<State>	getStates() Returns the set of States belonging to this Machine.
Language	getTransitionCover(int length) Calculates the n-transition cover for this Machine.
java.util.Set<Transition>	getTransitions() Returns the set of Transitions belonging to this Machine.
Machine	reset() Resets this Machine to its initial State.
Machine	validateMachine(Protocol protocol) Validates the States and Transitions of this Machine for completeness.

Methods inherited from class uk.ac.sheffield.vtts.model.Annotated

addNotice, getNotice

Methods inherited from class uk.ac.sheffield.vtts.model.Named

equals, getName, hashCode, setName, setName, toString

Methods inherited from class uk.ac.sheffield.vtts.model.Element

safeEquals, safeHashCode, semanticError

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

TIMEOUT

public static final int TIMEOUT

The timeout for state-space searches, set to five seconds.

See Also:

Constant Field Values

Constructor Detail

Machine

public Machine()

Creates a default finite state Machine.

Machine

public Machine(java.lang.String name)

Creates a named finite state Machine. A Machine may optionally be named, where any supplied name must then match the owning Service's name.

Parameters:

name - the name of the Machine.

Method Detail

addState

public Machine addState(State state)

Adds a named State to the Machine. Each State must be uniquely named. A duplicate State will replace an existing State with the same name. This method may be used to add all the desired States to a default Machine. Any State declared to be a initial State will be cached as the initial State, but only one initial State is allowed. The current State will also be set to the initial State.

Parameters:

state - the state to add.

Returns:

this Machine.

getState

public State getState(java.lang.String name)

Returns the unique State with the given name.

Parameters:

name - the name of the State.

Returns:

the State, or null.

getStates

public java.util.Set<State> getStates()

Returns the set of States belonging to this Machine. Creates a new set containing all the unique States of this Machine.

Returns:

the set of States.

getTransitions

public java.util.Set<Transition> getTransitions()

Returns the set of Transitions belonging to this Machine. Creates a new set containing all the unique Transitions of this Machine.

Returns:

the set of Transitions.

getInitialState

public State getInitialState()

Returns the initial State.

Returns:

the initial State.

getCurrentState

public State getCurrentState()

Returns the current State;

Returns:

the current State.

reset

public Machine reset()

Resets this Machine to its initial State. The current State of this Machine is reset to the Machine's initial State. This method is invoked at the start of executing a fresh Sequence.

Returns:

this Machine.

clear

public Machine clear()

Resets every State and Transition in this Machine to its unmarked status. Whenever a Transition fires, both the Transition and the reached State are marked, to indicate that they have been covered. This method is invoked before a new TestSuite is created, to reset the traces in the model.

Returns:

this Machine.

accept

public boolean accept(Event event)

Reports whether this Machine accepts an Event in its current State. Reports whether this Machine's current State has an exit Transition labelled with the same name as the Event.

Parameters:

event - the Event.

Returns:

true, if an enabled Transition exists for this Event.

fireEvent

public boolean fireEvent(Event event)

Fires an event on this Machine. Applies the Event to this Machine in its current State. If an enabled Transition exists, the Transition is marked as having been fired, and this Machine's current State is set to the destination State indicated by the Transition. If no enabled Transition exists, does nothing.

Parameters:

event - the event.

Returns:

true, if the Event is accepted by this Machine.

getAlphabet

public Alphabet getAlphabet()

Returns the Alphabet of this Machine. Computes the Alphabet, the set of Events understood by this Machine. Iterates over the Transitions of this Machine and collects the Transition labels uniquely in a set.

Returns:

the Alphabet of this Machine, the set of Events.

getStateCover

public Language getStateCover()

Calculates the state cover for this Machine. This is the smallest Language containing the shortest Sequences that will reach every State in this Machine. Performs a breadth-first search, starting with the empty Sequence, and extending this on each iteration with every Event from the Alphabet, until every State has been visited once. Times out if the search eventually fails to reach every State.

Returns:

the state cover Language.

getTransitionCover

public Language getTransitionCover(int length)

Calculates the n-transition cover for this Machine. This is a Language consisting of Sequences that will reach every State and then explore every Transition path of length k = 0..n, starting from each State. The result includes the state cover, and is computed by taking the product of the state cover and the bounded language Ln*, which is the set of all Sequences of length 0..n chosen from the Alphabet.

Parameters:

length - the maximum Transition path length to explore.

Returns:

the n-transition cover Language.

getStateCover

protected Language getStateCover(Alphabet alphabet)

Calculates the state cover for this Machine. This is the smallest Language containing the shortest Sequences that will reach every State in this Machine. Performs a breadth-first search, starting with the empty Sequence, and extending this on each iteration with every Event from the Alphabet, until every State has been visited once. Times out if the search eventually fails to reach every State.

Parameters:

alphabet - the Alphabet of this Machine.

Returns:

the state cover Language.

validateMachine

public Machine validateMachine(Protocol protocol)

Validates the States and Transitions of this Machine for completeness. Checks for correspondence between the Transitions in this Machine and the Scenarios in the Protocol. Checks for the existence of an initial State and that all States are reachable in the Machine (notwithstanding any guards in the Protocol). Checks the completeness of each State under all Events from the Alphabet. Annotates this Machine with different Notice, Analysis and Warning nodes.

Parameters:

protocol - the associated Protocol, for comparison.

Returns:

this annotated Machine.

checkDifference

protected Warning checkDifference(Notice topInfo,
                      Alphabet difference)

Checks the difference between the Protocol alphabet and the Machine alphabet. If the Protocol alphabet contains more Events, creates a Warning describing which Events are not handled by this Machine, and attaches this Warning to the topInfo Notice.

Parameters:

topInfo - the top-level Notice.

difference - the extra actions present in the Protocol alphabet.

Returns:

a Warning, or null.

checkInitialState

protected Warning checkInitialState(Notice topInfo)

Checks that this Machine has an initial State. If this Machine has no initial State, creates a Warning describing how this Machine cannot be simulated, and attaches this Warning to the topInfo Notice.

Parameters:

topInfo - the top-level Notice.

Returns:

a Warning, or null.

checkTargetStates

protected Warning checkTargetStates(Notice topInfo)

Checks that the Transitions of this Machine refer to properly-named target States. If any Transition refers to a non-existent target State, creates a Warning describing how that State does not exist, and attaches this Warning to the topInfo Notice.

Parameters:

topInfo - the top-level Notice.

Returns:

a Warning, or null.

checkStateCoverage

public Warning checkStateCoverage(Notice topInfo)

Checks the coverage of States after simulating this Machine to find the state cover. If one or more States were never reached, creates a Warning describing which States were never reached, and attaches this Warning to the topInfo Notice.

Parameters:

topInfo - the top-level Notice.

Returns:

a Warning, or null.

checkTransitionCoverage

public Warning checkTransitionCoverage(Notice topInfo)

Checks the coverage of Transitions after simulating this Machine with a Language of a given maximum size. If one or more Transitions were never fired, creates a Warning describing which Transitions were never fired, and attaches this Warning to the topInfo Notice.

Parameters:

topInfo - the top-level Notice.

Returns:

a Warning, or null.