fsm - NuSMV でのバブルソートのプログラミング

Question

NuSMV で単純なバブル ソートを FSM としてプログラムしようとしていますが、大きな問題に直面しています。配列の 2 つの要素間でスワップを実行しようとすると、配列でスワップを実行できません。プログラムが停止します。誰でもこれを解決できますか？どうもありがとう。

MODULE main
VAR

y: 0..5;
x : 0..5;
low : 0..10;
big : 0..10;

DEFINE
arr : [3,4,2,3,5,6];
output : [0,0,0,0,0,0];

ASSIGN

init(x) := 0;
init(y) := 1;
init(low) := 0;
init(big) := 0; 


next(low) := case
    arr[x] > arr[y] : arr[y];
    TRUE : arr[x];
    esac;

next(big) := case
    arr[x] > arr[y] : arr[x];
    TRUE : arr[x];
    esac;

TRANS
case
    arr[x] <= arr[y] : output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1;
    arr[x] > arr[y] : output[x] = big & output[y] = low & next(y) = y + 1 & next(x) = x + 1;
    y = 5 | x = 5 : next(y) = 0 & next(x) = 1;
    TRUE : next(y) = y + 1 & next(x) = x + 1;
esac