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
https://es.cs.uni-kl.de/teaching/mbes/exams/2022.08.04.mbes/2022.08.04.mbes.solutions.pdf

Could you explain the answers from exercise 7? In question b, why isn't emit(o2) in Cmust since i=1? And in question a and b why do we stop after step 0?
in * TF "Emb. Sys. and Rob." by (460 points)

1 Answer

0 votes

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.

by (170k points)
question 7b

Related questions

0 votes
1 answer
asked Mar 23, 2023 in * TF "Emb. Sys. and Rob." by lu (460 points)
+1 vote
1 answer
asked Apr 3, 2021 in * TF "Emb. Sys. and Rob." by SL (180 points)
+1 vote
1 answer
Imprint | Privacy Policy
...