Re: [tlaplus] Fox, goose and beans (rivercross) puzzle in TLA

[Stephan Merz <stepha...@xxxxxxxxx>]

Dear Dmitry,

your representation looks fine to me. I have two remarks:

1. Instead of using your Safety predicate as a state constraint, you could have adapted the definition of toRight to include the conjunct Safety(RightShore'), and similarly for toLeft in order to ensure that the model checker only generates safe configurations (instead of ignoring unsafe ones in the state space).

2. The sequentialization of toLeft and toRight is somewhat implicit, based on the fact that the farmer changes shore at every step, and therefore you cannot perform, say, two toLeft actions in sequence. Alternatively, you could record the position of the farmer in a state variable (and leave it out of the set of objects transported), writing something like

toRight(Obj) ==
  /\ farmer = "left"
  /\ farmer' = "right"
  /\ LeftShore' = LeftShore \ Obj
  /\ RightShore' = RightShore \cup Obj

In this way, I find it a little more obvious that the two actions must alternate. Of course, this is a matter of taste.

Best regards,

Stephan

On Apr 3, 2013, at 2:57 PM, Dmitry Kuvayskiy <dmitry.k...@xxxxxxxxx> wrote:

> 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
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
> 
>