uni/fmi/fmi23block4/ex3.a.smv

MODULE passenger(on_boat)
  VAR
    crossed : boolean;
  ASSIGN
    init(crossed) := FALSE;
    next(crossed) := on_boat ? !crossed : crossed;

MODULE main
  VAR
    -- selected passenger encodes which of the passengers will be crossed next
    -- selection happens as the boat returns, we could see this as the ferryman deciding what to do next while rowing back
    selected_passenger : {w, g, c, none};

    -- boat crossed encodes the boat is currently at the origin (not crossed) or at the destination (crossed)
    boat_crossed : boolean;

    -- these three passengers each have their own internal crossed variable (with the same meaning)
    -- they internally check whether they are on the boat and if so, their crossing value toggles
    wolf : passenger(selected_passenger = w);
    goat : passenger(selected_passenger = g);
    cabbage : passenger(selected_passenger = c);
  ASSIGN
    init(boat_crossed) := FALSE;

    -- the boat always toggles its crossing, representing the back and forth control flow of the boat
    next(boat_crossed) := !boat_crossed;

    -- this statement essentially encodes a set of follow-up states
    -- the only passengers which can be selected for crossing are those who have the same crossing value as the next boat crossing value
    -- in essence, due to this statement, the boat cannot take a passenger from the origin to the destination while at the desination or vice-versa
    next(selected_passenger) := {
      next(boat_crossed) = wolf.crossed ? w : selected_passenger,
      next(boat_crossed) = goat.crossed ? g : selected_passenger,
      next(boat_crossed) = cabbage.crossed ? c : selected_passenger,
      selected_passenger, none
    };
  DEFINE
    -- this is a simple definition for the goat being eaten by the wolf, looking at the crossed values of the boat, the wolf and the goat
    wolf_eats_goat := wolf.crossed = goat.crossed &
                      wolf.crossed != boat_crossed;
    -- same but for the cabbage being eaten by the goat
    goat_eats_cabbage := goat.crossed = cabbage.crossed &
                         goat.crossed != boat_crossed;
    -- this is a simple definition for all passengers being crossed, which is really the end state of our puzzle
    all_crossed := wolf.crossed &
                   goat.crossed &
                   cabbage.crossed;

  -- this spec is explained in detail in the trace provided in `ex3.a.out`
  LTLSPEC !(
    G (!wolf_eats_goat & !goat_eats_cabbage) &
    F all_crossed
  )