y-taka-23

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.

y-taka-23

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).

y-taka-23

/*
 * Leader Election by Chang-Roberts Algorithm
 */

byte leader = 0;  /* number of leaders */

proctype Node(chan ch_in, ch_out) {
    
    byte tok;
    

y-taka-23

名古屋モデル検査勉強会 #2

前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。

LTL 式による検査

LTL 式の構文

SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。

y-taka-23

/*
 * 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

y-taka-23

// **************************************************
//  通信チャネルとしてキューを用いたモデル
// **************************************************

open util/ordering[Time]
open alloy_queue[Request]

sig Time {}            // 時刻パラメータ
sig Client, Server {}  // 通信に参加するクライアントとサーバ
sig Request {}         // クライアントがサーバに送るメッセージ

y-taka-23

// ************************************
//  連結リストを用いたキューのモデル
// ************************************

module alloy_queue[Value]

// ------------------------------------
//   各要素の定義
// ------------------------------------

y-taka-23

// ************************************
//   排他制御のモデル
// ************************************

// Time シグネチャに全順序構造を導入
open util/ordering [Time]

// 時刻を表すシグネチャ
sig Time {}

y-taka-23

.    
.   		  	  
.		    	 
.
.    
. 
.    	
.		    	
.	    
.     

y-taka-23

.   	
.
.    
. 
.    				
.	 		
.	  	
. 
.    		
.