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

同僚の方が一時的な確認のために同名の関数を静的リンクした実行ファイルを作成しようとしてエラーになっていました。C言語ではできないんじゃないかな。と思っていたのですが、「HPではできたのに〜」と言っていたのを聞き、ならばGCCでもオプションでどう…

0からnまでの整数の和を求める例を題材にデバッガ(gdb)の使用例を紹介したいと思います。バグがある状態から始めます。 main.c(バグ有り) int sum(int n) { int acc = 0; int i; for (i = 0; i < n; i++) { acc += i; } return acc; } int main(void) { int …

[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)の「1.5 型に性質をもたせる HTMLの文字列エスケープ」を読んで、C言語の場合はどんな風にできるのかと思い実装してみました。おそらくコンパイル時のチェック…

今回もC言語の関数単体テスト系の話題です。mallocを利用する関数を試験する際にmallocのスタブを作成して単体試験を実行しようとすると単体試験のツール自体がmallocを使用していたりしてうまく動かないケースがあります。このような場合、GDBを使用してmal…

C言語の関数単体テストを作成している際に関数形式マクロの展開を調整したいと思う部分が出てきました。使用していたコンパイラはGCCでマニュアルを見るとマクロの読み込みを制御するオプション(-include)がありましたので、使ってみました。使用したのは以…

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

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

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

「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)コマンドのオプションが覚えられずに頻繁にヘルプを参照しています。私の環境ではヘルプを出力すると作業ターミナルの画面から溢れるのでページャを通して確認することが多いです。ページャを通すと検索機能を…

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

この文章について このページでは Coqで「Require Import Cpdt.CpdtTactics.」を実行した際に出力されたエラー「Error:Cannot find a physical path bound to logical path matching suffix Cpdt.」を解消する方法について紹介したいと思います。私がCoqの勉…

階乗を計算する関数 和に引き続き積についても同じように関数を定義したいと思います。まずは、階乗を求める関数から定義してみます。ソースは前回からの続きとなっています。 factorial01.c #include "util.h" int factorial(int n) { int acc = 1; int i; …

関数ポインタとは 関数ポインタとは関数を指すポインタのことです。私がC言語を学び始めた頃はポインタについてよく理解していないこともあり、関数ポインタが何の役に立つのかわかりませんでした。 そんな中、関数ポインタを理解するきっかけになったのは、…

プログラミング関する情報を色々書いていきたいと思います。 まずは、別のサイト向けに作成していた内容などを修正しつつ記事にしていこうと考えています。