NuSMV プログラムがあり、プログラム (ゲーム) が 5 タイム ステップ未満で勝てないことを CTL または LTL で指定する必要があります。またはより形式的: ゲームに勝つためには、少なくとも 5 つのタイム ステップが必要です。
私は明示的な時間変数を持っていないので、検証用に作成したくありません。すでに行われた移行の量を数える方法はありますか? 訪問した州の数、そのようなものですか？
現時点で私はこれを持っています：
SPEC ( (gameState != WIN) U (how to count time steps?))