question 7b

Question

I understand the answer to 7a now but I still have questions about 7b.

Why don't we put emit(o1) in step 0 Dmust since at step 0 we have o1 = true? And why do we never put E(o1)=1 if o1 = true?

Answer 1

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.