# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 4 Experimental Results
### Fischer's Mutual Exclusion Protocol  
Pseudo code for the well-known Fischer's Mutual Exclusion Protocol is shown in Listing 5[37]. Atomic operations are written between \"\(<\)\" and \"\(>\)\". The critical section and the code that is not part of the mutual exclusion protocol must not modify any variable used by the algorithm. The **await**\(<\)x == 0\(>\) should be interpreted as **while**\(\ \
eg\ <\)x == 0\(>\)**do** skip. The algorithm is executed by a process with the unique identifier \(n\). The delay operation must be long enough that process \(m\), which evaluated its await statement before \(n\) executes x = n, can complete statement x = m. In this case, process \(n\) will not enter the critical section and will wait for the next opportunity. ```
1 repeat
2<nctriticalsection>
3 repeat
4 await<x == 0>
5<x = m >
6<delay>
7 until<x == n >
8<criticalsection>
9 untilfalse
```  
Listing 6 shows the DT Promela model for FMEP that is based on the model available at [20]. Processes are created within initial process init (lines 21-26). The presented model has five process instances: P(0), P(1), P(2), P(3), and P(4) that execute concurrently. At the beginning, the value of the shared variable \(x\) is zero. After unbounded delay, the executing process instance checks if the value of the \(x\) variable is zero. If this is the case, it assigns \(x\) its identification value of \(id+1\). Next, the process waits for \(deltaC\) ticks to enable competing process instance to enter the critical section (line 14). Before it enters into the critical section, it checks if it is still available--the value of the shared variable \(x\) still holds its identification value. If that is the case, the process enters the critical section. It stays in the critical section for an unbounded delay. Before it leaves the critical section, it sets the shared variable \(x\) to zero. ```
1#include\"time.h\"
2
3#defineN5
4#definedeltaB1
5#definedeltaC2
6
7 bytex,in_crit;
8
9 prototypeP(byteid){
10 timerY,Y1;
11 do
12:!udelay(y);
13x==0->atomic(delay(y,delta)->x=id+1;)
14 atomic(delay(y,deltaC);)->
15 atomic(x=-id+1;in_crit++;)->
16 udelay(y1);
17 atomic(x=0;in_crit--)
18 od
19}
20
21 init
22{
23 atomic{
24 runP(0);runP(1);runP(2);runP(3);runP(4);
25}
26}
27
28 never{
29 do
30::in_crit>1->break;
31::skip
32 od
33}
```  
Listing 6: DT Promela model of the Fischer's Mutual Exclusion Protocol. We have verified the model with the declaration of a temporal claim. The never-claim is used most commonly to specify behavior that should never happen. Only statements that can have a side effect on the system state are not allowed. If claim is present in the model of the system, each step along the execution path consists of a pair of transitions. First, the claim automaton is executed. The second transition is from one of the active processes. If the claim automaton does not have any executable transitions, the search along this path is stopped. The search then backtracks and explores other executions. The claim is defined as a series of propositions, or boolean expressions, on the system state that must become true for the behavior of interest to be matched. A never claim can be used to match either finite or infinite behaviors. Finite behavior is matched if the claim can reach its final state. In our case, this happens if the variable in_crit is greater than 1 which indicates that more than one process has entered the critical section (lines 28-33). Listing 7 shows the DTMP of FMEP, without never claim and init process, which are the same as in the DT Promela model of the protocol. The expiration of a timer is modeled in DTMP with a message. Here we follow rules that are explained in Section 3. Because there are no other signals, PROC_P_TIMER_START_IND starts at 0. The PROC_P_TIMER_END_IND is set at the maximum number of timers. We have decided that each process will use two timers and PROC_P_TIMER_NUM is set accordingly. Input queues for the process instances are modeled with the array of channels chan_P.