y-taka-23

open util/ordering[Time]

sig Time {}

abstract sig Event {
    pre, post : Time,
} {
    post = pre.next
}

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

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

.    
.   		  	  
.		    	 
.
.    
. 
.    	
.		    	
.	    
.     

y-taka-23

.    
.
.    
.    
. 
. 	
.	 			 
.    						
.	  	
.	  		

y-taka-23

// ************************************
//   群のモデル
// ************************************

// ------------------------------------
//   群の公理
// ------------------------------------

// 群の元
sig Element {