AlloyAlloy の公式ページの Tutorial やってみる 2
前回の続き． Chapter. 2 ファイルシステムを記述した例をもとに説明を行う． // A file system object in the file system sig FSObject { parent: lone Dir }...
2020-05
AlloyAlloyAlloy の公式ページの 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 探して読んでください． モデル検査入門 ここでは「...