Let us call the state variable ofM1 setupMode that may take one of the three
2 It is in fact the most general common instance of both traces; i.e., any other instance of both
traces is also an instance of the most general common instance.
Advanced Topics 243
values "Inactive", "Activating", or "Active". Initially the value of setupMode is
"Inactive". The guarded update rule for ResSetup in M = M1 ?—M2 can be given
as
[Action("ResSetup(m,_,s)")]
public static void ResSetup(int m, Status s)
{
mode = mode.RemoveKey(m);
if (s == Status.Cancelled)
setupMode = "Inactive";
else
setupMode = "Active";
}
public static bool ResSetupEnabled(int m, Status s)
{
return
setupMode == "Activating" &&
mode.ContainsKey(m) &&
(s != Status.Cancelled || mode[m] == Mode.CancelRequested);
}
The guarded update rule for ResWork in M1 ?—M2 can be given as
[Action("ResWork(m,_,s)")]
public static void ResWork(int m, Status s)
{
mode = mode.RemoveKey(m);
}
public static bool ResWorkEnabled(int m, Status s)
{
return
setupMode == "Active" &&
mode.ContainsKey(m) &&
(s != Status.Cancelled || mode[m] == Mode.CancelRequested);
}
In M1 ?—M2 the guarded update rule of Cancel is the same as in M2, because in M1
Cancel is a self-loop. The following is a trace of M1 ?—M2:
ReqSetup(3)
ResSetup(3,_,STATUS("Completed"))
ReqWork(7)
Cancel(7)
ResWork(7,_,STATUS("Completed"))
244 Compositional Modeling
It is clearly also a trace of M2.
Pages:
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323