Exercise 3A: Write a TLA specification in a similar way to the previous ones which defines a program consisting of the two processes P0 and P1 executing the Peterson algorithm for two-process mutual exclusion.

The algorithm again: flag: array [0..1] of 0..1 turn: {a, b}

Program 0

loop

1. flag [0] = 1;

2. turn = b;

3. while flag [1] = 1 and turn = b do wait;

4. critical section;

5. flag [0] = 0 endloop Program 1

loop

1. flag [1] = 1;

2. turn = a;

3. while flag [0] = 1 and turn = a do wait;

4. critical section;

5. flag [1] = 0 endloop