[Circus] Modelling a simple puzzle in Circus

For the same river crossing puzzle (foxes and rabbits), it can be modeled in Circus as well.

The diagram below is the program written in Circus.

The Circus Crossing Program

Here's the latex source.

\documentclass{article}
%
\usepackage{circus}
%
\begin{document}

\begin{zsection}
    \SECTION\ CrossingPuzzle \parents\ circus\_toolkit
\end{zsection}

\begin{zed}
    DFR ::= F1 | F2 | F3 | R1 | R2 | R3 | Z \\
    F == \{F1, F2, F3\} \\
    R == \{R1, R2, R3\} \\
    FR == F \cup R \\
\end{zed}

\begin{circus}
    \circchannel\ move2: FR \cross FR \\ 
    \circchannel\ move1: FR \\ 
    \circchannel\ load: FR \\ 
    \circchannel\ escape \\
\end{circus}

\begin{circus}
    \circprocess\ Cross \circdef \circbegin \\
        \t1 \circstate\ State == [~ ls: \power~FR; boat: 
            \power~FR; rs: \power~FR | (\#~boat \leq 2) \land 
            % for ls or rs, if there exists rabbits, the number
            % of foxes shall be less than the number of rabbits
            (
              (
                (\#~(ls \cap F) \leq \#~(ls \cap R)) 
                \land (\#~(ls \cap R) > 0)
              ) \lor (\#~(ls \cap R) = 0)
            ) \land
            (
              (
                (\#~(rs \cap F) \leq \#~(rs \cap R))
                \land (\#~(rs \cap R) > 0)
              ) \lor (\#~(rs \cap R) = 0)
            )
        ~] \\
        \t1 Init == [~ (State)' | ls' = FR \land rs' = \emptyset 
            \land boat' = \emptyset ~] \\
        % move two creatures frm LS to RS
        \t1 Move2 == [~ \Delta State; c1?: FR; c2?: FR | 
            c1? \in ls \land c2? \in ls \land 
            c1? \neq c2? \land
            boat = \emptyset \land
            ls' = ls \setminus \{c1?, c2?\} \land
            boat' = \{c1?, c2?\} \land rs'=rs
        ~] \\
        % move one creature frm LS to RS because there is a creature on boat
        \t1 Move1 == [~ \Delta State; c?: FR | 
            c? \in ls \land (\#~boat = 1) \land
            ls' = ls \setminus \{c?\} \land
            boat' = boat \cup \{c?\} \land rs'=rs
        ~] \\
        % load one and back another
        \t1 LoadBack == [~ \Delta State; c?: FR | 
            c? \in boat \land (\#~boat = 2) \land
            ls \neq \emptyset \land
            ls' = ls \land boat' = boat \setminus \{c?\} \land 
            rs'=rs \cup \{c?\}
        ~] \\
        % load two 
        \t1 LoadAll == [~ \Delta State | 
            (\#~boat = 2) \land ls = \emptyset \land
            boat' = \emptyset \land rs'=rs \cup boat 
        ~] \\
        \t1 AMove \circdef (
            (\lcircguard boat = \emptyset \rcircguard \circguard 
               move2?c1?c2 \then \lschexpract Move2 \rschexpract) 
            \extchoice 
            (\lcircguard \#~boat = 1 \rcircguard \circguard 
               move1?c \then \lschexpract Move1 \rschexpract) 
            \extchoice 
            (\lcircguard ls \neq \emptyset \land \#~boat = 2 \rcircguard 
               \circguard load?c \prefixcolon (c \in boat) \then 
               \lschexpract LoadBack \rschexpract) 
            \extchoice 
            (\lcircguard ls = \emptyset \land \#~boat = 2 \rcircguard 
               \circguard \lschexpract LoadAll \rschexpract)
            ) \\
        \t1 AEnd \circdef (\lcircguard (ls = \emptyset \land boat = \emptyset) 
            \rcircguard \circguard escape \then \Skip) \\
        %
        \t1 \circspot \lschexpract Init \rschexpract \circseq (
            \circmu X \circspot (((AMove) \circseq X) \extchoice AEnd)) \\
    \circend
\end{circus}

\end{document}