TypeScriptTypeScript でシーケント計算自動化（トークン化編）
命題論理のシーケント自動計算機 - Tokenizer の実装 やりたいこと シーケント計算自動化 形式手法を使えるようになりたいと思って何度か Alloy に取り組んでみましたが，根本的に数理論理学がわかっていないので，一旦数理論理学を勉...
TypeScriptJavajna で DLL が呼び出せなかった話
事象 サーブレットから jna を使用して dll を呼び出せなかった． jna をビルドパスにも含んでいるし，コードに書かれたかディレクトリに dll を配置していたけども，「hoge.dll が見つかりません」とエラーが出た（具体的な ...
AlloyAlloy Analyzer 動かしてみた その 1
Alloy Analyzer について軽く文法を調べれたので，試しに動かしてみました． サンプル 問題 A, B, C, D の 4 人は，総務，外務，財務，防衛の 4 つの大臣に重複なく割り振られる．割り振りに関して，以下の情報が得られた...
AlloyAlloy Analyzer チートシート（全体の文法編）
永遠の暫定版．間違ってたらコメント下さい．わからないで書いているところもあるので，ほぼ私のためのメモになっています…（言い訳）． 全体像 モジュールヘッダ module hoge から書く．書いているモデルのモジュール名に当たると思われる...
AlloyAlloy Analyzer チートシート（論理式の文法編）
Alloy Analyzer を使ってみようと思ってはや数ヶ月，いくつか文献を見たけど無定義で記号が使われたりしていたりでぶん投げ続けていますが，もう日本語で文献を調べるのはやめました． 初歩の初歩は でググるのが一番ですね． ということ...
AlloyAlloy の公式ページの Tutorial やってみる 2
前回の続き． Chapter. 2 ファイルシステムを記述した例をもとに説明を行う． // A file system object in the file system sig FSObject { parent: lone Dir }...
AlloyAlloy の公式ページの Tutorial やってみる 1
Tutorial for Alloy Analyzer 4.0 和訳というほどではないですが，簡単にまとめます．元の Tutorial は こちら． いろいろ端折ったり意訳したりしてるので，参考程度で～． Chapter. 0 Approa...
数理論理学モデル検査入門の PDF を読んだまとめ 3（完結）
モデル検査入門の PDF を読んだまとめ 2の続きです． 第 6 章 CTL モデル検査 モデル検査を実施するためには， 検証したいシステムを Kripke モデル M として表現し， 検証したい性質を状態論理式 \varphi で表し（...
数理論理学モデル検査入門の PDF を読んだまとめ 2
モデル検査入門の PDF を読んだまとめ 1のつづき． 第 3 章 様相理論 K 様相理論は「今後どうなる」みたいな時相を取り扱うことになる． そのために，K-論理式を定義して（論理演算子 \Box を追加する）おく． 状態遷移を取り扱うた...
数理論理学モデル検査入門の PDF を読んだまとめ1
「モデル検査入門」でググると上位に京大の数理研 2009 年の講義ノートと思われる PDF が見つかるので読んでみた．自分用のまとめなので他人の参考にならないかもしれない．詳しくは PDF 探して読んでください． モデル検査入門 ここでは「...