ReqSetup(),ResSetup(_,_,Status("Cancelled")),ReqWork()
Two traces match if they have a common instance. Notice that two traces that
have no placeholders match if and only if they are equal. For example, the trace
ReqSetup(1,2),ResSetup(1,_,Status("Completed")),ReqWork(_,3)
is an instance2 of the trace
ReqSetup(1),ResSetup(_,_,Status("Completed")),ReqWork()
as well as the trace
ReqSetup(_,2),ResSetup(1),ReqWork(_,3)
Notice that none of the above traces are concrete.
14.3.1 Trace intersection
A desired property of M1 ?—M2 is that the set of all traces of M1 ?—M2 is the
intersection of the set of all traces of the loop extension of M1 for A2, say M1
, and
the set of traces of the loop extension of M2 for A1, say M2
. A reason why this
property is important is that it makes it possible to do compositional reasoning over
the traces in the following sense. If all traces of M1
satisfy a property p and all
traces of M2
satisfy a property q, then all traces of M1 ?—M2 satisfy both properties
p and q. A sufficient condition for the trace intersection property to be true is if M1
and M2 don??™t share any state variables.
LetM1 be the setup model program in Figure 14.15 and letM2 be the cancellation
model program in Figure 14.7. First, let us see how the model program M1 ?—M2 is
constructed. The state variables ofM1 ?—M2 is the union of the state variables ofM1
andM2.
Pages:
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322