It is also a trace of SetupC because it is an instance
of the trace
ReqSetup()
ResSetup(_,_,STATUS("Completed"))
ReqWork()
Cancel()
ResWork()
14.3.2 Crosscutting
It is often easier to write separate model programs for different features and to
use the product construction to create the product rather than creating the product
directly. When creating the product directly, one has to take into account all the
possible combinations of the state variables from the different features. Moreover,
the full model program can be developed incrementally by adding more feature
model programs without having to change the existing ones.
Another advantage of creating separate model programs is that it helps to separate
crosscutting concerns by using distinct state variables and in this way simplifies
compositional reasoning. Imagine, for example, a model program with a single
feature that includes all the features of SP. When doing so, it is natural to introduce
a single state variable that maps request IDs to compound ???request info??? values. A
request info describes the relevant information about a pending request in a given
state, namely the command associated with it, the mode of the request, and the
number of requested credits. Separate analysis of the features now requires fairly
sophisticated analysis techniques because the state information about the different
features is stored in a shared state variable.
Pages:
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324