Программирование bubblesort в NuSMV

Question

Я пытаюсь запрограммировать простой тип пузырьков как FSM в NuSMV, но у меня возникла серьезная проблема, я не могу выполнить своп в массиве, когда я пытаюсь сделать обмен между двумя элементами массива, программа останавливается. Может ли кто-нибудь помочь в решении этого? Большое спасибо.

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 требует ряд исправлений для того, чтобы исправить, таким образом, я решил написать новый с нуля, используя wikipedia в качестве ссылки. Модель, которую я написал, может быть запущена в пределах nuXmv, который является инструментом, который расширяет NuSMV с некоторыми интересными новыми функциями.

EDIT: 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, которые полагаются на базовые MathSAT5SMT 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 <- 

Я надеюсь, что вы найдете мой ответ полезным, хотя и с запозданием;).