random - ランダム トレースを使用した NuSMV シミュレーション

Question

作成した NuSMV モデルの「ランダム」または非決定論的シミュレーションを実行しようとしています。ただし、後続の実行間で生成されるトレースはまったく同じです。

モデルは次のとおりです。

MODULE main
VAR x : 0..4;
VAR clk : 0..10;

DEFINE next_x :=
    case
        x = 0 : {0,1};
        x = 1 : {1,2};
        x = 2 : {1,0};
        TRUE : {0};
    esac;

DEFINE next_clk :=
    case
        (clk < 10) : (clk+1);
        TRUE : clk;
    esac;

INIT (x = 0);
INIT (clk = 0);

TRANS (next(x) in next_x);
TRANS next(clk) = next_clk;

CTLSPEC AG(clk < 10);

対話型シェルで次のコマンドを使用してこれを実行しています。

go
pick_state -r
simulate -k -r 30
show_traces 1
quit

おそらく私のモデルに間違いがありますか？または、シェルで正しいコマンドを実行していません。

前もって感謝します！