spin2 4/24

各プロセスはrun命令を使わないとインスタンス化しない
ただし、tt active とすればよい。

active proctype Hello() {
  hogehoge()
}

とすれば、すぐに実行される。activeをproctypeの前に書けばよいが、activeをいくつか書くと、ランダムで実行される。

プロセス間通信をSPINで模倣するには、大域変数を使う。→しかし、大域変数はすべてのプロセスからアクセス可能で、他のプロセスから干渉される可能性がある。

bool x;
active proctype A() {
  x == 1;
  x = 0;
}
active proctype B() {
  x == 0;
  x = 1;
}

さらに、変数の値を変えたとき、同期させることが難しい。
そのため、promelaではチャネルを使う

チャネル
chan チャネル名 = [個数] of {型を並べる};
個数はチャネル内に貯まるデータの数を示す. 0なら同期通信
型は基本型、レコード、mtypeなどがつかえる

プロセス内で!を使用すると、信号を発信する
チャネル名 ! 値あるいは変数の並び

プロセス内で?を使用すると、信号を受信する
チャネル名 ? 値あるいは変数の並び

• 変数を書いたとき、その変数にチャネルから読み取った値を格納する

実行時にオプション-cを指定すると実行確認できる。