在 NuSMV 中编写冒泡排序
Programming a bubblesort in NuSMV
我正在尝试在 NuSMV 中编写一个简单的冒泡排序作为 FSM，但我面临一个主要问题，当我尝试在 2 之间进行交换时，我无法在数组中进行交换elements os 数组，程序停止。谁能帮忙解决这个问题？非常感谢。
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
这里你的模型有误：
TRANS
case
arr[x] <= arr[y] : output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1;
...
esac;
第一行表示如果arr[x] <= arr[y]为真，那么到下一个状态的转移关系定义为output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1。但是，后一个表达式在除第一个状态（值幸运匹配）之外的所有状态下的计算结果为 false，因此不可能向外转换到另一个状态。
此外，请注意您正在尝试更改 数组定义的值，这是无法完成的。要看到这一点，请比较此模型交换变量数组
的值
MODULE main()
VAR
arr: array 0..1 of {1,2};
ASSIGN
init(arr[0]) := 1;
init(arr[1]) := 2;
TRANS
next(arr[0]) = arr[1] &
next(arr[1]) = arr[0];
具有以下输出
nuXmv > reset; read_model -i swap.smv; go; pick_state -v ; simulate -v
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
******** Simulation Starting From State 1.1 ********
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
-> State: 1.2 <-
arr[0] = 2
arr[1] = 1
...
与此 其他 模型交换已定义数组的值
MODULE main()
DEFINE
arr := [1, 2];
TRANS
next(arr[0]) = arr[1] &
next(arr[1]) = arr[0];
这导致
nuXmv > reset; read_model -i swap_def.smv; go; pick_state -v ; simulate -v
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
******** Simulation Starting From State 1.1 ********
No future state exists: trace not built.
Simulation stopped at step 1.
您当前的 bubblesort 模型需要一些修复才能更正，因此我决定使用 wikipedia as reference. The model I wrote can be run within nuXmv[=59 从头开始编写一个新模型=]，这是一个扩展 NuSMV 的工具，具有一些有趣的 新 功能。
EDIT: I (slightly) modified the model in my original answer so as to be fully compatible with NuSMV
-- Bubblesort Algorithm model
--
-- author: Patrick Trentin
--
MODULE main
VAR
arr : array 0..4 of 1..5;
i : 0..4;
swapped : boolean;
DEFINE
do_swap := (i < 4) & arr[ (i + 0) mod 5 ] > arr[ (i + 1) mod 5 ];
do_ignore := (i < 4) & arr[ (i + 0) mod 5 ] <= arr[ (i + 1) mod 5 ];
do_rewind := (i = 4) & swapped = TRUE;
end_state := (i = 4) & swapped = FALSE;
ASSIGN
init(arr[0]) := 4; init(arr[1]) := 1; init(arr[2]) := 3;
init(arr[3]) := 2; init(arr[4]) := 5;
init(i) := 0;
next(i) := case
end_state : i; -- end state
TRUE : (i + 1) mod 5;
esac;
init(swapped) := FALSE;
next(swapped) := case
(i < 4) & arr[(i+0) mod 5] > arr[(i+1) mod 5] : TRUE;
do_rewind : FALSE;
TRUE : swapped;
esac;
-- swap two consequent elements if they are not
-- correctly sorted relative to one another
TRANS
do_swap -> (
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- perform no action if two consequent elements are already
-- sorted
TRANS
(do_ignore|do_rewind) -> (
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- perform no action if algorithm has finished
TRANS
(end_state) -> (
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- There exists no path in which the algorithm ends
LTLSPEC ! F end_state
-- There exists no path in which the algorithm ends
-- with a sorted array
LTLSPEC ! F G (arr[0] <= arr[1] &
arr[1] <= arr[2] &
arr[2] <= arr[3] &
arr[3] <= arr[4] &
end_state)
您可以在 nuXmv 上使用以下命令验证模型，它依赖于底层 MathSAT5 SMT Solver执行验证步骤：
~$ nuXmv -int
nuXmv> read_model -i bubblesort.smv
nuXmv> go_msat;
nuXmv> msat_check_ltlspec_bmc -k 15
或者您可以简单地使用 NuSMV
~$ NuSMV -int
NuSMV> read_model -i bubblesort.smv
NuSMV> go;
NuSMV> check_property
求解器找到的解如下：
-- specification !( F ( G ((((arr[0] <= arr[1] & arr[1] <= arr[2]) & arr[2] <= arr[3]) & arr[3] <= arr[4]) & end_state))) is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-> State: 2.1 <-
arr[0] = 4
arr[1] = 1
arr[2] = 3
arr[3] = 2
arr[4] = 5
i = 0
swapped = FALSE
end_state = FALSE
do_rewind = FALSE
do_ignore = FALSE
do_swap = TRUE
-> State: 2.2 <-
arr[0] = 1
arr[1] = 4
i = 1
swapped = TRUE
-> State: 2.3 <-
arr[1] = 3
arr[2] = 4
i = 2
-> State: 2.4 <-
arr[2] = 2
arr[3] = 4
i = 3
do_ignore = TRUE
do_swap = FALSE
-> State: 2.5 <-
i = 4
do_rewind = TRUE
do_ignore = FALSE
-> State: 2.6 <-
i = 0
swapped = FALSE
do_rewind = FALSE
do_ignore = TRUE
-> State: 2.7 <-
i = 1
do_ignore = FALSE
do_swap = TRUE
-> State: 2.8 <-
arr[1] = 2
arr[2] = 3
i = 2
swapped = TRUE
do_ignore = TRUE
do_swap = FALSE
-> State: 2.9 <-
i = 3
-> State: 2.10 <-
i = 4
do_rewind = TRUE
do_ignore = FALSE
-> State: 2.11 <-
i = 0
swapped = FALSE
do_rewind = FALSE
do_ignore = TRUE
-> State: 2.12 <-
i = 1
-> State: 2.13 <-
i = 2
-> State: 2.14 <-
i = 3
-- Loop starts here
-> State: 2.15 <-
i = 4
end_state = TRUE
do_ignore = FALSE
-> State: 2.16 <-
我希望你会发现我的回答有帮助，虽然晚了;)。
我正在尝试在 NuSMV 中编写一个简单的冒泡排序作为 FSM，但我面临一个主要问题，当我尝试在 2 之间进行交换时，我无法在数组中进行交换elements os 数组，程序停止。谁能帮忙解决这个问题？非常感谢。
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
这里你的模型有误：
TRANS
case
arr[x] <= arr[y] : output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1;
...
esac;
第一行表示如果arr[x] <= arr[y]为真，那么到下一个状态的转移关系定义为output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1。但是，后一个表达式在除第一个状态（值幸运匹配）之外的所有状态下的计算结果为 false，因此不可能向外转换到另一个状态。
此外，请注意您正在尝试更改 数组定义的值，这是无法完成的。要看到这一点，请比较此模型交换变量数组
的值MODULE main()
VAR
arr: array 0..1 of {1,2};
ASSIGN
init(arr[0]) := 1;
init(arr[1]) := 2;
TRANS
next(arr[0]) = arr[1] &
next(arr[1]) = arr[0];
具有以下输出
nuXmv > reset; read_model -i swap.smv; go; pick_state -v ; simulate -v
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
******** Simulation Starting From State 1.1 ********
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
-> State: 1.2 <-
arr[0] = 2
arr[1] = 1
...
与此 其他 模型交换已定义数组的值
MODULE main()
DEFINE
arr := [1, 2];
TRANS
next(arr[0]) = arr[1] &
next(arr[1]) = arr[0];
这导致
nuXmv > reset; read_model -i swap_def.smv; go; pick_state -v ; simulate -v
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
arr[0] = 1
arr[1] = 2
******** Simulation Starting From State 1.1 ********
No future state exists: trace not built.
Simulation stopped at step 1.
您当前的 bubblesort 模型需要一些修复才能更正，因此我决定使用 wikipedia as reference. The model I wrote can be run within nuXmv[=59 从头开始编写一个新模型=]，这是一个扩展 NuSMV 的工具，具有一些有趣的 新 功能。
EDIT: I (slightly) modified the model in my original answer so as to be fully compatible with NuSMV
-- Bubblesort Algorithm model
--
-- author: Patrick Trentin
--
MODULE main
VAR
arr : array 0..4 of 1..5;
i : 0..4;
swapped : boolean;
DEFINE
do_swap := (i < 4) & arr[ (i + 0) mod 5 ] > arr[ (i + 1) mod 5 ];
do_ignore := (i < 4) & arr[ (i + 0) mod 5 ] <= arr[ (i + 1) mod 5 ];
do_rewind := (i = 4) & swapped = TRUE;
end_state := (i = 4) & swapped = FALSE;
ASSIGN
init(arr[0]) := 4; init(arr[1]) := 1; init(arr[2]) := 3;
init(arr[3]) := 2; init(arr[4]) := 5;
init(i) := 0;
next(i) := case
end_state : i; -- end state
TRUE : (i + 1) mod 5;
esac;
init(swapped) := FALSE;
next(swapped) := case
(i < 4) & arr[(i+0) mod 5] > arr[(i+1) mod 5] : TRUE;
do_rewind : FALSE;
TRUE : swapped;
esac;
-- swap two consequent elements if they are not
-- correctly sorted relative to one another
TRANS
do_swap -> (
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- perform no action if two consequent elements are already
-- sorted
TRANS
(do_ignore|do_rewind) -> (
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- perform no action if algorithm has finished
TRANS
(end_state) -> (
next(arr[ (i + 0) mod 5 ]) = arr[ (i + 0) mod 5 ] &
next(arr[ (i + 1) mod 5 ]) = arr[ (i + 1) mod 5 ] &
next(arr[ (i + 2) mod 5 ]) = arr[ (i + 2) mod 5 ] &
next(arr[ (i + 3) mod 5 ]) = arr[ (i + 3) mod 5 ] &
next(arr[ (i + 4) mod 5 ]) = arr[ (i + 4) mod 5 ]
);
-- There exists no path in which the algorithm ends
LTLSPEC ! F end_state
-- There exists no path in which the algorithm ends
-- with a sorted array
LTLSPEC ! F G (arr[0] <= arr[1] &
arr[1] <= arr[2] &
arr[2] <= arr[3] &
arr[3] <= arr[4] &
end_state)
您可以在 nuXmv 上使用以下命令验证模型，它依赖于底层 MathSAT5 SMT Solver执行验证步骤：
~$ nuXmv -int
nuXmv> read_model -i bubblesort.smv
nuXmv> go_msat;
nuXmv> msat_check_ltlspec_bmc -k 15
或者您可以简单地使用 NuSMV
~$ NuSMV -int
NuSMV> read_model -i bubblesort.smv
NuSMV> go;
NuSMV> check_property
求解器找到的解如下：
-- specification !( F ( G ((((arr[0] <= arr[1] & arr[1] <= arr[2]) & arr[2] <= arr[3]) & arr[3] <= arr[4]) & end_state))) is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-> State: 2.1 <-
arr[0] = 4
arr[1] = 1
arr[2] = 3
arr[3] = 2
arr[4] = 5
i = 0
swapped = FALSE
end_state = FALSE
do_rewind = FALSE
do_ignore = FALSE
do_swap = TRUE
-> State: 2.2 <-
arr[0] = 1
arr[1] = 4
i = 1
swapped = TRUE
-> State: 2.3 <-
arr[1] = 3
arr[2] = 4
i = 2
-> State: 2.4 <-
arr[2] = 2
arr[3] = 4
i = 3
do_ignore = TRUE
do_swap = FALSE
-> State: 2.5 <-
i = 4
do_rewind = TRUE
do_ignore = FALSE
-> State: 2.6 <-
i = 0
swapped = FALSE
do_rewind = FALSE
do_ignore = TRUE
-> State: 2.7 <-
i = 1
do_ignore = FALSE
do_swap = TRUE
-> State: 2.8 <-
arr[1] = 2
arr[2] = 3
i = 2
swapped = TRUE
do_ignore = TRUE
do_swap = FALSE
-> State: 2.9 <-
i = 3
-> State: 2.10 <-
i = 4
do_rewind = TRUE
do_ignore = FALSE
-> State: 2.11 <-
i = 0
swapped = FALSE
do_rewind = FALSE
do_ignore = TRUE
-> State: 2.12 <-
i = 1
-> State: 2.13 <-
i = 2
-> State: 2.14 <-
i = 3
-- Loop starts here
-> State: 2.15 <-
i = 4
end_state = TRUE
do_ignore = FALSE
-> State: 2.16 <-
我希望你会发现我的回答有帮助，虽然晚了;)。