It is sometimes easier to reason about properties of composition when the action
vocabularies of the composed model programs are the same. In order to do so we
use a simple transformation. The effect of interleaving for nonshared actions is
achieved by treating actions not in the vocabulary as self-loops. We transform a
model program M with respect to a set of action symbols a1, . . . , ak into a new
model program called a loop extension of M for a1, . . . , ak, as follows. For each
action symbol ai not in the action vocabulary ofM, add a trivial guarded update rule
for ai whose enabling condition is true, and whose update rule produces no state
updates, that is, every action whose symbol is ai produces a self-loop in all states of
M. In reality, this transformation is not done explicitly but is built into the product
operation of model programs.
For example, consider the setup model program in Figure 14.15. The loop extension
of the setup model program for Cancel, say SetupC, has the additional
transitions
t("Inactive", Cancel(), "Inactive")
t("Activating", Cancel(), "Activating")
t("Active", Cancel(), "Active")
The arity of an action (symbol) is the number of arguments or parameters that
it takes. When describing a model program it is often convenient to omit trailing
parameters of an action that are not referenced by its guarded update rule.
Pages:
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320