nusmv - 我在这个“？？”中缺少什么 标签？

Question

我在以下代码中缺少什么？我正在尝试实施摆渡人解决方案。你会建议如何填写？部分？谢谢！

MODULE main

VAR
    ferryman: boolean;
    goat: boolean;
    cabage: boolean;
    wolf: boolean;
    carry: {g, c, w, 0};
    
ASSIGN
    init(ferryman) := FALSE;
    init(goat) := FALSE;
    init(wolf) := FALSE;
    init(cabage) := FALSE;
    init(carry) := 0;

    next(ferryman) := !ferryman ;
    next(carry) := {g, c, w, 0};
    next(goat) := case
                    carry = ?? & goat=ferryman: ??;
                    TRUE: goat;
                  esac;
    next(??) := case
                    carry = ?? & ??: ??;
                    TRUE: cabage;
                    esac;
    next(??) := case
                    carry = ?? & wolf=ferryman: ??;
                    TRUE: wolf;
                  esac;