代数演算子
CSPではプロセス間の様々なデータの受け渡しをチャネルを用いたメッセージパッシング方式で行う。 channel ch:{0..7} -- チャネルchの型を{0,1,・・,6,7}とする。 P = ch!5 -> SKIP -- '!'は送信を意味する。 Q = ch?x -> SKIP -- '?'は受信を意味する。 SYS…
conditional choice "if b then P else Q" は bがTRUEの場合プロセスPが、bがFALSEの場合はプロセスQが実行される。例えば、ジュースの残数を保持している自販機VMRの例を考える。 channel coin, juice VMCNT(n) = coin -> juice -> VMCNT(n-1) VMR = VMCNT(…
renaming P[ [e channel coin,coke,lemonade,cider,drink PERSON = coin -> ( coke -> drink -> SKIP |~| lemonade -> drink -> SKIP ) MIKE = PERSON[[ lemonade<-cider ]] -- このプロセスは次のようになる。 MIKE = coin -> ( coke -> drink -> SKIP |~| …
interrupt '/\' は P/\Q でプロセスPの実行中に Q が割り込む可能性を表す。プロセスP 実行中にプロセス Q のイベントが起こると Q に実行が移る。その後 P に実行は戻らない。親子が自販機でジュースを買うときに、親がコインを入れボタンを押そうとすると…
hiding'\'は (PROCESS) \ {(events)} と記述し、プロセスのアルファベット（インターフェイス）から指定したイベントを隠蔽する。下記の sharing で考えた例を使って解説する。 channel coin, coke, cider, lemonade, drink MIKE = coin -> ( coke -> drink …
interleaving P|||Q はプロセスP,Q がイベントで同期せずに、完全に独立して動作することを表す。例えば、以下のようなMIKEとRISAの動作を考える。 channel coin, coke, cider,lemonade, drink MIKE = coin -> ( coke -> drink -> SKIP |~| cider -> drink -…
interleaving の例において、MIKEとRISAはコインを別々に入れるが、二人で乾杯して同時に飲み始めるような場合はsharing（共有）を使う。 P[|{event}|]Q のように記述すると指定されたイベントで同期し、それ以外のイベントについては interleavingと同じく…
アルファベット プロセスのアルファベットを定義しておく。プロセスP のアルファベットαP とは P の持つべきイベントの集合である。例えば、 channel coin, coke, lemonade,drink VMS = coin -> ( coke -> VMS [] lemonade -> VMS ) aVMS = {coin, coke, lem…
internal choice '|~|'はプロセスの内部選択を表す。外部選択との違いを購入者の例を使って説明する。購入者はコインを入れ、コーラかレモネードを購入した後にそれを飲む。コーラとレモネードの選択は購入者自身の好みや気分によって決定されるとする。 cha…
external choice P[]Q はプロセスの選択を意味する。プロセスP,Q のどちらのイベントが先に起こるかによって実行するプロセスが決定される。 例えば、コインを入れた後、いくつかの種類が選べる自動販売機は次のようになる。 channel coin, coke, lemonade V…
何度も繰り返し販売できる自動販売機は再帰を用いて次のように記述できる。 VMR = coin -> juice -> VMR プロセスVMRはイベント coin,juice の後、再び自身VMRに移っている。VMRはcoin,juice,coin,juice,・・・を繰り返すプロセスである。また、VMRは次のよ…
seqential ';' は P;Q で、プロセスP,Q の逐次処理を表わす。ただし、プロセスP が SKIP になったときにのみプロセスQに実行が移る。２回の販売で終了する自動販売機は以下のように書けた。 channel coin, juice VM2 = coin -> juice -> coin -> juice -> SK…
簡単な例 これから幾つかの代数演算子を簡単な例を用いて解説していく。CSPは主に並行システムを記述するものであるが、まずは身近な例であるジュースの自動販売機と購入者の相互作用を例にモデル記述していくことにする。自販機と購入者の動作（イベント）…
