 instance of DLC by executing transition TR1 in Figure 7.27; unfor- tunately, the instance is dead; therefore, an output to a Null Pid is executed, detected by the Validator. Remark: the error discovered by ObjectGeode in the same configuration is a bit different. The error scenario discovered by ObjectGeode cannot be replayed by the Validator, because in ObjectGeode the feed command transmits signals to the model without storing them in the input queues. When replaying the error discovered by ObjectGeode, the Tau Validator signals Exhaustive Simulation 205 Report Viewer 5 reports 3 MaxQueueLength 2 Output Error in SDL Output Error in SDL Output of signal V76frame of signal V76frame Signal sent to NULL Signal sent to NULL Sender: <<Block Sender: <<Block DLCa>> dispatch:1 DLCa>> dispatch:1 Depth: 23 Depth: 28 Figure 7.25 The Report Viewer (5 reports) MSC bug_exh4 process process <<Block DLCa>> <Block DLCb>> dispatch dispatch env_a dispatch_3 process AtoB_1 dispatch_4 env_b <<Block DLCa>> L_EstabReq BtoA_2 DLC_5 (0, true) V76frame T320(12) (SABME : (.0.)) V76frame L_Establnd (SABME (.0.)) V76frame T320(12) (SABME (.0.)) DLCstopped L Releaselnd L_EstabResp process <<Block DLCb>> DLC_6 (0, false) V76frame V76frame (UA : (.0.)) V76frame (UA : . . 0 .)) (UA (.0.)) Figure 7.26 The error MSC trace 206 Validation of Communications Systems with SDL PROCESS dispatch(1, 1) transition TR1 output to ready Null Pid V76frame (V76para) V76para ! present SABME DLCpeer:= V76frame(V76para) V76para !SABME ! DLCi TO DLCs(V76para) ! UA ! DLCi) DLCs(DLCpeer) Figure 7.27 The output to Null in process dispatch part1 (extract) that the input queue limit (of 1 signal here) is reached when transmitting the L_EstabResp: the input queue of dispatch already contains the saved v76frame. 7.3.4.4 Correct the error The simulation has revealed that we must protect the expressions after TO in the output state- ments to avoid having a Null Pid. For that, you will add a decision to test the value of the expression: if Null, the output is not performed.