logic - NuSMV で再帰的に定義されたエラーを理解する

Question

エラーが発生した NuSMV のコードがあります。コードは次のとおりです。

MODULE main
VAR
    x1: {a,b,c,d,e};
    x2: {a,b,c,d,e};
ASSIGN

    next(x1) := case
        x1=a & x2=c: e;

        x1=d & next(x2)=c : a;
        TRUE : x1;
    esac;
    next(x2) := case
            x1=b & x2=b: c;

            x2=d & next(x1)=e : e;
            TRUE : x2;
        esac;

したがって、これを NuSMV でコンパイルすると、エラーが発生します。recursively defined: x1

x1 の遷移ルール​​の x2 に関連付けられた次のステートメントを削除することで、このエラーを簡単に処理できx1=d & next(x2)=c : a;ますx1=d : a;。x1=d & x2=d : a;

エラーの原因となっている NuSMV ソフトウェアの仕組みと、上記の修正によってエラーが解決される理由を理解したいと思います。私が理解していない同期実装何とか何とか何とかしていると思います。誰かが正確で詳細な技術的説明をすることができますか?

また、 variable でエラーが発生しない理由も説明してくださいx2。その遷移規則は、次の演算子を使用して定義されています。