arraysalgorithmmodel-checkingpromelaspin

All possible Knight moving on a chessboard in promela


Is it possible to bypass a chessboard of size N × N with a knight from the initial position (I, J), having visited each square only once?

#define A[] = True; A[I,J] = false;
active proctype method(){
bit I=4;
bit J=3;
bit K=1;
bit N=8;

do
::I>2 && J<N && A[I-2,J+1] => I=I-2;J=J+1; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I>2 && J>1 && A[I-2,J-1] => I=I-2;J=J-1; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I<N && J>1 && A[I+1,J-2] => I=I+1;J=J-2; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I>2 && J>1 && A[I-1,J-2] => I=I-1;J=J-2; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I<N && J<N && A[I+1,J+2] => I=I+1;J=J+2; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I>2 && J<N && A[I-1,J+2] => I=I-1;J=J+2; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I<N && J<N && A[I+2,J+1] => I=I+2;J=j+1; A[I,J]=False; K++;
printf("i %d j %d \n"i, j);
::I<N && J>1 && A[I+2,J-1] => I=I+2;J=J-1; A[I,J]=False; K++;
::K==N*N break
od
}

But i get error in matrix A[I,J]

spin: line   9 "pan_in", Error: syntax error    saw '',' = '44''
spin: line  27 "pan_in", Error: no runable process

Algotithm ---picture algorithm


Solution

  • Note: the model provided in the question does not allow one to reproduce the given error message, because there are many more syntax error contained in it.


    ONE-DIMENSIONAL MATRICES.

    In Promela, multi-dimensional arrays are not directly supported. Therefore, the expression A[i, j] is not supported.

    One workaround is to define an array of a struct containing another array. IMHO, a better workaround is to use one dimensional arrays and clever indexing.

    For this purposes, it is convenient to declare the chessboard array at a global scope level, so that we can then use macros to access a given chessboard location:

    #define CHESSBOARD_SIZE 8
    
    bool chessboard[CHESSBOARD_SIZE * CHESSBOARD_SIZE];
    
    #define CHESSBOARD(r, c) chessboard[(r) * CHESSBOARD_SIZE + (c)]
    

    RUNNING EXAMPLE.

    A complete example follows:

    #define CHESSBOARD_SIZE 4
    
    int i, j;
    int chessboard[CHESSBOARD_SIZE * CHESSBOARD_SIZE];
    
    #define CHESSBOARD(r, c) chessboard[(r) * CHESSBOARD_SIZE + (c)]
    #define IS_VALID(r, c)   ((r) >= 0 && (c) >= 0 && (r) < CHESSBOARD_SIZE && (c) < CHESSBOARD_SIZE)
    #define IS_FREE(r, c)    (IS_VALID((r), (c)) && CHESSBOARD((r), (c)) == 0)
    
    inline do_move_knight_to(src_r, src_c, dst_r, dst_c, id_move)
    {
        assert(IS_VALID(src_r, src_c));
        assert(IS_VALID(dst_r, dst_c));
        src_r = dst_r;
        src_c = dst_c;
        CHESSBOARD(src_r, src_c) = id_move;
    }
    
    inline print_chessboard()
    {
        printf("Chessboard:\n");
        for (i : 0 .. (CHESSBOARD_SIZE - 1)) {
            for (j : 0 .. (CHESSBOARD_SIZE - 1)) {
                if
                    :: CHESSBOARD(i, j) == 0 ->
                        printf("--");
                    :: 0 < CHESSBOARD(i, j) && CHESSBOARD(i, j) < 10 ->
                        printf("0%d", CHESSBOARD(i, j));
                    :: else ->
                        printf("%d", CHESSBOARD(i, j));
                fi
            }
            printf("\n");
        }
        printf("\n");
    }
    
    proctype knight_moves(int r; int c)
    {
        int counter = 1;
    
        /* initial step */
        do_move_knight_to(r, c, r, c, counter);
        counter++;
        printf("Knight starts in [%d, %d].\n", r, c);
    
        do
            :: counter <= CHESSBOARD_SIZE * CHESSBOARD_SIZE ->
                if
                    :: IS_FREE(r - 2, c + 1) ->
                       do_move_knight_to(r, c, r - 2, c + 1, counter)
                    :: IS_FREE(r - 2, c - 1) ->
                       do_move_knight_to(r, c, r - 2, c - 1, counter)
                    :: IS_FREE(r + 1, c - 2) ->
                       do_move_knight_to(r, c, r + 1, c - 2, counter)
                    :: IS_FREE(r - 1, c - 2) ->
                       do_move_knight_to(r, c, r - 1, c - 2, counter)
                    :: IS_FREE(r + 1, c + 2) ->
                       do_move_knight_to(r, c, r + 1, c + 2, counter)
                    :: IS_FREE(r - 1, c + 2) ->
                       do_move_knight_to(r, c, r - 1, c + 2, counter)
                    :: IS_FREE(r + 2, c + 1) ->
                       do_move_knight_to(r, c, r + 2, c + 1, counter)
                    :: IS_FREE(r + 2, c - 1) ->
                       do_move_knight_to(r, c, r + 2, c - 1, counter)
                    :: else ->
                       printf("No available move.\n\n");
                       print_chessboard();
    knight_is_stuck:
                       break;
                fi;
                counter++;
                printf("Knight moves to [%d, %d].\n", r, c);
            :: else ->
                printf("Knight covered entire chessboard.\n\n");
                print_chessboard();
    knight_covered_entire_chessboard:
                break;
        od;
    }
    
    init
    {
        int r, c;
    
        select(r: 0 .. CHESSBOARD_SIZE - 1);
        select(c: 0 .. CHESSBOARD_SIZE - 1);
    
        run knight_moves(r, c);
    }
    
    ltl no_full_cover { [] !knight_moves[1]@knight_covered_entire_chessboard };
    

    SIMULATION.

    The output of a simulation run:

    ~$ spin test.pml
    ...
              Knight starts in [3, 0].
              Knight moves to [2, 2].
              Knight moves to [0, 3].
              Knight moves to [1, 1].
              Knight moves to [2, 3].
              Knight moves to [3, 1].
              Knight moves to [1, 2].
              Knight moves to [3, 3].
              Knight moves to [2, 1].
              Knight moves to [0, 2].
              Knight moves to [1, 0].
              No available move.
    
              Chessboard:
              --          --          10          03          
              11          04          07          --          
              --          09          02          05          
              01          06          --          08          
    
    2 processes created
    

    NO 4x4 TOUR.

    For CHESSBOARD_SIZE = 4, it can be verified that the knight cannot cover the full chessboard:

    ~$ spin -search -bfs -ltl no_full_cover test.pml 
    ...
    Depth=      10 States=      107 Transitions=      107 Memory=   128.195 
    Depth=      20 States=      795 Transitions=      795 Memory=   128.293 
    Depth=      30 States= 3.66e+03 Transitions= 3.66e+03 Memory=   128.879 
    Depth=      40 States= 1.38e+04 Transitions= 1.38e+04 Memory=   130.832 
    Depth=      50 States= 4.22e+04 Transitions= 4.22e+04 Memory=   136.203 t=     0.02 R=   2e+06
    Depth=      60 States= 1.03e+05 Transitions= 1.03e+05 Memory=   147.336 t=     0.05 R=   2e+06
    Depth=      70 States= 1.98e+05 Transitions= 1.98e+05 Memory=   163.938 t=     0.11 R=   2e+06
    Depth=      80 States= 3.03e+05 Transitions= 3.03e+05 Memory=   181.809 t=     0.17 R=   2e+06
    Depth=      90 States=  4.1e+05 Transitions=  4.1e+05 Memory=   199.680 t=     0.24 R=   2e+06
    Depth=     100 States= 5.16e+05 Transitions= 5.16e+05 Memory=   217.453 t=      0.3 R=   2e+06
    Depth=     110 States= 6.22e+05 Transitions= 6.22e+05 Memory=   235.324 t=     0.37 R=   2e+06
    Depth=     120 States= 7.27e+05 Transitions= 7.27e+05 Memory=   252.902 t=     0.43 R=   2e+06
    Depth=     130 States= 8.28e+05 Transitions= 8.28e+05 Memory=   269.895 t=     0.49 R=   2e+06
    Depth=     140 States= 9.18e+05 Transitions= 9.18e+05 Memory=   284.738 t=     0.55 R=   2e+06
    Depth=     150 States= 9.78e+05 Transitions= 9.78e+05 Memory=   294.602 t=     0.58 R=   2e+06
    Depth=     160 States= 9.98e+05 Transitions= 9.98e+05 Memory=   297.824 t=      0.6 R=   2e+06
    
    (Spin Version 6.5.0 -- 17 July 2019)
        + Breadth-First Search
        + Partial Order Reduction
    
    Full statespace search for:
        never claim             + (no_full_cover)
        assertion violations    + (if within scope of claim)
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      - (disabled by never claim)
    
    State-vector 120 byte, depth reached 167, errors: 0
       999549 states, stored
          999549 nominal states (stored-atomic)
            0 states, matched
       999549 transitions (= stored+matched)
            0 atomic steps
    hash conflicts:       396 (resolved)
    
    Stats on memory usage (in Megabytes):
      141.080   equivalent memory usage for states (stored*(State-vector + overhead))
      170.191   actual memory usage for states
      128.000   memory used for hash table (-w24)
      298.020   total actual memory usage
    
    
    unreached in proctype knight_moves
        test.pml:75, state 74, "printf('Knight covered entire chessboard.\n')"
        (1 of 110 states)
    unreached in init
        (0 of 16 states)
    unreached in claim no_full_cover
        _spin_nvr.tmp:8, state 10, "-end-"
        (1 of 10 states)
    
    pan: elapsed time 0.6 seconds
    pan: rate   1665915 states/second
    

    A 5x5 TOUR.

    For CHESSBOARD_SIZE = 5, spin finds an execution trace that violates the LTL property whereby the knight's tour covers every tile of the chessboard:

    ~$ spin -search test.pml
    ...
    pan:1: assertion violated  !( !( !((knight_moves[1]._p==knight_covered_entire_chessboard)))) (at depth 514)
    pan: wrote test.pml.trail
    
    (Spin Version 6.5.0 -- 17 July 2019)
    Warning: Search not completed
        + Partial Order Reduction
    
    Full statespace search for:
        never claim             + (no_full_cover)
        assertion violations    + (if within scope of claim)
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      - (disabled by never claim)
    
    State-vector 160 byte, depth reached 514, errors: 1
      1241104 states, stored
         8508 states, matched
      1249612 transitions (= stored+matched)
            0 atomic steps
    hash conflicts:       997 (resolved)
    
    Stats on memory usage (in Megabytes):
      222.518   equivalent memory usage for states (stored*(State-vector + overhead))
      199.077   actual memory usage for states (compression: 89.47%)
                state-vector as stored = 140 byte + 28 byte overhead
      128.000   memory used for hash table (-w24)
        0.534   memory used for DFS stack (-m10000)
      327.362   total actual memory usage
    
    
    
    pan: elapsed time 0.6 seconds
    pan: rate 2068506.7 states/second
    

    The knight's tour can be replayed as follows:

    ~$ spin -t test.pml
    ...
                  Knight starts in [0, 0].
                  Knight moves to [1, 2].
                  Knight moves to [2, 0].
                  Knight moves to [0, 1].
                  Knight moves to [1, 3].
                  Knight moves to [3, 4].
                  Knight moves to [4, 2].
                  Knight moves to [3, 0].
                  Knight moves to [1, 1].
                  Knight moves to [0, 3].
                  Knight moves to [2, 4].
                  Knight moves to [4, 3].
                  Knight moves to [3, 1].
                  Knight moves to [1, 0].
                  Knight moves to [2, 2].
                  Knight moves to [4, 1].
                  Knight moves to [3, 3].
                  Knight moves to [1, 4].
                  Knight moves to [0, 2].
                  Knight moves to [2, 1].
                  Knight moves to [4, 0].
                  Knight moves to [3, 2].
                  Knight moves to [4, 4].
                  Knight moves to [2, 3].
                  Knight moves to [0, 4].
                  Knight covered entire chessboard.
    
    Chessboard:
                  01              04              19              10              25              
                  14              09              02              05              18              
                  03              20              15              24              11              
                  08              13              22              17              06              
                  21              16              07              12              23              
    
    spin: _spin_nvr.tmp:3, Error: assertion violated
    spin: text of failed assertion: assert(!(!(!((knight_moves[1]._p==knight_covered_entire_chessboard)))))
    Never claim moves to line 3 [assert(!(!(!((knight_moves[1]._p==knight_covered_entire_chessboard)))))]
    spin: trail ends after 515 steps
    ...
    

    I was able to quickly find solutions up to CHESSBOARD_SIZE equal 7, before I ran out of memory.