SPIN:3x3の魔法陣の数値選択部分にselectを使用してみる

3x3の魔法陣の解をSPINで求める記事をアップロードした後に、マニュアル(http://spinroot.com/spin/Man)を見ていると、たまたまselectというものがあるのを知りました。

selectを使用すると数値を非決定的に選択する部分を簡単に記述できそうでしたので、magicSquare.pmlをselectを使用して書き直してみます。

作成したソースは以下のとおりです。

ソース 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) ->
      /* 数値を非決定的に選ぶ */
      select(a : 1..9);

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

検証器を作成しての確認

検証時の生成からエラートレイルの列挙

$ spin -run -e magicSquare.pml 
:
省略
:
$ 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

同じ結果になっていそうです。
マニュアルにあたると色々と発見があります。