# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 3 Discrete Time Model for Promela
The TIMER_VAL_DATA_TYPE is synonym for the short data type and defines the domain of timer values. If necessary, this can be changed to int which is the largest data type supported by Promela within the channel initializer [10]. Next, globally defined temporary variables are defined that are used by the Monitor process. They are excluded from the state descriptor during verification with the keyword hidden (lines 3-8). When a timer is set or reset, processes communicate with the Monitor over the predefined synchronous channel CHAN_TIMEOUT_PROC, which is a synonym for the channel definition chan_timeout (Listing 2, lines 10-11). The number of the timers supported by the channel is limited by the TIMER_NUM_DATA_TYPE. Processes activate the selected timer with an inline function set. The body of the inline function is inserted directly into the body of the process as a replacement text for a symbolic name with parameters. It sends the TID (tmr) and its value (value) to the CHAN_TIMEOUT_PROC channel. Next, the Monitor returns the execution to the sending process with the return of the same signal. This prevents interleaving of processes during this statement. The timer can be reset with the reset inline function that sets timer value to 0. Additionally, the model of the SDL framework has to ensure that all pending timer expiration messages are removed from the input queue of the owning process instance. ```
1#define TIMER_NUM_DATA_TYPE byte
2#define TIMER_VAL_DATA_TYPE show
3 hidden TIMER_VAL_DATA_TYPE unimportant_val;
4 hidden TIMER_NUM_DATA_TYPE tmp_timer_id;
5 hidden TIMER_NUM_DATA_TYPE tmp_counter;
6 hidden TIMER_NUM_DATA_TYPE min_val_index;
7 hidden TIMER_VAL_DATA_TYPE tmp_timer_id_val;
8 hidden TIMER_NUM_DATA_TYPE tmp_channel_offset;
9
10 chanchan_timeout=[0]of(TIMER_NUM_DATA_TYPE,TIMER_VAL_DATA_TYPE);
11#defineCHAN_TIMEOUT_PROC chan_timeout
12
13 inlineset(tmr,value){CHAN_TIMEOUT_PROC!tmr(value);
14 CHAN_TIMEOUT_PROC?tmr(unimportant_val);}
15 inlinereset(tmr){CHAN_TIMEOUT_PROC!tmr(unimportant_val);}
16 CHAN_TIMEOUT_PROC?tmr(unimportant_val);}
17
18 show bool pv_proc_full_queue_error = false;
19 show bool pv_runtime_error = false;
20 show bool pv_timeout_send_error = false;
```
1 activeprototypeMonitor(){
2 TIMER_VAL_DATA_TYPEtimers_val[NUMBER_OF_TIMERS];
3 do
4i:atomic{CHAN_TIMEOUT_PROC7 tmp_timer_id(tmp_timer_id_val);
5 timers_val[tmp_timer_id] =tmp_timer_id_val;
6 CHAN_TIMEOUT_PROC1 tmp_timer_id((tmp_timer_id_val));
7}
8::atomic{timeout->printf(\"MSC:U70\
\");
9 atomic{
10 tmp_counter=0;
11 min_val_index=0;
12 do
13:tmp_counter<NUMBER_OF_TIMERS->
14 if
15::timers_val[min_val_index] == 0 -> min_val_index++;tmp_counter++
16::(timers_val[tmp_counter] <timers_val[min_val_index] && \
17 timers_val[tmp_counter]!=0)->
18 min_val_index=tmp_counter;
19 tmp_counter++;
20::else->tmp_counter++;
21#:else->break;
22 id;
23
24>
25 tmp_counter=0;
26 if
27::min_val_index==NUMBER_OF_TIMERS->skip;
28::else->
29 do
30::((tmp_counter<NUMBER_OF_TIMERS)&& (timers_val[tmp_counter] == \
31 timers_val[min_val_index]))->
32 if
33::(timers_val[tmp_counter]!=0)->
34 send_to_channel(tmp_counter);
35 if
36:tmp_counter==min_val_index->skip;tmp_counter++;
37::else->timers_val[tmp_counter] =0;tmp_counter++;
38 if;
39::else->tmp_counter++;
40 ifi;
41::tmp_counter==NUMBER_OF_TIMERS->break;
42::else->tmp_counter++;
43 dd;
44 tmp_counter=0;
45d0
46::tmp_counter<NUMBER_OF_TIMERS->
47 if
48::((timers_val[tmp_counter]!=0)&& (tmp_counter!=min_val_index))->
49 timers_val[tmp_counter]=timers_val[tmp_counter]-timers_val[min_val_index];
50::else->skip;
51 ifi;tmp_counter++;
52i:tmp_counter>=NUMBER_OF_TIMERS->break;
53 od;
54 timers_val[min_val_index]=0;
55 ifi;
56 temp_counter=0;
57 min_val_index=0
58}
59::pv_proc_full_queue_error==true->assert(false);
60::pv_runtime_error==true->assert(false);
61::pv_timeout_send_error==true->assert(false);
62 od;
63}
```
Listing 3: dtmp.pml, part 2: Definition of process Monitor. The Monitor process executes in a loop (Listing 3). It includes five option statements (guards).