It is specified how the given message affects the behavior of subsequent messages. Firstly, subsequent messages enabled, i.e., will terminate normally, and disabled disabled, i.e., will terminate abnormally, if invoked, are specified.
This is specified in IBDL using the enables and
disables clauses with formulas of the form
(enables | disables)
g(y1, ..., yk) if
p(xi1, ..., xil, y1, ..., yk)
where g is a message of the same interface3,
xij is in
,
y1, ..., yk,
are new variables, p is a predicate.
The above formula appearing in a enables (or disables) clause defines the set of all messages g(d1, ..., dk) which are enabled (or disabled), after a particular invocation m(c1, ..., cn), if the condition p(ci1, ..., cil, d1, ..., dk) evaluates to true.
A message that is neither in the enables nor in the disables set will continue to exhibit the same behavior as it did before the message m(c1, ..., cn).
A specification for a message is not well-formed if it enables and disables a message at the same time.