Süsteemide modelleerimine 2018/19 sügis

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.