Graded-CTL NuSMV

Source Code for "ABP10"

Description of the Alternating Bit Protocol
===========================================

The protocol consist of four `agents':

1) The Sender
2) The Receiver
3) The Sender to Receiver Medium S2R
4) The Receiver to Sender Medium R2S

The four agents are connected via logical channels that act as fifo
queues. The capacity of these channels is supposed to be of arbitrary
size (even infinite). `s2r.in' is a logical output channel for the
Sender and a logical input channel for the S2R medium and so on. The
contents of an s2r channel datagram can be `err' or `data(b,d)' with
'b' a binary value and `d' of an arbitraty but fixed data type. The
contents of an r2s channel datagram can be `err' or `ack(b)' with 'b'
a binary value.

Sender and Receiver both have a binary `alternating bit' variable
dentoted `ab'. They also have a local variable `d' that is used to
store the transmitted data. The Sender has three control states:

'get' = get data from user (user not modeled here)
'send' = wait for s2r channel ready and send data
'wait_for_ack' = wait for response on r2s channel

The Receiver also has three control states:

'receive' = wait for incoming data on channel s2r
'deliver' = deliver data to user (user not modeled here)
'send_ack' = wait for r2s channel ready and send acknowledgement

The transitions on the following state diagrams are attributed by
conditions, assignments to local variables (ab and d) and patterns
matching the contents of the input and output channels (i/o).

For example a transition with the attribute

'ab == 1 & d := ? & ./data(ab,d)'

has the semantic that this transition is enabled iff the current
value of the alternating bit is one. After this transition has 'fired'
the new value of d is choosen nondeterministically, a message 'data'
with the current values of ab and d as arguments is written onto the
output channel and ab does not change. The dot `.' in `./data(ab,d)'
can be interpreted as an `epsilon' which means that the input channel
may contain arbitrary or no data and that it does not change.

If no transition is enabled (because conditions evaluate to false,
the input pattern does not match, or the output channel is full)
then the state of the agent does not change.

Sender:
=======

Receiver:
=========

(* means any data)

S2R:
====

R2S:
====

MODULE Sender(s2r_in, r2s_out)

VAR
state : { get, send, wait_for_ack };
abp : boolean;
data : 0..1023;--DATA

ASSIGN

init(state) := get;
init(abp) := 0;

next(state) := case
state = get : send;
state = send & s2r_in.tag = mt : wait_for_ack;
state = send & !(s2r_in.tag = mt) : send;
state = wait_for_ack & (!abp & r2s_out.tag = ack0 | abp & r2s_out.tag = ack1): get;
state = wait_for_ack & (abp & r2s_out.tag = ack0 | !abp & r2s_out.tag = ack1 | r2s_out.tag = error): send;
state = wait_for_ack & r2s_out.tag = mt: wait_for_ack;
esac;

next(abp) := case
state = wait_for_ack & (!abp & r2s_out.tag = ack0 | abp & r2s_out.tag = ack1): !abp;
1: abp;
esac;

next(data) := case
state = wait_for_ack & (!abp & r2s_out.tag = ack0 | abp & r2s_out.tag = ack1): 0..1023;
1: data;
esac;

next(s2r_in.tag) := case
state = send & s2r_in.tag = mt : case
abp: data1;
!abp: data0;
esac;
1: s2r_in.tag;
esac;

next(s2r_in.data) := case
state = send & s2r_in.tag = mt: data;
1: s2r_in.data;
esac;

next(r2s_out.tag) := case
state = wait_for_ack: mt;
1: r2s_out.tag;
esac;

FAIRNESS running

MODULE Receiver(r2s_in, s2r_out)

VAR
state : { receive, deliver, send_ack };
abp : boolean;
data : 0..1023;--DATA

ASSIGN
init(state) := receive;
init(abp) := 0;

next(state) := case
state = receive & (!abp & s2r_out.tag = data0 | abp & s2r_out.tag = data1): deliver;
state = receive & (abp & s2r_out.tag = data0 | !abp & s2r_out.tag = data1 | s2r_out.tag = error): send_ack;
state = receive & s2r_out.tag = mt: state;
state = deliver: send_ack;
state = send_ack & r2s_in.tag = mt: receive;
state = send_ack & !(r2s_in.tag = mt): state;
esac;

next(abp) := case
state = deliver: !abp;
1: abp;
esac;

next(data) := case
state = receive &(!abp & s2r_out.tag = data0 | abp & s2r_out.tag = data1): s2r_out.data;
1: data;
esac;

next(s2r_out.tag) := case
state = receive: mt;
1: s2r_out.tag;
esac;

next(s2r_out.data) := s2r_out.data;

next(r2s_in.tag) := case
state = send_ack & r2s_in.tag = mt : case
abp: ack0;
!abp: ack1;
esac;
1: r2s_in.tag;
esac;

FAIRNESS running

MODULE S2RData

VAR
tag : { mt, data0, data1, error };
data : 0..1023;--DATA

ASSIGN
init(tag) := mt;

MODULE R2SData

VAR
tag : { mt, ack0, ack1, error };

ASSIGN
init(tag) := mt;

MODULE R2S(i, o)

ASSIGN
next(o.tag) := case
o.tag = mt & !(i.tag = mt): i.tag union error;
1: o.tag;
esac;

next(i.tag) := case
o.tag = mt & !(i.tag = mt): mt;
1: i.tag;
esac;

FAIRNESS running
FAIRNESS o.tag = ack0 | o.tag = ack1

MODULE S2R(i, o)

ASSIGN
next(o.tag) := case
o.tag = mt & !(i.tag = mt): i.tag union error;
1: o.tag;
esac;

next(i.tag) := case
o.tag = mt & !(i.tag = mt): mt;
1: i.tag;
esac;

next(o.data) := case
o.tag = mt & !(i.tag = mt): i.data;
1: o.data;
esac;

next(i.data) := i.data;

FAIRNESS running
FAIRNESS o.tag = data0 | o.tag = data1

MODULE main

VAR
sender: process Sender(s2r_in, r2s_out);
s2r_in: S2RData;
s2r_out: S2RData;
receiver: process Receiver(r2s_in, s2r_out);
r2s_in: R2SData;
r2s_out: R2SData;
r2s: process R2S(r2s_in, r2s_out);
s2r: process S2R(s2r_in, s2r_out);