Count == 0) return window.Count > 0;
else return true;
}
}
}
Figure 14.1. Credits feature model program.
228 Compositional Modeling
terms) that are considered when combining actions, not the methods (the C# code).
Section 14.3 (below) explains in detail how actions are combined.
The action ReqSetup(m,c), where m is a message ID and c a requested number of
credits, has an update rule, given by the method Req, that records in the state variable
requests that m has an outstanding credit request for c credits, and removes m from
the window. The guard of this update rule is defined by the conjunction of the two
predicates (Boolean methods) named ReqEnabled (recall that an action method is
enabled only when all of its enabling conditions are true). The first predicate requires
m to appear in the window, and the second one requires c to be positive.
A Requirement attribute associated with each of the predicates provides a connection
between the model program and the corresponding section or paragraph in
the natural language document, and motivates the split of the enabling condition
into two predicates, rather than just one predicate.
The action ResSetup(m,c, ), where m is a message ID and c is a granted number
of credits, has an update rule given by the action method Res. It adds to the window
the set of new IDs {maxId + 1, . . . , maxId + c}, which is empty if c is zero, records
that the new maximum ID is maxId + c and removes m from the pending requests
map.
Pages:
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305