123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354 |
- 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
- )
|