Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
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?
related to an answer for: Quartz (Causality Analysis)
in * TF "Emb. Sys. and Rob." by (460 points)

1 Answer

+1 vote
 
Best answer

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.
by (170k points)
selected by
Quartz (Causality Analysis)

Related questions

0 votes
1 answer
0 votes
1 answer
+1 vote
1 answer
asked Sep 12, 2018 in * TF "Softw.-Eng." by davidschulz (410 points)
0 votes
1 answer
Imprint | Privacy Policy
...