Fox, goose and beans (rivercross) puzzle in TLA

[Dmitry Kuvayskiy <dmitry.k...@xxxxxxxxx>]

Hello!

I am studying TLA+ and PlusCal and below is one of my first
specifications (in TLA+). I wonder if any guru could evaluate how
idiomatic my code is and what could be done better. (The code works, I
just want to know how good it is.)
The puzzle I tried to solve is "Fox, goose and beans" classic -- how
can a farmer cross the river with a condition that he can take on a
boat only one object at a time. For more info see
http://en.wikipedia.org/wiki/Fox,_goose_and_bag_of_beans_puzzle .

Below is the code. In a model I specify my invariants "TypeInv" and
"NotSolved", also I add "Safety(LeftShore) /\ Safety(RightShore)" as a
state constraint.
Any comments are appreciated, thanks in advance.

------------------------------- MODULE shores
-------------------------------

VARIABLES LeftShore, RightShore

Objects == {"Farmer", "Fox", "Goose", "Beans"}

Init == /\ LeftShore = Objects
        /\ RightShore = {}

TypeInv == /\ LeftShore \in SUBSET Objects
           /\ RightShore \in SUBSET Objects

Safety(Shore) == \/ "Farmer" \in Shore
                 \/ /\ \neg ({"Fox", "Goose"} \subseteq Shore)
                    /\ \neg ({"Goose", "Beans"} \subseteq
Shore)

toRight(Obj) ==  /\ Obj \in SUBSET LeftShore
                 /\ RightShore' = RightShore \cup Obj
                 /\ LeftShore'  = LeftShore \ Obj

toLeft(Obj) ==  /\ Obj \in SUBSET RightShore
                /\ RightShore' = RightShore \ Obj
                /\ LeftShore'  = LeftShore \cup Obj

Next == \/ toRight({"Farmer"})
        \/ toRight({"Farmer", "Fox"})
        \/ toRight({"Farmer", "Goose"})
        \/ toRight({"Farmer", "Beans"})
        \/ toLeft({"Farmer"})
        \/ toLeft({"Farmer", "Fox"})
        \/ toLeft({"Farmer", "Goose"})
        \/ toLeft({"Farmer", "Beans"})

Spec == Init /\ [][Next]_<<LeftShore, RightShore>>

NotSolved == Objects # RightShore