The global declaration part
      ////////////////The Model//////////////////
      #define N 4; //number of stations

channel begin;
      channel end;
      channel busy;
      channel cd[N];

var k = [-1(N)]; //record state of the station, 0: sending the message
      var j = 0; //used to broadcast the collision messgae

clock x; //the clock for bus
      clock y[N]; //the clock for the station

In this example, we define N as a constant tha represents four stations competing for the bus.  channel begin represents that station begins to send messages; channel end represents that the station completes the transmission; channel busy represents that one station is sending the messages on the bus; channel cd[N] is an array of channels, representing that the ith station receives a collision.

The process definition part

Bus Process:

Station Process with paramenter i:        

In this example, when process Bus is in the bus_collision state, and process Station(0) is in the sender_retry state, the next execution is that two processes synchronise by channel cd, the evaluation order of the channel cd  likes the following:

1. channel cd[j]! output clock guard (x<26) evaluation and checking

2. channel cd[j]!  output channel name evaluation (j)

3. channel cd[i]? input channel name evaluation (the value of i is 0)

4. channel cd[i]?  input clock guard (y[i]<52) evaluation and checking

5. channel output program (j=j+1) evaluation         

The whole system is defined as follows:

CSMACD =  (|||m :{0..N-1} @ Station(m)) ||| Bus;

The asserstion part
     ////////////////////////////////////////////////////////////////////////////////////

#assert CSMACD deadlockfree;