[Z] Solving a simple puzzle in Z by CTL model checking

For the same previous river crossing puzzle, it can be modeled in Z and solved in ProB as well.

The Z program

The LaTeX Source

\documentclass{article}
\usepackage{fuzz}

\begin{document} 

\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{zed}
    State \defs [~ ls: \power~FR; boat: \power~FR; rs: \power~FR | 
       (\#~boat \leq 2) \land 
       (
          (
             (\#~(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)
       )
    ~] \\
    Init \defs [~ State' | ls' = FR \land rs' = \emptyset 
        \land boat' = \emptyset ~] \\
    % move two creatures frm LS to RS
    Move2 \defs [~ \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
    Move1 \defs [~ \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
    LoadBack \defs [~ \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 
    LoadAll \defs [~ \Delta State | 
        (\#~boat = 2) \land ls = \emptyset \land
        boat' = \emptyset \land rs'=rs \cup boat 
    ~] \\
\end{zed}
\end{document}

Solving by CTL model checking in ProB

Check CTL formula: "AG(not e(LoadAll))",  and a counterexample found. This is one of the solutions.