uk.ac.sheffield.vtts.model

Class Protocol

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.Protocol

public class Protocol
extends Annotated

Protocol is a model of the abstract behaviour of a software service. A Protocol consists of a Memory, an abstraction over the state Variables used by the Service, and a set of Operations, describing the Operations offered by the Service. Each Operation describes its signature in terms of (optional) Input and Output Parameters. Each Operation consists of one or more Scenarios, where each Scenario represents one logical path through the Operation.

Version:

Broker@Cloud 1.0

Author:

Anthony J H Simons

Field Summary

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
Protocol() Creates a default Protocol with no name.
Protocol(java.lang.String name) Creates a named Protocol.

Method Summary

Methods

Modifier and Type	Method and Description
boolean	accept(Event event) Reports whether this Protocol accepts an Event in its current Memory state.
Protocol	addMemory(Memory memory) Adds the Memory to this Protocol.
Protocol	addOperation(Operation operation) Adds an Operation to this Protocol's set of Operations.
protected Warning	checkDifference(Notice topInfo, Alphabet difference) Checks the difference between the Machine alphabet and the Protocol alphabet.
boolean	fireEvent(Event event) Fires an event on this Protocol.
Alphabet	getAlphabet() Returns the Alphabet of this Protocol.
Memory	getMemory() Returns the memory of this service.
Operation	getOperation(Event event) Returns the Operation corresponding to the supplied Event.
Operation	getOperation(java.lang.String name) Returns the Operation with the specified unique name.
java.util.Set<Operation>	getOperations() Returns all the Operations of this Protocol, as a set.
Scenario	getScenario(Event event) Returns the Scenario corresponding to the supplied Event.
Protocol	reset() Resets this Protocol to its initial state.
Protocol	verifyProtocol(Machine machine) Verifies this Protocol for formal consistency and 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

Constructor Detail

Protocol

public Protocol()

Creates a default Protocol with no name.

Protocol

public Protocol(java.lang.String name)

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

Parameters:

name - the name of this Protocol.

Method Detail

addMemory

public Protocol addMemory(Memory memory)

Adds the Memory to this Protocol. The Memory is an abstraction over the global state Variables read and written by this Protocol. The Memory consists of a set of Constants and Variables, and an initial Binding of Constant values to Variables. When the Memory is added to this Protocol, this triggers resolution of the Variable names used in the Binding, such that all references point to declared Variables.

Parameters:

memory - the Memory to add.

Returns:

this Protocol.

getMemory

public Memory getMemory()

Returns the memory of this service. The Memory is an abstraction over the global state Variables read and written by this Protocol. It is an error if the Memory has not been attached, when it is first accessed for scope resolution purposes.

Returns:

the Memory of this Protocol.

addOperation

public Protocol addOperation(Operation operation)

Adds an Operation to this Protocol's set of Operations. Each Operation describes its signature in terms of (optional) Input and Output Parameters. Each Operation consists of one or more Scenarios, where each Scenario represents a logical path through the Operation. When an Operation is added to this Protocol, this triggers resolution of the global and local Parameters (Input, Output, or Variable) that are referenced within each Scenario, such that all references point to declared Parameters, whether global Variables in Memory, or local Inputs and Outputs declared in the Operation.

Parameters:

operation - the Operation to add.

Returns:

this Protocol.

getOperation

public Operation getOperation(java.lang.String name)

Returns the Operation with the specified unique name.

Parameters:

name - the name of the Operation.

Returns:

the associated Operation, or null if no such Operation exists.

getOperations

public java.util.Set<Operation> getOperations()

Returns all the Operations of this Protocol, as a set. Operations are uniquely named.

Returns:

the set of Operations in this Protocol.

getAlphabet

public Alphabet getAlphabet()

Returns the Alphabet of this Protocol. Computes the Alphabet, the set of Events understood by this Protocol. Iterates over the Operations and Scenarios of this Protocol, collecting the Scenario labels as a set of unique Events. This is used when checking that the Protocol and Machine understand the same set of Events.

Returns:

the Alphabet of this Protocol, a set of Events.

getScenario

public Scenario getScenario(Event event)

Returns the Scenario corresponding to the supplied Event. The Event is a label on a Transition of the Machine, which corresponds to one Scenario in an Operation of the Protocol.

Parameters:

event - the Event.

Returns:

the corresponding Scenario, which must exist.

getOperation

public Operation getOperation(Event event)

Returns the Operation corresponding to the supplied Event. Selects the Operation, whose name is equal to the Event's request-name. Raises a semantic error if no such Operation exists.

Parameters:

event - the Event.

Returns:

the corresponding Operation, which must exist.

reset

public Protocol reset()

Resets this Protocol to its initial state. Rebinds Memory to its initial value and unbinds all parameters in each Operation.

Returns:

this Protocol.

accept

public boolean accept(Event event)

Reports whether this Protocol accepts an Event in its current Memory state. Selects the Operation corresponding to the Event's request-name and selects the Scenario from the Operation, whose name is equal to the Event's whole name. Reports whether this Scenario may be executed in the current Memory environment.

Parameters:

event - an Event.

Returns:

true, if the corresponding Scenario can be executed.

fireEvent

public boolean fireEvent(Event event)

Fires an event on this Protocol. Selects the Operation named by the supplied Event's request-name, and fires the event on that Operation.

Parameters:

event - an Event.

Returns:

true, if the Event can fire.

verifyProtocol

public Protocol verifyProtocol(Machine machine)

Verifies this Protocol for formal consistency and completeness. Checks for correspondence between the Scenarios in the Protocol and the Transitions in the Machine. Checks that the Memory is correctly initialised. Checks that each Operation is deterministic and complete under all input and memory conditions. Annotates the Protocol with various Notice, Analysis and Warning nodes.

Parameters:

machine - the associated Machine, for comparison.

Returns:

the annotated Protocol.

checkDifference

protected Warning checkDifference(Notice topInfo,
                      Alphabet difference)

Checks the difference between the Machine alphabet and the Protocol alphabet. If the Machine alphabet contains more events, creates a Warning describing which events are not handled by this Protocol.

Parameters:

topInfo - the top-level Notice.

difference - the extra events present in the Machine alphabet.

Returns:

a Warning, or null.