We want to admit more than 2 entities in the network. There is the problem that it is possible now that 2 stations send at the same time. In wireless networks an entity can't detect if there is a collision at the receiver.
We use the CSMA-CA-algorithm to resolve this problem and avoid collisions. The idea of this algorithm is that an entity waits a random time before it starts sending a message. Note that the algorithm just avoids collisions and not prevents collisions. It can happen that 2 stations decide to wait the same time and then start sending at the same time. The stations can't detect such a collision.
The simplified model in MoDeST:
01 process station(int id) {
02 clock timer;
03 do{
04 ::PERFORM_CSMA-CA; send_message{=timer=0,data=2 sending=true=};
05 when (timer==1) finish_send_message{= sending=!true =}
06 }
07 }
08 par{
09 ::coordinator()
10 ::relabel{send_message, finish_send_message} by
11 {s1_send_message, s1_finish_send_message} station(1)
12 ::relabel{send_message, finish_send_message} by
13 {s2_send_message, s2_finish_send_message} station(2)}
14 }
The process station has a parameter id, which models the address of the station in the network.
The expression PERFORM_CSMA-CA is a placeholder for the code that represents
the CSMA-CA-algorithm and not a part of a MoDeST construct.
It is used to hide the details and allows to show a global view of the model.
The next important point is that we only need to model one process station()
and can create more instances with the help of relabel.
We declare the actions s1_send_message,s3_send_message,s1_finish_send_message
and s2_finish_send_message
and give each instance of the process station() an own id.
We introduce a global boolean variable sending to indicate that a station is sending.
We don't use the synchronization on common actions to model the communication,
because we don't want to extend the coordinator each time when we add a new station to the network
(at least 2 new actions for 1 new station would be necessary, see
5.)