[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Fox, goose and beans (rivercross) puzzle in TLA

• From: Dmitry Kuvayskiy <dmitry.k...@xxxxxxxxx>
• Date: Wed, 3 Apr 2013 05:57:29 -0700 (PDT)
• User-agent: G2/1.0

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