このブログでは、現在「GCC:関数重複定義(Multiple Definition)を-z muldefsで許可する - プログラミングなどなど」が見られている回数が圧倒的に多く、全体の約半分を締めています。個人的には使用することが無かったため、なぜ、こんなに見られるのだろう…
7/22から7/25と4連休だったのと、SPINからちょっと離れたいとの思いから、HaskellのFunctorからMonadの流れを勉強してみようと思い本(プログラミングHaskell 第2版)を読んでいました。読み進める中でStateモナドを定義する前のFunctorのfmap実装がぱっと理解…
SPINでは検証式の記述に時相論理という論理が使えるのですが、よく理解できなかったので簡単なものから理解していこうと考えました。しかし、単純と思いきやハマった例を紹介します。ハマった部分を確認しようとしましたが、結果としては現状、手詰まりとな…
前回モデル(SPIN:モデル(安全性(排他)と応答性) - プログラミングなどなど)でLTLで検証式を記述する際に実は、トライ&エラーを行っていました。その際、記述したLTLで想定していた検査が行われていないようなケースがありました。 そもそも、記述したLTLが誤…
LTLに少し慣れた気がしたので、簡単なモデルを記述し練習してみることにしました。モデルとしては、サーバでは標準で第1サービスが有効になっているが、運用者から第2サービスの開始操作があった場合に、サービスを切り替えるというものです。サービスは排他…
前回(SPIN:LTLを使った2プロセスの実行順序確認 - プログラミングなどなど)の内容と似ていますが、今度は2つのプロセスA,BがプロセスCにメッセージ送信する例を考えてみました。前回の内容とほぼ同じなので、同じオプションで結果が得られると考えていました…
SPINでは記述したモデルについてLTLで記述した性質の検証を行うことで反例がないかどうかをチェックしてくれます。私はまだ理解が浅いのでLTLで記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した…
私は、普段の開発はほぼLinuxで行っています。 その際に、「コマンドのオプションなんだっけ?」とか、「関数の引数なんだっけ?」と思うことがあります。インターネットで調べるのも有りですが、ぱっと調べられるので使えるようになっていると便利です。 man…
Twitter APIを使ってみようと思ったのですが、認証やら何やらが必要になりそうでした。これまでWebAPIは使ったことがなかったので、ひつまず手に届きそうな天気情報を取得するものから試してみました。 お天気Webサービス仕様 手に届きそうなものを探してい…
gprologのFDの練習として、SPINで以前に書いた3x3の魔法陣の解を求めてみます。gprologのソースファイルにはサンプルが含まれています。その中にmagsq.plがあり、魔法陣のサイズを指定できるものがあります。 ソース ms.pl /* 魔法陣 */ ms(MS) :- MS = [ V1…
gprologのマニュアルを見ていると「9 Finite domain solver and built-in predicates」という章がありました。「9.1 introduction」にも「constraint solver」という記述があるので、何らかの制約問題を解いてくれるのかと思い試して見ました。簡単そうなサ…
基本情報技術者試験で出てくるアローダイヤグラムでクリティカルパスを求める問題ですが、prologを使うとスッキリかけるのではないかと思い挑戦してみました。使用したprologの処理系はgprologとなります。問題は以下のようなものでした。問題のダイアグラム…
「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の勉…
