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で記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した…