Consider the concurrent program consisting of the two processes shown below:

// Process 1 // Process 2 while(true) { while(true) { r1 = turn; r2 = turn; if (!r1) { if (r2) { <crit1>; <crit2>; turn = true; turn = false; } } } } // Shared datastructures boolean turn = r1 = r2 = false;

States are described by the following propositional variables:

- t for turn equals true;
- r
_{1}for r1 equals true; - r
_{2}for r2 equals true; - c
_{1}for process 1 is in its critical section; - c
_{2}for process 2 is in its critical section.

The starting state is s_{0}
= (¬t, ¬r_{1}, ¬r_{2}, ¬c_{1}, ¬c_{2}). Each process
performs the following sequence of actions: copy the value of variable turn into
its local variable r1 or r2;
evaluate the if statement; depending on the outcome, either do its
critical section and set turn to be
true (false), or return to the first step. Actions can be arbitrarily
interleaved. As usual we assume that assignment is an atomic operation.
If we are in a state where for example r_{1}
holds and t does not and process
1 executes atomic action r1 = turn we
make a transition to a state where
¬r_{1} holds. In this example we can also assume that
evaluating the if statement
is an atomic operation since the value of the local variable can't be
changed by another process. So if we are in the state where ¬r_{1} holds and process
1 evaluates the condition of its if
statement, we move to a state where c_{1}
is true.

**Questions:**

- Draw the state transition diagram.
- Write a CTL formula expressing the following property: it is impossible that r1 is true and process 1 is in its critical section. Is this formula true at the start state of the transition system you drew? Justify your answer using the truth definition for CTL formulas.
- Write a CTL formula expressing the property of non-strict scheduling: process 1 and process 2 don't always take turns at entering critical section, but instead for example process 1 can go into critical section several times in a row. (Hint: you may need to use Until operator.) Is this formula true at the start state of the transition system you drew? Justify your answer using the truth definition for CTL formulas.