用NuSMV语言编写一个bubblesort

Question

我试图在NuSMV中将一个简单的气泡类型作为FSM进行编程，但是我面临一个主要的问题，我不能在数组中进行交换，当我试图在数组上的两个元素之间进行交换时，程序就停止了。有人能帮我解决这个问题吗？非常感谢。

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]是真，那么到下一个状态的转换关系由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模型需要一些修复才能得到纠正，因此我决定使用维基百科作为参考从头编写一个新的模型。我编写的模型可以在nuXmv中运行，它是一个扩展NuSMV和一些有趣的新特性的工具。

编辑：i(稍微)修改了我原来答案中的模型，以便与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解决程序执行验证步骤：

 ~$ 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 <-

我希望你会发现我的回答很有帮助，尽管很晚了;)