プログラミングなどなど

プログラミングに関係しそうな内容を

SPIN

SPIN:Never Claimと通常プロセスの動作の違いに気をつけよう

SPINでは検証式の記述に時相論理という論理が使えるのですが、よく理解できなかったので簡単なものから理解していこうと考えました。しかし、単純と思いきやハマった例を紹介します。ハマった部分を確認しようとしましたが、結果としては現状、手詰まりとな…

SPIN:LTLの記述によっては意図した検査にならない?

前回モデル(SPIN:モデル(安全性(排他)と応答性) - プログラミングなどなど)でLTLで検証式を記述する際に実は、トライ&エラーを行っていました。その際、記述したLTLで想定していた検査が行われていないようなケースがありました。 そもそも、記述したLTLが誤…

SPIN:モデル(安全性(排他)と応答性)

LTLに少し慣れた気がしたので、簡単なモデルを記述し練習してみることにしました。モデルとしては、サーバでは標準で第1サービスが有効になっているが、運用者から第2サービスの開始操作があった場合に、サービスを切り替えるというものです。サービスは排他…

SPIN:2プロセスからのメッセージ受信順序確認

前回(SPIN:LTLを使った2プロセスの実行順序確認 - プログラミングなどなど)の内容と似ていますが、今度は2つのプロセスA,BがプロセスCにメッセージ送信する例を考えてみました。前回の内容とほぼ同じなので、同じオプションで結果が得られると考えていました…

SPIN:LTLを使った2プロセスの実行順序確認

SPINでは記述したモデルについてLTLで記述した性質の検証を行うことで反例がないかどうかをチェックしてくれます。私はまだ理解が浅いのでLTLで記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した…

SPIN:1信号(赤青黃)の遷移サンプル

「SPINによる設計モデル検証」のNever Claimの2信号サンプルがあるのですが、自身の勉強としてもっと簡単なサンプルから作成してみました。モデルとしては、赤から青になり、青から黄、黄から赤になる信号のモデルと、Never Claimを記述します。記述したファ…

SPIN:状態の探索(2プロセス)(探索)

前回「Pr: 0 Tr: 6」で探索が切れているように見える部分が気になったので、デバッグしてみました。調べられた感じでは、プロセスの削除順序が関係しているようです。一応、「プロセスは生成順序と逆順で消滅する」と記載のある資料を見つけたのでこの記述の…

SPIN:状態の探索(2プロセス)

今回は2プロセスが動作するサンプルモデルを作成して状態空間の探索を追ってみました。前回と同じように読み解けるかと思いきや、よくわからない動きを見ることとなりました。使用したソースは以下となります。 使用したソースから検証器の実行まで 単に2プ…

SPIN:状態探索(1プロセス,分岐あり)とグラフ化

SPINの検証器が状態空間をどのように探索しているのかが気になったので、状態ベクトルを出力させながら追ってみました。使用したソースは以下となります。 使用したソースから検証器の実行まで 分岐を2箇所に用意した計4経路を通るような以下のソースを用意…

SPIN,C言語,デバッグ:State Vectorと変数

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

SPIN:-o2オプションを使用して書き込みだけの変数も検証させる

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

SPIN:順次の実行と値

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

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

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

SPIN:3x3の魔法陣の解を求める

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

spin, panコマンドのヘルプとページャ(less)

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

SPIN:-searchオプションを指定した場合の動きについて

PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。 検証器の…