River.tla

--------------------------- MODULE River ---------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache

VARIABLE
  (*
    @type: Set(Str);
  *)
  origin

VARIABLE
  (*
    @type: Set(Str);
  *)
  boat

VARIABLE
  (*
    @type: Set(Str);
  *)
  destination

(*
  @type: ((Set(Str)) => Bool);
*)
isSafe(location) ==
  ({ "goat", "cabbage" } \subseteq location => "farmer" \in location)
    /\ ({ "goat", "wolf" } \subseteq location => "farmer" \in location)

(*
  @type: (() => Bool);
*)
init ==
  origin' := { "wolf", "goat", "cabbage", "farmer" }
    /\ boat' := {}
    /\ destination' := {}

(*
  @type: (() => Bool);
*)
embarkOrigin ==
  "farmer" \in origin
    /\ (\E toEmbark \in {
      s \in SUBSET origin:
        Cardinality(s) <= 2 /\ "farmer" \in s
    }:
      isSafe((origin \ toEmbark))
        /\ boat' := (boat \union toEmbark)
        /\ origin' := (origin \ toEmbark)
        /\ destination' := destination)

(*
  @type: (() => Bool);
*)
disembarkDestination ==
  "farmer" \in boat
    /\ boat' := {}
    /\ destination' := (destination \union boat)
    /\ origin' := origin

(*
  @type: (() => Bool);
*)
embarkDestination ==
  "farmer" \in destination
    /\ (\E toEmbark \in {
      s \in SUBSET destination:
        Cardinality(s) <= 2 /\ "farmer" \in s
    }:
      isSafe((destination \ toEmbark))
        /\ boat' := (boat \union toEmbark)
        /\ destination' := (destination \ toEmbark)
        /\ origin' := origin)

(*
  @type: (() => Bool);
*)
disembarkOrigin ==
  "farmer" \in boat
    /\ boat' := {}
    /\ origin' := (origin \union boat)
    /\ destination' := destination

(*
  @type: (() => Bool);
*)
safety == isSafe(origin) /\ isSafe(boat) /\ isSafe(destination)

(*
  @type: (() => Bool);
*)
noSolution == origin /= {} \/ boat /= {}

(*
  @type: (() => Bool);
*)
consistency ==
  origin \intersect destination = {}
    /\ origin \intersect boat = {}
    /\ boat \intersect destination = {}

(*
  @type: (() => Bool);
*)
step ==
  embarkOrigin
    \/ disembarkDestination
    \/ embarkDestination
    \/ disembarkOrigin

================================================================================