For
example, in the sample protocol model, the arity of a cancel action is one, the arity
of a request action is two, and the arity of a response action is three. Given an
action symbol f with arity k we often use the abbreviated form f (t1, . . . , ti) for
some i, 0 ?‰¤ i ?‰¤ k, to stand for the term f (t1, . . . , ti , _, . . . , _) with k ??’ i trailing
underscores called placeholders.1 For example, Cancel() stands for Cancel( ). An
instance of an action with placeholders is a replacement of some (or none) of the
placeholders with concrete values.Atrace with placeholders is a sequence of actions
with placeholders and an instance of a trace with placeholders is an instantiation of
some of the placeholders in it. We often say trace to mean a trace that may contain
1 Formally, each occurrence of a placeholder represents a fresh logic variable. A term without
logic variables is called ground.
242 Compositional Modeling
placeholders.We say that an action or a trace is concrete when it has no placeholders.
If a trace of a model program has placeholders, then any instance of it is a trace of
that model program as well, because a placeholder indicates that the corresponding
argument has no behavioral significance with respect to this model program.
For example,
ReqSetup(),ResSetup(_,_,STATUS("Completed")),ReqWork()
is a trace of the setup model program, whereas
ReqSetup(),ResSetup(),ReqWork()
is not, because the following instance of it is not a trace of the setup model program.
Pages:
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321