put_v76frame 11 D_presentextract (v76para) A_=i.D__vrp_1.A_=false. : from_waitua_input_v76fram Dpresentextract (v76para) A =dm. : 0 The basic block labeled 29 in the results above is located in process dispatch, in a transition from state ready beginning with the input of signal v76frame. D means decision, presen- textract(v76para) means v76para ! present, .A =i means answer =i. Finally, the answer is followed by another decision: D_extract(dlcs, dlciextract (iextract(v76para))). A_=null means a decision containing DLCs (V76para !I ! DLCi)=Null. The corresponding basic block, plus the basic block number 39, are shown in Figure 7.59. process dispatch(1, 1) ready V76frame (V76para) basic block 39 V76para present SABME ) ( ) ) ( XIDresp ) DLCs(V76para L_SetparmConf I ! DLCi) basic block 29 ( UA ) V76frame(V76para) TO DLCs(V76para) I ! DLCi) Figure 7.59 The two basic blocks never executed in process dispatch The basic block number 29 corresponds to one of the five decisions added previously, to protect against output to Null. The fact that it has never been executed is not a problem. The basic block number 39 also corresponds to a case that should never happen. The basic block number 11, shown in Figure 7.60, corresponds to the result False to the procedure CRCok: it is normal for this basic block to have never been executed, as the procedure always returns True. The basic block number 15, shown in Figure 7.61, corresponds to the answer DM to the decision V76para ! present. It means that a connection establishment has never been refused by the peer Service User. After checking that our feed commands contain the transmission of L_ReleaseReq to block DLCb, we see that an input of L_ReleaseReq is missing in state waitEstabResp, corresponding to the case where the connection is refused. Note that if we had used a process to model each Service User instead of using the Simulator feed command, the SU process would have transmitted L_ReleaseReq to block DLCb; then the Simulator would have detected an exception because the s