/* Run instructions:
 * prom2lts-seq --ltl=river.ltl --trace=solution.gcf river.prm
 * ltsmin-printtrace solution.gcf | grep -vE "guard|pc|action|ltl|buchi"
 */

bool man, wolf, goat, cabbage;

init {
    do
    :: man == wolf -> atomic { man = !man; wolf = !wolf }
    :: man == goat -> atomic { man = !man; goat = !goat }
    :: man == cabbage -> atomic { man = !man; cabbage = !cabbage }
    :: true -> man = !man
    od
}