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;