When a combined action executes, all
of its update rules execute and all of its parameters are used. It is the actions (the
Advanced Topics 227
namespace SP
{
[Feature]
class Credits
{
static Set
window = new Set(0);
static int maxId = 0;
static Map requests = Map.EmptyMap;
[Action("ReqSetup(m,c)")]
[Action("ReqWork(m,c)")]
static void Req(int m, int c)
{
requests = requests.Add(m, c);
window = window.Remove(m);
}
[Requirement("Section ...: Message IDs must not be repeated")]
static bool ReqEnabled(int m){return window.Contains(m);}
[Requirement("Section ...: Requested credits must be > 0.")]
static bool ReqEnabled(int m, int c){return c > 0;}
[Action("ResSetup(m,c,_)")]
[Action("ResWork(m,c,_)")]
public static void Res(int m, int c)
{
for (int i = 1; i <= c; i++) window = window.Add(maxId + i);
requests = requests.RemoveKey(m);
maxId = maxId + c;
}
[Requirement("Section ...: Must be a pending credit request")]
static bool ResEnabled(int m){return requests.ContainsKey(m);}
[Requirement("Section ...: Must not grant more credits than requested")]
static bool ResEnabled(int m, int c){return requests[m] >= c;}
[AcceptingStateCondition]
static bool IsAcceptingState() { return requests.IsEmpty; }
[StateInvariant("Section ...: Client must have enough credits")]
static bool ClientHasEnoughCredits()
{
if (requests.
Pages:
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304