Question

Можно ли обойти шахматную доску размером N × N с конем из начальной позиции (I, J), посетив каждый квадрат только один раз?

#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
}

Но я получаю ошибку в матрице A [I, J]

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

Алгоритм ---

Patrick Trentin · Answer 1 · 07 ноября 2019

Примечание: модель, представленная в вопросе, не позволяет воспроизвести данное сообщение об ошибке, поскольку в нем содержится много других синтаксических ошибок .

ОДНОМЕРНЫЕ МАТРИЦЫ.

В Promela многомерные массивы напрямую не поддерживаются . Поэтому выражение A[i, j] не поддерживается.

Один из обходных путей - определить массив структуры, содержащей другой массив. ИМХО, лучшим обходным путем является использование одномерных массивов и умное индексирование.

Для этих целей удобно объявить массив шахматной доски на глобальном уровне области видимости, чтобы мы могли затем использовать макросов для доступа к заданному местоположению шахматной доски:

#define CHESSBOARD_SIZE 8

bool chessboard[CHESSBOARD_SIZE * CHESSBOARD_SIZE];

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

ПРИМЕР РАБОТЫ.

Ниже приведен полный пример:

#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 };

МОДЕЛИРОВАНИЕ.

Вывод прогона моделирования:

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

Для CHESSBOARD_SIZE = 4, можно убедиться, что конь не может покрыть всю шахматную доску:

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

5x5 TOUR.

Для CHESSBOARD_SIZE = 5, spin находит след выполнения, который нарушает свойство LTL , в соответствии с которым тур коня покрывает каждую клетку шахматной доски:

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

Тур коня можно воспроизвести следующим образом:

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

Мне удалось быстро найти решения до CHESSBOARD_SIZE, равного 7, до того, как мне не хватило памяти.

Все возможные рыцари движутся по шахматной доске в промеле

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Все возможные рыцари движутся по шахматной доске в промеле

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Похожие темы