Promela

プロセス

イニシャルプロセスの定義

initはイニシャルプロセスを定義する。

init {
  printf("init\n");
}

プロセスの定義

プロセスの定義はproctypeを使用する。

proctype P1(){
  printf("hello");
}

proctype P2(int x){
  printf("x=%d\n");
}

プロセスの実行

定義されたプロセスの実行にはrunを使用する。

init {
  run P1();
  run P2(100);
}

proctype P1(){
  printf("hello\n");
}

proctype P2(int x){
  printf("x=%d\n",x);
}

プロセスの定義にactiveを付けると、イニシャル時にプロセスの実行を始める。 Nを指定すると複数のプロセスを実行する。

active proctype P(){
  printf("hello pid=%d",_pid);
}

#define N 5
active [N] proctype Pn(){
  printf("hello pid=%d",_pid);
}

条件文と制御文

繰り返し

proctype P(){
  do
    :: printf("A\n");
    :: printf("B\n");
    :: printf("C\n");
  od;
}

条件文

proctype P(){
  int n = 10;
  if
    :: (n < 5) -> printf("A\n");
    :: (n == 10) -> printf("B\n");
    :: else -> printf("C\n");
  fi
}

goto文

proctype P(){
  goto label;
  printf("A");
label:
  printf("B");
}

通信チャンネル

同期通信

chan ch = [0] of {int,int};

非同期通信

chan ch = [1] of {int,int};

データの送信と受信

• データの送信

"!!"を使用するとチャンネルにメッセージがソートされ格納される。

ch ! 100,200;
ch !! 100,200;

• データの受信

• チャンネルの先頭からメッセージを取り出す(FIFO)

int x,y;
ch ? x,y;

• 条件を指定してにメッセージを取り出す

値を指定すると、値が一致したメッセージを取り出す。

chan ch = [5] of {int,int};
ch ?? x,100;

メッセージのコピー

"< >"で囲むと、メッセージと取り除かずにコピーしてメッセージを取り出す。

ch ? <x,y>;
ch ?? <x,y>;

メッセージのポーリング

"[ ]"で囲むと、変数の値は変わらない。

ch ? [x,y];
ch ?? [x,y];

値を指定して条件を指定する。

if
 ::ch ? [x,100] -> 
   ch ? x,100;
   /*何か処理を行う*/ 
fi

関数

• full
• empty
• nfull
• nempty
• len

チャンネルが一杯かチャンネルの状態を確認する

if
 ::(full(ch)) -> skip;
fi

Note

• 条件文ではelseを使用しない。empty/nemptyとfull/nfullを対になるようにする。
• _pidを値に変換するにはeval(_pid)とする。