Look again at the guarded actions of program 7b which are as follows:
- st&!o1 => next(l1) = true
- o1&st => next(l2) = true
- st&!o2 => o1 = true
- o1&l1&!o1|l1&!o1 => next(l1) = true
- o1&o1&l1|l2&!o1 => next(l2) = true
- l2&!o1 => o2 = true
In the first step, we have st=true & l1=false & l2=false, and therefore, the guarded actions become
- !o1 => next(l1) = true
- o1 => next(l2) = true
- !o2 => o1 = true
Now, if we start with o1=o2=⊥, then all guards are ⊥, so we don't know anything. However, we see that there is no guarded action on o2, so that o2 is determined by the reaction to absence. However, that is only seen *after* the first micro step where o1=o2=⊥ holds. This gives us then a reason to change the value of o2 from ⊥ to false (reaction to absence), and this triggers then !o2 => o1 = true which sets o1 true (in the must and can set). This changes then the value of o1 from ⊥ to true.