SPIN:3x3の魔法陣の解を求める
「SPINモデル検査入門」という本の11章ケーススタディに8クイーン問題の解を求めるサンプルがあったので、自身の練習として3x3の魔法陣の解を求めてみたいと思います。
作成したソースは以下のとおりです。
ソース magicSquare.pml
#define SIZE 3 /* ------------------------- 魔法陣ms 1列目 2列目 3列目 1行目 ms[0] ms[1] ms[2] 2行目 ms[3] ms[4] ms[5] 3行目 ms[6] ms[7] ms[8] -------------------------- */ byte ms[SIZE*SIZE]; /* ------------------------- 使用済みの数値判定用 例 used[0] == true <- 数値1使用済み used[1] == false <- 数値2未使用 : used[8] == true <- 数値9使用済み -------------------------- */ bool used[SIZE*SIZE]; active proctype p() { /* 魔法陣に1から9の数値を非決定的に設定していく */ byte a; byte i = 0 do :: i < (SIZE*SIZE) -> /* 数値を非決定的に選ぶ */ if :: a = 1 :: a = 2 :: a = 3 :: a = 4 :: a = 5 :: a = 6 :: a = 7 :: a = 8 :: a = 9 fi if /* 選んだ数値が未使用の場合 */ :: used[a-1] != true -> ms[i] = a; used[a-1] = true i++ /* 選んだ数値が使用済みの場合 */ :: else -> skip fi /* 魔法陣に数値を入れきったらループを抜ける */ :: i == SIZE*SIZE -> break od /* 魔法陣 */ printf("\nMS : %d %d %d\nMS : %d %d %d\nMS : %d %d %d\n", ms[0],ms[1],ms[2],ms[3],ms[4],ms[5],ms[6],ms[7],ms[8]); /* 魔法陣の和を確認する */ bool check = true; if :: /* 各行のチェック */ (ms[0] + ms[1] + ms[2] == 15) && (ms[3] + ms[4] + ms[5] == 15) && (ms[6] + ms[7] + ms[8] == 15) && /* 各列のチェック */ (ms[0] + ms[3] + ms[6] == 15) && (ms[1] + ms[4] + ms[7] == 15) && (ms[2] + ms[5] + ms[8] == 15) && /* 対角線のチェック */ (ms[0] + ms[4] + ms[8] == 15) && (ms[6] + ms[4] + ms[2] == 15) -> check = true :: else -> check = false fi /* 検証により検出させるため check == false を検査式にする */ assert(check == false); }
手動シミュレーションでの簡易動作確認
手動シミュレーションで検証エラーになる場合とならない場合を簡易的に確認します。
魔法陣が成立しない(検証エラーにならない)場合
手動で何度も入力するのが面倒なので入力データを作成しました。
入力データ in01
$ cat in01 1 2 3 4 5 6 7 8 9
シミュレーション
作成したデータをリダイレクトで入力します。
$ spin -i magicSquare.pml < in01
Select stmnt (proc 0 (p:1) )
choice 1: ((i<(3*3)))
:
(略)
:
Select stmnt (proc 0 (p:1) )
choice 2: ((i==(3*3)))
MS : 1 2 3
MS : 4 5 6
MS : 7 8 9
Select stmnt (proc 0 (p:1) )
choice 2: (else)
1 process created魔法陣が成立していないので、検証エラーも出ていません。
魔法陣が成立する(検証エラーになる)場合
入力データ in02
$ cat in02 2 7 6 9 5 1 4 3 8
シミュレーション
$ spin -i magicSquare.pml < in02 Select stmnt (proc 0 (p:1) ) choice 1: ((i<(3*3))) : (略) : spin: magicSquare.pml:78, Error: assertion violated spin: text of failed assertion: assert((check==0)) #processes: 1 ms[0] = 2 ms[1] = 7 ms[2] = 6 ms[3] = 9 ms[4] = 5 ms[5] = 1 ms[6] = 4 ms[7] = 3 ms[8] = 8 used[0] = 1 used[1] = 1 used[2] = 1 used[3] = 1 used[4] = 1 used[5] = 1 used[6] = 1 used[7] = 1 used[8] = 1 89: proc 0 (p:1) magicSquare.pml:78 (state 34) 1 process created
魔法陣が成立しているので、検証エラーとなっています。
検証器を作成しての確認
検証時の生成から実行
$ spin -run -e magicSquare.pml
Depth= 172 States= 1e+06 Transitions= 2.47e+06 Memory= 181.952 t= 0.51 R= 2e+06
Depth= 172 States= 2e+06 Transitions= 4.93e+06 Memory= 235.272 t= 1.04 R= 2e+06
Depth= 172 States= 3e+06 Transitions= 7.4e+06 Memory= 288.593 t= 1.59 R= 2e+06
Depth= 172 States= 4e+06 Transitions= 9.87e+06 Memory= 341.913 t= 2.15 R= 2e+06
pan:1: assertion violated (check==0) (at depth 110)
pan: wrote magicSquare.pml1.trail
Depth= 172 States= 5e+06 Transitions= 1.23e+07 Memory= 395.233 t= 2.78 R= 2e+06
pan: wrote magicSquare.pml2.trail
Depth= 172 States= 6e+06 Transitions= 1.48e+07 Memory= 448.554 t= 3.47 R= 2e+06
Depth= 172 States= 7e+06 Transitions= 1.73e+07 Memory= 501.776 t= 4.18 R= 2e+06
Depth= 172 States= 8e+06 Transitions= 1.97e+07 Memory= 555.097 t= 4.83 R= 2e+06
Depth= 172 States= 9e+06 Transitions= 2.22e+07 Memory= 608.417 t= 5.47 R= 2e+06
pan: wrote magicSquare.pml3.trail
Depth= 172 States= 1e+07 Transitions= 2.47e+07 Memory= 661.737 t= 6.15 R= 2e+06
pan: wrote magicSquare.pml4.trail
Depth= 172 States= 1.1e+07 Transitions= 2.71e+07 Memory= 715.058 t= 6.84 R= 2e+06
Depth= 172 States= 1.2e+07 Transitions= 2.96e+07 Memory= 768.378 t= 7.56 R= 2e+06
Depth= 172 States= 1.3e+07 Transitions= 3.21e+07 Memory= 821.698 t= 8.39 R= 2e+06
Depth= 172 States= 1.4e+07 Transitions= 3.45e+07 Memory= 874.921 t= 9.22 R= 2e+06
pan: wrote magicSquare.pml5.trail
Depth= 172 States= 1.5e+07 Transitions= 3.7e+07 Memory= 928.241 t= 10.1 R= 1e+06
pan: wrote magicSquare.pml6.trail
Depth= 172 States= 1.6e+07 Transitions= 3.95e+07 Memory= 981.562 t= 10.9 R= 1e+06
Depth= 172 States= 1.7e+07 Transitions= 4.19e+07 Memory= 1034.882 t= 11.9 R= 1e+06
Depth= 172 States= 1.8e+07 Transitions= 4.44e+07 Memory= 1088.202 t= 13 R= 1e+06
Depth= 172 States= 1.9e+07 Transitions= 4.69e+07 Memory= 1141.522 t= 13.9 R= 1e+06
pan: wrote magicSquare.pml7.trail
Depth= 172 States= 2e+07 Transitions= 4.93e+07 Memory= 1194.843 t= 14.8 R= 1e+06
pan: wrote magicSquare.pml8.trail
Depth= 172 States= 2.1e+07 Transitions= 5.18e+07 Memory= 1248.065 t= 15.7 R= 1e+06
Depth= 172 States= 2.2e+07 Transitions= 5.43e+07 Memory= 1301.386 t= 16.7 R= 1e+06
Depth= 172 States= 2.3e+07 Transitions= 5.67e+07 Memory= 1354.706 t= 17.9 R= 1e+06
Depth= 172 States= 2.4e+07 Transitions= 5.92e+07 Memory= 1408.026 t= 18.9 R= 1e+06
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 32 byte, depth reached 172, errors: 8
24987242 states, stored
36640017 states, matched
61627259 transitions (= stored+matched)
0 atomic steps
hash conflicts: 19533061 (resolved)
Stats on memory usage (in Megabytes):
1429.781 equivalent memory usage for states (stored*(State-vector + overhead))
1332.493 actual memory usage for states (compression: 93.20%)
state-vector as stored = 28 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1460.663 total actual memory usage
unreached in proctype p
(0 of 35 states)
pan: elapsed time 19.8 seconds
pan: rate 1263257.9 states/second8パターンのエラーが検出されています。
エラートレイルの列挙
8パターンあるので魔法陣出力部分を抜き出して出力させます。
$ for i in $(seq 1 8); do echo magicSquare.pml$i.trail; spin -t$i -B magicSquare.pml | grep MS; done magicSquare.pml1.trail MS : 2 7 6 MS : 9 5 1 MS : 4 3 8 magicSquare.pml2.trail MS : 2 9 4 MS : 7 5 3 MS : 6 1 8 magicSquare.pml3.trail MS : 4 3 8 MS : 9 5 1 MS : 2 7 6 magicSquare.pml4.trail MS : 4 9 2 MS : 3 5 7 MS : 8 1 6 magicSquare.pml5.trail MS : 6 1 8 MS : 7 5 3 MS : 2 9 4 magicSquare.pml6.trail MS : 6 7 2 MS : 1 5 9 MS : 8 3 4 magicSquare.pml7.trail MS : 8 1 6 MS : 3 5 7 MS : 4 9 2 magicSquare.pml8.trail MS : 8 3 4 MS : 1 5 9 MS : 6 7 2
確かに魔法陣になっていそうです。
