# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 3 Discrete Time Model for Promela
Executed statements are selected non-deterministically between the executable guards. The first option statement (lines 4-7) checks if a signal with two parameters can be received at the CHAN_TIMEOUT_PROC channel. This happens when some process changes the value of one of its timers. Timer identification number and value of the timer are stored in temporary variables tmp_timer_id and tmp_timer_id_val, respectively. Next, the value of the timer is stored in the timers_val array where TID is used as an index. Finally, the execution is transferred back to the sender. The whole option has to be executed as an atomic sequence. The second option statement is executed when all processes are blocked and a predefined Promela timeout event occurs. Then, timers that should expire are found. Figure 2 presents the expiration of timers in DTMP graphically. In this example, four timers (\(t_{1}\), \(t_{2}\), \(t_{3}\), \(t_{4}\)) are active. Their values are 4, 6, 10 and 6. A timer is inactive when its value is equal to 0. At each timeout event, timers that hold the minimum value are found. In the presented example, the timer \(t_{1}\) expires at the first timeout event. To ensure correct expiration order, the value of \(t_{1}\) is subtracted from the remaining active timers. Next, timers \(t_{2}\) and \(t_{4}\) should expire, but timers \(t_{1}\) and \(t_{4}\) are set to 8 and 5, respectively, before the next timeout event. Therefore, timer \(t_{3}\) expires the next timeout event. The values of the remaining active timers (\(t_{1}\), \(t_{4}\)) are decreased by 4. Process Monitor finds the minimal expiration value of active timers by exploring the array of timers timers_val with the help of temporary index tmp_counter (Listing 3, lines 12-23). The first option statement of the if selection construct skips deactivated timers. The second option statement is executable if the active timer at the current temporary index has a new minimal expiration value. Then, variable min_val_index is updated with the TID. When NUMBER_OF_TIMERS is reached, the search is completed. Next, the inline send_to_channel is used to send a timer expiration messages (lines 29-43). The inline send_to_channel is adapted to the input queue of every process. Finally, values of all active timers are decreased (lines 45-53). The maximum possible number of timers (NUMBER_OF_TIMERS) is acquired with the static analysis of the SDL specification. It is computed as follows:

\[\sum_{n=1}^{proc_{t}}num\_tmr\_proc_{n}*max\_inst_{n}, \tag{1}\]

where

* \(proc_{t}\)--is the number of process definitions in a model that include timers,
* \(num\_tmr\_proc_{n}\)--is the number of timer definitions in the \(n\)-th process, and
* \(max\_inst_{n}\)--is the maximum number of instances of the \(n\)-th process. The Monitor process also reports unexpected values of the automatically inserted probes that monitor execution of the Promela framework for the abstract SDL machine as defined in [14] (lines 59-61). If the input queue of the process is full, probe pv_proc_full_queue is activated. Probe pv_runtime_error detects errors in the Promela model of the SDL system. Probe pv_timeout_send_error detects addressing errors. During the static analysis of the SDL specification all signals are enumerated. The timer expiration signals are identified in the Promela model with the use of TID. The range of TIDs is defined by the subset of the enumerated SDL signals:

* TMR_BEGIN_INDEX--TID of the first timer,
* TMR_END_INDEX--next free signal number in the model. For each process we define similar macros where a unique prefix defines the location of the process within the SDL structure:

* prefix_TMR_START_INDEX--TID of the first timer used by the process,

Figure 2: Expiration of timers. prefix__TMR_END_INDEX--value of the next free TID, and prefix__TMR_NUMBER--number of the timers in the process. For example, the number of timers in the process P that is part of the block B would be defined in B_P_TMR_NUMBER.