Demo files for the SmlMC Model Checker

buffer.sml

A simple example.

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:

d : int->string lis: list->(`a->string)->string


buf_struct.sml
buf_choice.sml
buf_timed.sml

Three simple examples demonstrating different features.


ssm_protocol.sml

A more elaborate example, see the DrDobbs article.

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:
var: the variable data members
fix: the fixed values
Only the var part will contribute to the states, in order to save space in the state hash table.

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.


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)

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

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.


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.

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.


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

The protocol tries to establish a root/child hierarchy between 2 equal nodes, and uses timers for this purpose. The principle is as follows:

When a node detects root contention it first makes a random choice between waiting a long or a short time.
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.
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:
fast : short waiting time
slow : long waiting time
gamma: interconnection delay

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.