l, but the difference is that in S1, the expression sender in process client contains the Pid of process instance server(1) (because 190 Validation of Communications Systems with SDL it has just consumed the signal echo_reply), while in S8, sender contains the Pid of process instance client(1) (because it has just consumed the timer signal T1). Also, a PING sequence has been simulated in interactive mode before starting the exhaustive simulation; otherwise we get two more states where the expression sender contains Null as no signal has been consumed yet. 7.2.2 Exhaustive simulation of counters To show a larger states graph, we simulate an SDL model containing incremented variables. 7.2.2.1 A model with counters Figure 7.11 shows an SDL model containing two identical processes count1 and count2, based on the block type counter. system count block counters counters count1 : counter count2 : counter counter Figure 7.11 The SDL system count Figure 7.12 shows the contents of process type counter: variable n is initialized to 1, then each time an input NONE is performed (spontaneous transition), n is incremented. When n is greater than 100, n is set back to 1, and the count starts again. process type counter ready n Integer; n:= 1 ready n:=n+1 <= 100) ready Figure 7.12 The process type counter 7.2.2.2 Exhaustive simulation of model count As expected, running the exhaustive simulation on model count generates 10000 global states: each process count1 and count2 has 100 states; as they are not synchronized, the number of global states is the product 100 X 100. The tool used here is the ObjectGeode Simulator. Exhaustive Simulation 191 count1 count2 count1 : input NONE count1 : input NONE count1 : input NONE n = 100 count2 : input NONE n = 100 count2 : input NONE count1 : input NONE n =99 count2 : input NONE n = 100 S10000 Figure 7.13 Partial states graph of model count Using the two textual files optionally generated by the Simulator, we have manually drawn a part of the reachable states graph of the SDL model, as shown i