「SPIN例題1」の編集履歴（バックアップ）一覧はこちら

「SPIN例題1」(2011/02/04 (金) 13:54:52) の最新版変更点

追加された行は緑色になります。

削除された行は赤色になります。

簡単な説明と簡単な例で簡単に雰囲気をつかみたい。
spinがインストールしてあるのが前提。
----
&bold(){&u(){構造：}}
　Promelaが扱う主なデータタイプは以下の通り
|BGCOLOR(#DCDCDC):データタイプ|BGCOLOR(#DCDCDC):値の範囲|BGCOLOR(#DCDCDC):補足|
|bit|0..1|1bit|
|bool|false, true|1bitでfが0でtが1|
|byte|0..255|8bit|
|short|-2^15..-2^15-1|符号付16bit|
|int|-2^31..-2^31-1|符号付32bit|
　すべてintで宣言すればいいわけではなく、状態が多くなりすぎて検査できない（いわゆる状態爆発）を防ぐために、intよりshort、shortよりbyte、byteよりbitなどと小さくしていくと無駄がなくなってモデル的にも良い、と言われている。

他には、mtypeやpid、unsignedがある。mtypeは良く使うので後に例を書きたいと思う。pidはプロセスの識別子でこれも後に説明したいと思う。unsignedは使っているところあまり見かけないのでスルー。
----
&bold(){&u(){例題：}}
　そういったわけで、すごく簡単な例を書いてみる。
「nが5まで1つずつ増えて5になったら0になるカウンター」

Promela/SPINも含むモデル検査は状態遷移(オートマトン)の枠組みを基本としているので、状態遷移をまず考える。
&space(10)&ref(5n_e.png,,title=カウンターの状態遷移図)
カウンターの状態遷移。
もっと一般化すると以下のようになる。
#ref(5n.png)

以上のモデルを考えてから、それをもとにPromelaで記述してみる。
Promelaはプロセスという動作単位で構成するので、proctypeというプロセス宣言がメインになる。
#highlight(linenumber,promela){{
int n = 0;

active proctype counter(){
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
} }}
このような形になる。

最初なので細かく説明、というかメモを残しておくことにする。
1行目から
#highlight(promela){
int n = 0;}
いわゆるグローバル変数の宣言。どのプロセスからもアクセスできる。宣言と同時に0で初期化。SPINの日本語解説書では大域変数という名称で書かれていることが多いので、大域変数と呼ぶことにする。
　大域変数があるということは局所変数（ローカル変数）もあるわけで、プロセス宣言内に変数を宣言すれば局所変数で、スコープ一般的なプログラミング言語と同じだと思います。（スコープは厳密に確認していないが…）

次にメインとなるプロセス宣言。
#highlight(promela){{
active proctype counter(){
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
} }}
　proctypeで囲まれた部分がプロセス宣言。counterという名前のプロセスである。宣言の形は以下の通り。
#aa(blockquote){{proctype プロセス名 (引数) {
  ...中身... 
} }}
　こんな形で宣言する。
　proctypeの前に&bold(){active}とついているのは、プロセス生成したらすぐ実行しますよ(activeになる)という意味の宣言。任意のタイミングでプロセスを実行したい場合は、あとで説明するinitを使ったり使わなかったりするとできる。そのうち説明したい。

　次にプロセスの中身について。上のコードでは以下の部分
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
　この処理はdo文といって、いわゆるループ文で書き方は
#aa(blockquote){do
  ::(ガード条件文) -> 文; 文; 文; ...
  ::(ガード条件文) -> 文; 文; 文; ...
                 ...
                 ...
od;
}
　となる。また、if文も同じように記述でき
#aa(blockquote){if
  ::(ガード条件文) -> 文; 文; 文; ...
  ::(ガード条件文) -> 文; 文; 文; ...
                 ...
                 ...
fi;
}
　こうなる。do文とif文の違いは、ループを行うか行わないかの違いだけで基本的には同じ。

　で、こういうif文やdo文の構造はガードコマンドと言う。参考リンク：http://ja.wikipedia.org/wiki/Guarded_Command_Language
　動きとしては、
ガード条件が発火する(trueになる)のであれば->以降の文を実行することができる。もし発火しない(falseになる)場合は、ガードが発火するまで実行をブロックし待ち続ける。ガード条件が複数ある場合も同じ。

　C言語などのif文の条件は真にならなければ、そのまま次のステップに進むが、Promelaはガード条件が真にならない場合は真になるまで待ち続けるのが大きな違い。
　ちなみに ::else -> 文;という風にも書け、真にならない場合に実行される。

　またPromelaは非決定性を持つので、ガード条件が複数発火してもよく、その場合には実行はランダムに選ばれる。
　たとえば
#aa(blockquote){do
  ::(n < 3) -> printf("nは3以下");
  ::(n < 4) -> printf("nは4以下");
od;}
　のように書いてnが2だった場合、どちらの条件も発火可能であり、実行はランダムにどちらかが選ばれる。
　ちなみにprintfは使えるが、コンパイルしたときには完全に無視されるので注意。

　Promelaでは文1つを遷移と考える状態遷移系として考える
atode
----
&bold(){&u(){実行：}}
　ということで、書いたら保存して実行してみる。ちなみに拡張子は何でもよい。参考書などでは.pや.prom、.pmlといろいろあるが、おそらく.pmlが一番多数派だと思う。
　シミュレーション実行は以下の通り
|&bold(){spin -p <filename>}|
　コマンドプロンプトなりバッシュなりでコマンドを打つ。
　-pはプロセスの状態変化を画面に出力するオプションで、これを打たずに実行すると画面に何も表示されない。
　この例題は無限ループを起こすように書いてあるので上記のコマンドを打つと画面にザザーとずっと状態が出力される。ひたすらシミュレーションをしている状態なのだけども、これはこれで意図通り。
#aa(blockquote){{　　...
7210:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7211:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7212:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7213:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7214:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7215:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7216:	proc  0 (counter) ex1.pml:4 (state 5)	[((n==5))]
7217:	proc  0 (counter) ex1.pml:6 (state 4)	[n = 0]
7218:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7219:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7220:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7221:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7222:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7223:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7224:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7225:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7226:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7227:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7228:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7229:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7230:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7231:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
　　...}}
----
　補足：他にも覚えておくと幸せになるオプション(シミュレーション時のみ)をいくつかあげておきます。
1.
|大域変数の状態を画面に出したい|
|&bold(){spin -g <filename>}|
2.
|局所変数の状態も出したい|
|&bold(){spin -l <filename>}|
3.
|対話的(interactive)にシミュレーション実行したい|
|&bold(){spin -i <filename>}|
4.
|そもそもヘルプを出して自分で見たい|
|&bold(){spin --h}|
　ぐらいです。spin -p -l -g <filename>とかで組み合わせることもできます。

　このモデルで検証してもあまり意味がないので、検証のコマンドは次に。　

簡単な説明と簡単な例で簡単に雰囲気をつかみたい。
spinがインストールしてあるのが前提。
----
&bold(){&u(){構造：}}
　Promelaが扱う主なデータタイプは以下の通り
|BGCOLOR(#DCDCDC):データタイプ|BGCOLOR(#DCDCDC):値の範囲|BGCOLOR(#DCDCDC):補足|
|bit|0..1|1bit|
|bool|false, true|1bitでfが0でtが1|
|byte|0..255|8bit|
|short|-2^15..-2^15-1|符号付16bit|
|int|-2^31..-2^31-1|符号付32bit|
　すべてintで宣言すればいいわけではなく、状態が多くなりすぎて検査できない（いわゆる状態爆発）を防ぐために、intよりshort、shortよりbyte、byteよりbitなどと小さくしていくと無駄がなくなってモデル的にも良い、と言われている。

他には、mtypeやpid、unsignedがある。mtypeは良く使うので後に例を書きたいと思う。pidはプロセスの識別子でこれも後に説明したいと思う。unsignedは使っているところあまり見かけないのでスルー。
----
&bold(){&u(){例題：}}
　そういったわけで、すごく簡単な例を書いてみる。
「nが5まで1つずつ増えて5になったら0になるカウンター」

Promela/SPINも含むモデル検査は状態遷移(オートマトン)の枠組みを基本としているので、状態遷移をまず考える。
&space(10)&ref(5n_e.png,,title=カウンターの状態遷移図)
カウンターの状態遷移。
もっと一般化すると以下のようになる。
#ref(5n.png)

以上のモデルを考えてから、それをもとにPromelaで記述してみる。
Promelaはプロセスという動作単位で構成するので、proctypeというプロセス宣言がメインになる。
#highlight(linenumber,promela){{
int n = 0;

active proctype counter(){
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
} }}
このような形になる。

最初なので細かく説明、というかメモを残しておくことにする。
1行目から
#highlight(promela){
int n = 0;}
いわゆるグローバル変数の宣言。どのプロセスからもアクセスできる。宣言と同時に0で初期化。SPINの日本語解説書では大域変数という名称で書かれていることが多いので、大域変数と呼ぶことにする。
　大域変数があるということは局所変数（ローカル変数）もあるわけで、プロセス宣言内に変数を宣言すれば局所変数で、スコープ一般的なプログラミング言語と同じだと思います。（スコープは厳密に確認していないが…）

次にメインとなるプロセス宣言。
#highlight(promela){{
active proctype counter(){
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
} }}
　proctypeで囲まれた部分がプロセス宣言。counterという名前のプロセスである。宣言の形は以下の通り。
#aa(blockquote){{proctype プロセス名 (引数) {
  ...中身... 
} }}
　こんな形で宣言する。
　proctypeの前に&bold(){active}とついているのは、プロセス生成したらすぐ実行しますよ(activeになる)という意味の宣言。任意のタイミングでプロセスを実行したい場合は、あとで説明するinitを使ったり使わなかったりするとできる。そのうち説明したい。

　次にプロセスの中身について。上のコードでは以下の部分
  do
    ::(n < 5) -> n++;
    ::(n == 5) -> n = 0;
  od;
　この処理はdo文といって、いわゆるループ文で書き方は
#aa(blockquote){do
  ::(ガード条件文) -> 文; 文; 文; ...
  ::(ガード条件文) -> 文; 文; 文; ...
                 ...
                 ...
od;
}
　となる。また、if文も同じように記述でき
#aa(blockquote){if
  ::(ガード条件文) -> 文; 文; 文; ...
  ::(ガード条件文) -> 文; 文; 文; ...
                 ...
                 ...
fi;
}
　こうなる。do文とif文の違いは、ループを行うか行わないかの違いだけで基本的には同じ。

　で、こういうif文やdo文の構造はガードコマンドと言う。参考リンク：http://ja.wikipedia.org/wiki/Guarded_Command_Language
　動きとしては、
ガード条件が発火する(trueになる)のであれば->以降の文を実行することができる。もし発火しない(falseになる)場合は、ガードが発火するまで実行をブロックし待ち続ける。ガード条件が複数ある場合も同じ。

　C言語などのif文の条件は真にならなければ、そのまま次のステップに進むが、Promelaはガード条件が真にならない場合は真になるまで待ち続けるのが大きな違い。
　ちなみに ::else -> 文;という風にも書け、真にならない場合に実行される。

　またPromelaは非決定性を持つので、ガード条件が複数発火してもよく、その場合には実行はランダムに選ばれる。
　たとえば
#aa(blockquote){do
  ::(n < 3) -> printf("nは3以下");
  ::(n < 4) -> printf("nは4以下");
od;}
　のように書いてnが2だった場合、どちらの条件も発火可能であり、実行はランダムにどちらかが選ばれる。
　ちなみにprintfは使えるが、コンパイルしたときには完全に無視されるので注意。
----
&bold(){&u(){実行：}}
　ということで、書いたら保存して実行してみる。ちなみに拡張子は何でもよい。参考書などでは.pや.prom、.pmlといろいろあるが、おそらく.pmlが一番多数派だと思う。
　シミュレーション実行は以下の通り
|&bold(){spin -p <filename>}|
　コマンドプロンプトなりバッシュなりでコマンドを打つ。
　-pはプロセスの状態変化を画面に出力するオプションで、これを打たずに実行すると画面に何も表示されない。
　この例題は無限ループを起こすように書いてあるので上記のコマンドを打つと画面にザザーとずっと状態が出力される。ひたすらシミュレーションをしている状態なのだけども、これはこれで意図通り。
#aa(blockquote){{　　...
7210:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7211:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7212:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7213:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7214:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7215:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7216:	proc  0 (counter) ex1.pml:4 (state 5)	[((n==5))]
7217:	proc  0 (counter) ex1.pml:6 (state 4)	[n = 0]
7218:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7219:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7220:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7221:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7222:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7223:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7224:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7225:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7226:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7227:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7228:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
7229:	proc  0 (counter) ex1.pml:5 (state 2)	[n = (n+1)]
7230:	proc  0 (counter) ex1.pml:8 (state 6)	[.(goto)]
7231:	proc  0 (counter) ex1.pml:4 (state 5)	[((n<5))]
　　...}}
----
　補足：他にも覚えておくと幸せになるオプション(シミュレーション時のみ)をいくつかあげておきます。
1.
|大域変数の状態を画面に出したい|
|&bold(){spin -g <filename>}|
2.
|局所変数の状態も出したい|
|&bold(){spin -l <filename>}|
3.
|対話的(interactive)にシミュレーション実行したい|
|&bold(){spin -i <filename>}|
4.
|そもそもヘルプを出して自分で見たい|
|&bold(){spin --h}|
　ぐらいです。spin -p -l -g <filename>とかで組み合わせることもできます。

　このモデルで検証してもあまり意味がないので、検証のコマンドは次に。