For each shared resource R the multiplexer
records the expected usage count kR that is initially 0. An event E is dequeued from
some event queue, if
1. E is not a resource usage event, or
2. E is a resource usage event R(k) for some shared resource R, and k = kR. In
this case, kR is incremenetd by one.
274 Reactive Systems
The stepper consumes the events produced by the multiplexer, filters out the
resource usage events, and maps all the other events into observable actions that are
enqueued into the observation queue of the conformance tester.
Consider the example with two agents A1 and A2 depicted in Figure 16.7. A
possible sequence of events that are entered into the observation queue is
(a, e, b, c, f, g, d)
An asynchronous stepper can use a multiplexer to enqueue events into the observation
queue of the conformance tester. For example, in the stepper of the SP
server shown in Figure 16.5, if the different requests to the server always start different
threads that may share resources and the server supports per-thread response
handlers, then multiplexing of the thread-based events could be integrated into the
responder.
16.7 Exercises
1. Consider the revision control system model program in Chapter 10. What
actions are controllable and what actions are observable? Motivate.
2. Extend the sample SP server and stepper to handle cancellation and run ct to
experiment with it.
Pages:
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362