「SpinIntro.pdf」の「SPIN's Basic Data Structures」を見ると状態ベクトル(State vecot)は全ての変数を保持している旨の記載があります。また、PanのCompile-Time Optionsには状態ベクトルをダンプするオプション(SDUMP)について記載があります。コンパイ…

SPINのstate vector(状態ベクトル?)が気になってデバッグしているときに、pan.cでビットフィールドが使われている箇所を見つけました。C言語の本で存在は知っていたのですが、使用したこともなく、また実際のコードで見たのは初めてでした。state vectorの理…

spinのヘルプを見ているときに-o2オプションが気になりました。 -o2オプションのヘルプの説明を読むと書き込みだけの変数も隠さずに検証するような記述になっています。このオプションの説明から、もしかすると「SPINモデル検査入門」で紹介されている8クイ…

これまで読んだSPIN本のどこかに書かれているかもしれませんが完全にスルーしていた内容を紹介します。(SPINモデル検査入門の8クイーン問題で知りました。)以下の見出しでわかってしまいますが、以下のモデルを実行した際に Hello, world!は出力されるでしょ…

3x3の魔法陣の解をSPINで求める記事をアップロードした後に、マニュアル(http://spinroot.com/spin/Man)を見ていると、たまたまselectというものがあるのを知りました。selectを使用すると数値を非決定的に選択する部分を簡単に記述できそうでしたので、magi…

「SPINモデル検査入門」という本の11章ケーススタディに8クイーン問題の解を求めるサンプルがあったので、自身の練習として3x3の魔法陣の解を求めてみたいと思います。作成したソースは以下のとおりです。 ソース magicSquare.pml #define SIZE 3 /* -------…

SPINを勉強しているのですが、spin, 検証器(pan)コマンドのオプションが覚えられずに頻繁にヘルプを参照しています。私の環境ではヘルプを出力すると作業ターミナルの画面から溢れるのでページャを通して確認することが多いです。ページャを通すと検索機能を…