注意：本问题中提供的模型无法重现给定的错误信息，因为该模型中有许多语法错误。
一维矩阵。
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;
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
不支持4x4的游览。
对于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游历。
对于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的解决方案。
#define A[] = True; A[I,J] = false;这段代码是什么意思？它不是有效的Promela代码。 - Patrick Trentin