# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 4 Experimental Results
### Fischer's Mutual Exclusion Protocol
It suffices that associated channels chan_P[id] store only one message of the type TIMER_NUM_DATA_TYPE. The size of the array is the same as the number of process instances. In an attempt to prepare as similar a model to the DT Promela version as possible, we have modeled expire, delay, and udelay statements (lines 8-10). Construction of the inline send_to_channel might have seemed complicated when the SDL framework was used (Listing 4), but here it is shown that its preparation can be straightforward for simpler models (lines 12-28). Timer identification number is used to find the process that owns the timer. First guard checks if TID is within defined limits (line 14). If this is the case, temporary variable tmp_channel_offset is assigned the index of the timer in the array of timers. This has to be divided by the number of timers used by each process. TID 0 and 1 are assigned to the process with ID 0, TID 2 and 3 are assigned to process with ID 1, etc. Next, the buffer of associated process is checked to see if it is within expected limits, and a timer expiration signal is sent to the selected channel. The model of the process P is very similar to the DT Promela model. Timers y and y1 are assigned TID at the start of the process. Now, a mainstream version of Spin can be used to verify the protocol formally. To demonstrate the use of the Spin 6.4.6 and the SpinRCP 3.1.0 we have set deltaB to the value of 2 in the model with three active processes. Figure 3 shows the beginning of the MSC diagram for the guided simulation of the execution trail that violated the condition that only one process can enter the critical section. Process P[2] sets TID 4 to the value of 1 (deltaB). Process Monitor updates the timers_val table and returns the execution to the process. Next, timers with TID 2 and 0 are set to the same value. After the Promela timeout statement, process Monitor checks which timers are about to expire. Since all of the timers have expiration value 1, they all expire, and owning processes are sent the timer expiration message. The execution of the guided simulation was interrupted during the update of the array of timers, right before the update of the timers_val[0] which still holds the value of the expired timer. The timer expiration messages are not displayed in the MSC diagram because they have not been received by the processes thus far. They are still in the associated channels that hold the TID of the expired timers (Figure 3). ```
1#definePROC_P_TIHER_START_IND0
2#definePROC_P_TIHER_END_IND10
3#definePROC_P_TIHER_NUM2
4#definecv_buff2
5#defineNUMBER_OF_TIHERs10
6 chanchanchan_P[6]=[1]of(byte);
7
8 inline{inline{} }
```
9 inline{ } ```
1#definePROC_P_TIHER_START_IND0
10 inline{ }
```
11#definePROC_P_TIHER_NUM2
12#definePROC_P_TIHER_NUM2
13#defineNUMBER_OF_TIHERs10
14 chanchan_P[6]=[1]of(byte);
15
16
17 inline{ } ```


A detailed analysis revealed that process P[1] and P[2] entered the critical section concurrently. As shown, SpinRCP can display global and local variables and the contents of channel queues. Additionally, the display of the MSC can be optimized with the virtual processes, selected channels can be ignored or followed explicitly [16]. We have performed exhaustive exploration with Partial Order Reduction (POR) of both models. We have used DT Spin 4.1.1, Spin 4.1.1, and Spin 6.4.6, all with hash-table size of \(2^{18}\), so that memory usage can be compared. We have performed eight verification runs with each tool. Valid execution of the protocol depends on the value of the timers. The value of deltaC must be greater than the value of deltaB. Verification confirmed than only one process can enter into the critical section concurrently. Verification results of the DTMP model with both versions of Spin were very similar. Table 1 summarizes results for the DT and mainstream version of Spin 4.1.1. It presents the number of states, number of transitions, state-vector size, memory usage, and time required for formal verification of models. The parameter N presents the number of concurrent processes.