We consider in that exam problem the following program
module P7a(event ?i,o1,o2) {
immediate abort {
if(!o2) emit(o1);
if(i) l:pause;
if(!o1) emit(o2);
} when(!o1);
}The program has the following guarded actions:
- o1&i&o1&st => next(l) = true
- !o2&o1&st => emit(o1)
- !o1&!i&o1&st => emit(o2)
- !o1&o1&l => emit(o2)
At initial time, we have st=1 and l=0 so that the guarded actions are reduced to the following ones
- o1&i&o1 => next(l) = true
- !o2&o1 => emit(o1)
- !o1&!i&o1 => emit(o2)
In two-valued logic, we could conclude that !o1&!i&o1 is false so that emit(o2) would not be added to the can set. In three-valued logic, however, this is not the case: If o1=⊥ and i=0 holds, then the guard !o1&!I&o1 evaluates to ⊥. Now, recall that the can-set is the set of actions whose guards are not false, and that the must set is the set of actions whose guards are true. As our guard is ⊥, it is neither true nor false, hence, the action belongs to the can set, but not to the must set.
