We consider the following module:
module P(event bool ?a,?b,o1, bool o2)
{
loop {
{
l0: pause;
if(b)
emit next(o1);
l1: pause;
if(b)
emit(o2);
} || {
if(a) {
l2: pause;
emit(o1);
}
}
}
}
There are many ways how the control-flow actions can be computed. The best way would be to follow the symbolic compilation as explained in the course. This should generate the following guarded actions:
control flow:
st => next(l0) = true
a&st => next(l2) = true
(l1&l2|l2&!(l0|l1)|l1&!l2) => next(l0) = true
l0 => next(l1) = true
a&(l1&l2 | l2&!(l0|l1)|l1&!l2) => next(l2) = true
data flow:
b&l0 => next(o1) = true
b&l1 => o2 = true
l2 => o1 = true
The ones you mention are among the ones above. How are they explained?
If you consider l0, it is entered whenever the loop body is started, i.e., when the loop is started and when the loop body terminates (and is restarted). If the loop is initially started, we have st (and all other labels are false), so that explains the guarded action st => next(l0) = true.
To determine when the loop body terminates, we have to consider the termination of a parallel statement. Recall that S1||S2 terminates if term(S1)&!insd(S2) | !insd(S1)&term(S2) | term(S1)&term(S2) holds. We moreover have term(S1) = l1, term(S2) = l2, insd(S1)=l0|l1 and insd(S2) = l2, so that
term(S1||S2) = l1&!l2 | !(l0|l1)&l2 | l1&l2
holds. That explains the guarded action (l1&l2|l2&!(l0|l1)|l1&!l2) => next(l0) = true which is just term(S1||S2) => next(l0) = true.
For the guarded action on l2, note that it is entered at starting time when additionally a holds, which yields guarded action a&st => next(l2) = true. Moreover, l2 is entered if the loop reiterates and a holds, i.e., if a&term(S1||S2) holds. Based on the above results, this yields a&(l1&l2 | l2&!(l0|l1)|l1&!l2) => next(l2) = true.
