There are different ways to answer that question; the preferred one in the exam is to reason with the SOS rules and the must and can sets of actions. Below, I am using the compilation to guarded actions for the same.
In question 7a, we stop after step 0 since the exam task just asks for the result obtained for inputs i=false and i=true in the first reaction step only. So, we do not consider the further execution in 7a.
The program in 7a is as follows:
module P7a(event ?i,o1,o2) {
immediate abort {
if(i) emit(o2);
if(!o2) emit(o1);
if(o1) emit(o2);
} when(!o2);
}
For the program in 7a, we obtain the following guarded actions:
- i&o2&st => o2 = true
- !o2&o2&st => o1 = true
- o1&o2&st => o2 = true
So, if st=true and i=false, we have
- false => o2 = true
- !o2&o2 => o1 = true
- o1&o2 => o2 = true
So, neither o1 nor o2 can be determined which means that their emit statements are in the can sets, but not in the must sets. And if st=true and i=true, we have
- o2 => o2 = true
- !o2&o2 => o1 = true
- o1&o2 => o2 = true
which again does neither give values for o1 nor for o2 in the causality analysis.
In problem 7b, there is no input, so I don't understand your question. We consider
module P7b(event o1,o2) {
if(!o2) emit(o1);
weak suspend {
l1:immediate await(o1);
l2:pause;
if(!o1) emit(o2);
} when(!o1);
}
which has the following guarded actions:
- 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
- !o1 => next(l1) = true
- o1 => next(l2) = true
- !o2 => o1 = true
Since there is no action for setting o2 at this point of time, o2 becomes false by the reaction to absence. Hence, by "!o2 => o1 = true", o1 becomes true. We therefore execute the following in the first point of time
- next(l2) = true
- o1 = true
So, at time t=1, we have st=false & l1=false & l2=true, so that we have
- false => next(l1) = true
- false => next(l2) = true
- false => o1 = true
- false => next(l1) = true
- !o1 => next(l2) = true
- !o1 => o2 = true
Now, there is no action on o1, so that it becomes false by the reaction to absence. Because of this, we set o2=true, and next(l2)=true.
