NuSMV を使用してモデルをチェックしようとしましたが、コードは次のとおりです。
ただし、NuSMV kernel.smvシェルに入力するとエラーが発生します
file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(tx.fired) at line 16
私は NuSMV モデル チェッカーの初心者なので、この構文エラーを修正できませんでした。助けてください、ありがとう！