Protocol model

Each process is modeled as an automaton that behaves as follows. Each time an event occurs, the corresponding processor examines its state and decides what its next state will be and what action it is supposed to take in response to the event, i.e. to make some local computation and/or send message(s) to some of its neighbours. These messages will be received after some time, according to the communication delay of the transmittion line. We introduce some definitions below :

The model of the protocol that is executed in this simulator is that of a deterministic finite state automaton of a specific form, i.e. a 8-tuple (K, S, M, T, R, I, A, d).

K

is the finite set of the states in which each node of the distributed system can be.

S

is the initial state of every node.

M

is the finite set of all the types of messages that nodes can send. Every member of M is associated with a set of variables, which hold the values that are sent each time.

T

is the set of timers that are used in each node.

R

is a set of registers that each process (node) can use locally; these local registers hold the local values that are used as auxilliary information about the state of the node.

I

For every node, each local register has an initial value that is contained in the set of the initial register values I.
In this set, there are also some special values included, called protocol parameters (e.g. some threshold values for bounding the number of trials to control the complexity of the protocol, or some probability parameters if the protocol can take probabilistic actions, etc) that control the execution of the protocol and can vary between different executions.

A

is a set of actions; in each of these actions a new local state may selected, local variable values may be updated, some messages may be sent, and a timer can be set (started) or reset (stopped).

d

is the transition function; for each couple (state, event) it specifies an action of the set A to be taken. An event, as described at the section on the simulator model, is a receipt of a message by a node or a timeout generated by a timer. The case that a node wakes up spontaneously is taken care of by the generation of a special event, the INITPROTOCOL event: Strictly speaking, d is a function :

       <d>  :  ( <K> * ({INITPROTOCOL} U <M> U <T>) )  -> <A>