I'm trying to program a simple bubble sort as a FSM in NuSMV, but i'm facing a major problem, I can't do the swap in the array, when I try to make a swap between 2 elements os the array, the program stops. Can anyone help solve this? Thanks a lot.
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
Your model is wrong here:
TRANS
case
arr[x] <= arr[y] : output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1;
...
esac;
The first line means that if arr[x] <= arr[y] is true, then the transition relation to the next state is defined by output[x] = low & output[y] = big & next(y) = y + 1 & next(x) = x + 1. However, the latter expression evaluates to false in all but the first state (for which there is a lucky match of values), and thus there is no possible outgoing transition to another state.
Moreover, notice that you are trying to change the values of an array definition, which it can't be done. To see this, compare this model swapping the values of a variable array
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];
which has the following output
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
...
with this other model swapping the values of a defined array
MODULE main()
DEFINE
arr := [1, 2];
TRANS
next(arr[0]) = arr[1] &
next(arr[1]) = arr[0];
which results in
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.
Your current model for bubblesort requires a number of fixes in order to be corrected, thus I decided to write a new one from scratch using wikipedia as reference. The model I wrote can be run within nuXmv, which is a tool that extends NuSMV with some interesting new features.
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)
You can verify the model with the following commands on nuXmv, which rely on the underlying MathSAT5 SMT Solver for doing the verification step:
~$ nuXmv -int
nuXmv> read_model -i bubblesort.smv
nuXmv> go_msat;
nuXmv> msat_check_ltlspec_bmc -k 15
Or you can simply use NuSMV
~$ NuSMV -int
NuSMV> read_model -i bubblesort.smv
NuSMV> go;
NuSMV> check_property
The solution found by the solver is the following one:
-- 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 <-
I hope you'll find my answer helpful, albeit late ;).