CODEWITHSUNDEEP
fsmmodel-checkingnusmv
Paulo Sousa
Paulo Sousa

Reputation: 75

Programming a bubblesort in NuSMV

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

Upvotes: 1

Views: 1752

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

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 ;).

Upvotes: 2

Related Questions