## Solutions

### Peterson's algorithm

We only did Peterson's algorithm in the second lab. (I will briefly go over the temporal formula's next Tuseday). Here's the algorithm:

fair process thread \in Threads variable other = CHOOSE t \in Threads : t /= self begin P1: flag[self] := TRUE; P2: turn := other; P3: await ~flag[other] \/ turn = self; CS: skip; P4: flag[self] := FALSE; P5: goto P1 end process;

### Ferryman

By defining some auxiliary values, we can simplify the algorithm significantly. We also include the "ferryman" as part of the goods, so he can pick himself in order to cross on his own. Here's a polished version of what we had on Tuesday, but the flaw is still there!

------------------------------ MODULE ferryman ------------------------------ (*--algorithm ferryman variable pos = [item \in goods |-> "left"] define goods == {"goat", "cabbage", "wolf", "ferryman"} flip(side) == CASE side = "left" -> "right" [] side = "right" -> "left" currentside == pos["ferryman"] otherside == flip(currentside) currentside_items == {it \in goods : pos[it] = currentside} Safe == \/ pos["goat"] = pos["wolf"] \/ pos["goat"] = pos["cabbage"] => pos["ferryman"] = pos["goat"] Solved == \A item \in goods : pos[item] = "right" Solution == []Safe /\ <>Solved ThereIsNoSolution == ~Solution end define begin Ferry: with item \in currentside_items do pos[item] := otherside end with; P1: pos["ferryman"] := otherside; goto Ferry end algorithm*) =============================================================================

If we try to use TLA+ to disprove that ThereIsNoSolition, we find that TLA fails; indeed, this algorithm doesn't have a solution. The problem is actually worth noting. I spoke at length about these labels during the lecture, so we all (even me!) probably understand that adding the label `P1`

will no longer make the assignments atomic. (We had to add the label because we can't assign twice to the same struct in an atomic section.) Here's what I did not consider: these assignment actually have a meaning in the domain that we're modelling. *It really does matter whether the ferryman is on the boat together with the goods or swims along and arrives a while after!* Mistaken assumptions about atomicity requirements are a very common cause of errors; that's why I made this mistake. ;) Anyway, we can fix it by parallel assignment:

begin Ferry: with item \in currentside_items do pos[item] := otherside || pos["ferryman"] := otherside end with; goto Ferry

If you run this, you should find a solution. When I try this, the counter-example is a solution where after having reached the final state, the ferryman goes back with the goat and stutters on the other side, probably admiring his solution from afar. This satisfies the formula. If we want him to stay at the solution, we can use `Solution == []Safe /\ <>[]Solved`

.