Notice function pr.printq in print_comp. This is a general text formatting function, using the "quotation/antiquotation" feature of Moscow ML. In structure pr (from sml_lib) several string-conversion functions are provided, for instance:
The access functions for data members of the Ne datatype are
bundled in structure ne.
The data members for a network element are split into 2 groups,
in datatype Var_Fix. This is a record with 2 fields:
Notice that fix contains a reference called i3, which points
to a clock source that itself is a Component. Maybe it's not so easy
to understand how this works, however it is normal functional programming style.
Event con1 controls the communication between ne1 and
ne2.
If it has value Con(false), then there is a cable break between
these 2 network elements.
The actual SSM protocol functionality (choosing the input with the best
clock quality, also considering port priorities) is performed
by function sel_alg.
The Leader Election Protocol tries to find the node with
the highest quality. The nodes are interconnected in a ring.
The quality is encoded in the first data member of type Node.
The protocol only works if the output value of a Node is buffered
in a queue. This queue is modeled as a list, the 4th data member
of Node.
Model checking:
If you run this code you will notice that 34 states are found,
where in 3 final states a deadlock occurs: each philosopher
has 1 fork, and nobody can eat. A remedy is listed in an
(out-commented) code part. Here the deadlock situation is detected,
and one of the philosophers is persuaded to lay his fork down.
Notice that the value of with_timing is false.
If it is set to true, then the deadlock situation is
reached immediately in the first state.
Each event controls 1 philosopher and 2 forks. At the start all
events are activated. After an event has fired it will activate
its 2 neighboring events. You might try other schemes, maybe you
find a solution where all philosophers can think and eat forever
without a special deadlock detection. The laying down of the 2
forks by a philosopher is done concurrently. You might want to
modify this such that there is an intermediate state between putting down
the first and the second fork.
In the SmlMC code it can be seen that each telephone is
controlled by a lot of events, from which always only one is
active. This way a kind of FSM (finite-state machine) is
modeled, with several non-deterministic choices for the
transitions between the FSM states. Function okay calculates if
an transition can be taken, depending on the state of the data
in the multiplexer. If an transition cannot be taken, then event
next_ev is activated, which will be re-activated until the
transition can be taken. The data member of component next_state
is equal to #index (see SmlMC_head.sml), which is equal to
the index of the event in the events vector.
Notice that component Subs (modelling one telephone)
has an extra member of type string. This is only used for identification.
The protocol tries to establish a root/child hierarchy between 2 equal
nodes, and uses timers for this purpose. The principle is as follows:
The protocol works if slow - fast > gamma. If you decrease
slow, then model checking will reveal an error
(function reach_test).
In the paper is clarified that no preq signal should be sent
if the interconnection is "busy". In the SmlMC code this is implemented
by testing if the output buffer is empty before filling it with a preq
signal (in state AWAKE).
A remark about the coding style for the FSM: this is done with a case
statement used like a switch statement in C.
In SML, the selection value then
must be a constant: an integer, a string or an instance of a datatype.
The last option has been chosen here. Notice that, depending on the state
of a node, events are activated in different ways. In state AWAKE the node
activates the wire to the other node, and it can be re-activated
(in state PREQ) by the other wire.
Only the var part will contribute to the states, in order
to save space in the state hash table.
leader.sml
The file from which this is a translation: leader.spin. This
is Promela code as used by the model checker Spin (see:
whatispin.html)
path_test checks if at any time more then 1 leader is selected.
reach_test does the same for the final system states.
philosophers.sml
The classic "dining philosophers" problem. Here 3 philosophers
are sitting around the table. It is easy to parameterize the
code such that there are N of them. Notice that vector components
consists of vectors of integers, demonstrating that a user-defined datatype
is not always needed.
pots.sml
This is a Plain Old Telephone System. It is a translation of an
original Lotos file: pots-wb.lotos, which is a somewhat
simplified version of a realistic telephone system with one
multiplexer and 2 telephones. The Lotos source contains much
comment to clarify how this works. The original Lotos code for
the full system can be found in
demos.html.
root_cont.sml
This is a model for the root contention phase of the IEEE 1394 (FireWire)
protocol, as described in a paper:
firewire.pdf
When a node detects root contention it first makes a random choice
between waiting a long or a short time.
On page 8 of the firewire paper an FSM diagram of a node is depicted. This
FSM has been translated to the functionality of an event
(function node_ev). The 2 nodes start with an equal waiting time.
When the start state RC is traversed the second time, one of the nodes
gets a longer waiting time. Three delays are involved:
After the waiting period has elapsed, either no message has arrived:
then a parent request is issued,
or a parent request has been received:
then assumed "root" and an acknowledgment is issued.
As soon as a node receives an acknowledgment, then assumed "child".
If a node that has sent a parent request receives another parent request
instead of an acknowledgment, then start over again.
fast : short waiting time
slow : long waiting time
gamma: interconnection delay