# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 3 Discrete Time Model for Promela
We have automated static analysis of the SDL specification and the definition of macros with the _sdl2 pml_ tool [19]. The Promela channel that models the SDL input queue of the specific SDL process should support reception of all possible SDL signals with parameters, including timer expiration signals. Therefore, the channel definition that models the input queue of a specific SDL process can be unique. If the process can have more than one instance, an array of channels is defined. Consequently, the definition of the inline send_to_channel has to be adapted for each system. It sends timer expiration messages to all process instances that include timers. Listing 4 presents part of the inline that was generated by the _sdl2 pml_ tool for the real-world SDL system described in [13]. It includes only a small part of the inline definition that is dedicated to the process L3 netA in the block L3. It demonstrates how macros are used to send a timer expiration message to the right process instance. Let us assume that this particular system includes 49 SDL signals that are not associated with timers. Additionally, the specification permits five instances of the SDL process L3 netA that utilizes four timers T1-T4. Imagine that process L3 netA is the second process that is assigned TIDs and that the first analyzed process has only one instance that utilizes 10 timers. The following macros would be defined:

* #define TMR_BEGIN_INDEX 50--number of the signal that represents first TID,
* #define L3_L3 netA_TMR_START_INDEX 60--number of the signal that represents the first timer used by the process L3 netA,
* #define L3_L3 netA_TMR_END_INDEX 80,
* #define L3_L3 netA_TMR_NUMBER 4--number of utilized timers by each process instance,
*  chan_L3_L3 netA 2--the channel that models the input queue of the SDL process. The first guard in the inline send_to_channel (Listing 4 checks if an expired timer is associated with the process L3 netA. This is done by checking if the TID is within the expected range of values for all process instances (3-4). If this is not the case, probe pv_timeout_send_error is set to true, which triggers error at the Monitor process. ```  
Next, the channel offset has to be calculated for the process instance that owns the expired timer. Channel offset for the first instance of the process is equal to zero and increases by one for each new process instance. If the TID of the expired timer is 25, variable tmp_channel_offset is assigned the number of the timer within the model of the process, \(25-(60-50)=15\). This represents timer T4 in the fourth instance of the process. Channel offset is obtained by dividing this number with the number of utilized timers by each process instance, \(\lfloor 15/4\rfloor=3\) (line 8). In our example, calculated offset is associated with the fourth instance, as expected. Now, the number of the timer expiration message is calculated. Each timer is assigned only one unique timer expiration message number that is used by all process instances, \(50+(25-3*4)=63\) (line 11). Message numbers 50-9 are assigned to the first analyzed process. For the timers utilized by process L3 netA the following numbers are used: T1 \(\leftrightarrow\) 60, T2 \(\leftrightarrow\) 61, T3 \(\leftrightarrow\) 62, T4 \(\leftrightarrow\) 63. This confirms that timer T4 expired. Constant value cv_buff defines the capacity of the message channel that models the SDL input queue of the process. To optimize the state-space of the model it should be kept to the minimum. By default the _sdl2 pml_ tool sets it to 4. However, if this limit is reached during the run of the system, execution of the model is not sound. If the input queue of the process is full, probe pv_proc_full_queue is activated and the process Monitor stops the evaluation of the model, due to the false assertion (line 14), and the buffer should be increased before the next run. If everything is in order, a timer expiration message is sent to the associated message channel chan_L3_L3 netA with the calculated channel offset.