在 NuSMV 中编程冒泡排序

Question

我正在尝试在 NuSMV 中将简单的冒泡排序编程为 FSM，但我面临一个主要问题，当我尝试在 2 个元素之间进行交换时，我无法在数组中进行交换 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

Answer 1

你的模型在这里是错误的：

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]为true，那么到下一个状态的转换关系由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
...

用这个other模型交换定义数组的值

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 作为参考从头开始编写一个新模型。我编写的模型可以在 nuXmv 中运行，这是一个扩展了 NuSMV 并具有一些有趣的新功能的工具。

编辑：我（稍微）修改了原始答案中的模型，以便与 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 <-

希望我的回答对您有所帮助，尽管有点晚 ;)。