前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。
SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。
IDENTIFICATION DIVISION. | |
PROGRAM-ID. FIBONACCI. | |
DATA DIVISION. | |
WORKING-STORAGE SECTION. | |
01 ARGUMENT PIC 9(2). | |
01 RETURN-VALUE PIC 9(25). | |
01 RESULT PIC Z(25). | |
01 DP-TABLE. | |
03 VALS PIC 9(25) OCCURS 99. |
IDENTIFICATION DIVISION. | |
PROGRAM-ID. RNPCALC. | |
DATA DIVISION. | |
WORKING-STORAGE SECTION. | |
01 STACK-POS PIC 9(2) VALUE 1. | |
01 STACK. | |
03 STACK-DATA PIC 9(4) OCCURS 10 VALUE 0. | |
01 EXPR PIC X(20). | |
01 EXPR-POS PIC 9(2). |
/* | |
* Leader Election by Chang-Roberts Algorithm | |
*/ | |
byte leader = 0; /* number of leaders */ | |
proctype Node(chan ch_in, ch_out) { | |
byte tok; | |
前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。
SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。
/* | |
* Impossibility of the 8-Puzzle | |
* | |
* NOTICE: For full statespace search, run-time option -m230000 needed, e.g. | |
* $ spin -a promela_8puzzle.pml | |
* $ gcc -o pan pan.c | |
* $ ./pan -m230000 | |
*/ | |
#define SPACE 0 |
// ************************************************** | |
// 通信チャネルとしてキューを用いたモデル | |
// ************************************************** | |
open util/ordering[Time] | |
open alloy_queue[Request] | |
sig Time {} // 時刻パラメータ | |
sig Client, Server {} // 通信に参加するクライアントとサーバ | |
sig Request {} // クライアントがサーバに送るメッセージ |
// ************************************ | |
// 連結リストを用いたキューのモデル | |
// ************************************ | |
module alloy_queue[Value] | |
// ------------------------------------ | |
// 各要素の定義 | |
// ------------------------------------ |
// ************************************ | |
// 排他制御のモデル | |
// ************************************ | |
// Time シグネチャに全順序構造を導入 | |
open util/ordering [Time] | |
// 時刻を表すシグネチャ | |
sig Time {} |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. | |
. |