2009-04-25

hiding(隠蔽)

hiding'\'は (PROCESS) \ {(events)} と記述し、プロセスのアルファベット（インターフェイス）から指定したイベントを隠蔽する。下記の sharing で考えた例を使って解説する。

channel coin, coke, cider, lemonade, drink
MIKE = coin -> ( coke -> drink -> SKIP
                 |~|
                 cider -> drink -> SKIP )

RISA = coin -> lemonade -> drink -> SKIP

VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS
                []
                cider -> VMS )

MIKEとRISA はジュースで乾杯するとし、イベントdrink で同期する。sharing（共有）で解説したとおり、

PEOPLE = MIKE |[{drink}]| RISA

ここで、イベントdrink は PEOPLEの中でのイベントであり、VMSとは関係のないイベントである。そこでこのイベントを PEOPLEの内部に隠蔽する。
MIKE と RISA が２人だけで乾杯するとき、PEOPLEの外部との相互作用としてイベントdrink は見えていないことが適切であり、例えば他に drinkイベントを持つKEN が現われても、もはや MIKE と RISA の乾杯には干渉できない。*1
プロセスPEOPLE と VMSは coin,coke,lemonade,ciderで同期をとる。

 PEOPLE = MIKE |[{drink}]| RISA \ {drink}

 aPEOPLE = {coin,coke,lemonade,cider}
 -- aPEOPLE = aMIKE ∪ aRISA - {drink}

 aVMS = {coin,coke,lemonade,cider}

 SYSTEM = PEOPLE [aPEOPLE||aVMS] VMS

*1:もちろん、KEN が２人の乾杯に参加するような場合はイベントdrink を隠蔽しない。

2009-04-25

interleaving

代数演算子

interleaving P|||Q はプロセスP,Q がイベントで同期せずに、完全に独立して動作することを表す。例えば、以下のようなMIKEとRISAの動作を考える。

channel coin, coke, cider,lemonade, drink
MIKE = coin -> ( coke -> drink -> SKIP
                 |~|
                 cider -> drink -> SKIP )

RISA = coin -> lemonade -> drink -> SKIP

MIKEはコーラかサイダーを飲み、RISAはレモネードしか飲まないとする。MIKEとRISAは共通のイベントcoin, drink を持つが、このイベントで２人が同期するわけではない。２人で一緒にコインを入れるわけではないし、２人で同時に飲むとは限らないだろう。このような場合はinterleavingで記述する。

 PEOPLE = MIKE ||| RISA
 
 aPEOPLE = {coin,coke,cider,lemonade,drink}
 --      = aMIKE ∪ aRISA

この記述ではMIKEとRISAはすべてのイベントをそれぞれ別々に起こす。
さらにVMSとの関係を記述してみよう。

VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS
                []
                cider -> VMS )

aVMS = {coin,coke,lemonade,cider}

SYSTEM = VMS [aVMS||aPEOPLE] PEOPLE

 -- SYSTEMの実行例
 -- <coin(MIKE),coke,coin(RISA),drink(MIKE),lemonade,drink(RISA)>

MIKEが先に coin のイベントを起こした後は MIKEがジュースを選びVMSが再び最初の状態に戻るまで、RISAはイベントcoinを起こすことはできない。（VMSのcoinと同期する必要があるので。）
VMSはMIKEとRISAの起こすイベントcoin,coke,lemonade,ciderで同期しているが、これらを起こしたのが MIKE であるか RISA であるかは考慮していない。プロセスPEOPLE とイベント同期しているだけである。

2009-04-25

sharing(共有)

代数演算子

interleaving の例において、MIKEとRISAはコインを別々に入れるが、二人で乾杯して同時に飲み始めるような場合はsharing（共有）を使う。
P[|{event}|]Q　のように記述すると指定されたイベントで同期し、それ以外のイベントについては interleavingと同じく別々に起こす。

channel coin, coke, cider, lemonade, drink
MIKE = coin -> ( coke -> drink -> SKIP
                 |~|
                 cider -> drink -> SKIP )

RISA = coin -> lemonade -> drink -> SKIP

PEOPLE = MIKE |[{drink}]| RISA

 --    PEOPLEの実行例
 -- < coin(RISA),lemonade,coin(MIKE),cider,drink(RISA&MIKE) >

プロセスPEOPLE はMIKE と RISA のどちらが先にコインを入れてジュースを買うかはわからないが、drinkのイベントでは必ず同期する。イベントcoin はMIKEとRISAが別々に起こすので2度起きるが、drink は2人で同期するので１度しか起こらない。

sharingの同期するイベントを空とすると、interleaving に等しい。

P[|{}|]Q ＝ P|||Q

2009-04-24

parallel(並行)

代数演算子

アルファベット

プロセスのアルファベットを定義しておく。プロセスP のアルファベットαP とは P の持つべきイベントの集合である。例えば、

channel coin, coke, lemonade,drink
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

aVMS = {coin, coke, lemonade}  -- VMSのアルファベット

PERSON = coin -> ( coke -> drink -> PERSON
                   |~|
                   lemonade -> drink -> PERSON )

aPERSON = {coin, coke, lemonade, drink}

parallel（並行）

P[αP||αQ]Q *1でプロセスP,Qの並行動作を表す。αPとαQの共通のイベントでPとQは同期する。

これまで購入者(PERSON)と自販機(VMS)を記述してきたので、これらが互いに作用しながら動作するシステムの記述を行おう。PERSONとVMSはそれぞれの共通イベントcoin,coke,lemonadeで同期する。drinkはPERSONのみが行うので自販機と同期しない。

 SYSTEM = VMS[{coin,coke,lemonade}||{coin,coke,lemonade,drink}]PERSON
 
 -- 次のように書いても同じ。
 aVMS = {coin, coke, lemonade}
 aPERSON = {coin, coke, lemonade, drink} 
 SYSTEM = VMS [aVMS||aPERSON] PERSON

プロセスSYSTEMは１〜４を繰り返す。

VMS,PERSONともにイベントcoin が起こせる（ready）状態にあるので、coinのイベントが起こりVMS、PERSONともに次のプロセスに移る。
PERSONはcoke->drink->PERSON または lemonade->drink->PERSON のどちらかのプロセスを選択している。
前者[後者] の場合、イベントcoke[lemonade] で同期しPERSONは次のプロセスに移り、VMSは自身に戻る。
PERSONはイベントdrinkを起こし、最初の状態に戻る。

外部選択と環境

上記のSYSTEMは PERSONが内部選択で coke,lemonade どちらのイベントを起こすかを選択していると言えるが、ここでPERSONも外部選択を行うような場合を考えてみよう。例えば、購入者がcoke,lemonade 両方のボタンを同時に押して決定を自販機に任せるような場合である。

VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

PERSON = coin -> ( coke -> drink -> PERSON
                   []
                   lemonade -> drink -> PERSON )

SYSTEM = VMS [aVMS||aPERSON] PERSON

このように PERSON（またはVMS)の外部選択のどちらのイベントも実行可能な場合、この選択は非決定的（内部選択）になる。つまり、coke, lemonade のどちらのイベントが起こるかは分からないが、どちらかのイベントは起こる。実際に自販機のボタンを２つ同時に押したとき、どのような決定のされ方をするのかは自販機によるだろう。

 --イベント a,b が共に起こり得る（ready）状態ならば、
 ( a->P [] b->Q ) ≡ ( a->P |~| b->Q )

このことから、選択に関するイベントが同じ場合は常に非決定的になる。

( a->P [] a->Q ) ≡ ( a->P |~| a->Q )

*1:よく P||Q で省略表記する。

2009-04-24

internal choice(内部選択)

代数演算子

internal choice '|~|'はプロセスの内部選択を表す。外部選択との違いを購入者の例を使って説明する。

購入者はコインを入れ、コーラかレモネードを購入した後にそれを飲む。コーラとレモネードの選択は購入者自身の好みや気分によって決定されるとする。

channel coin, coke, lemonade, drink
PERSON = coin -> ( coke -> drink -> SKIP
                   |~|
                   lemonade -> drink -> SKIP )

ここでは、プロセスcoke->drink->SKIP, lemonade->drink->SKIPの選択を内部選択とした。'内部'の意味はその選択が外部（自販機）によらず PERSON自身によって決定されるということである。もしコーディングする際は、この選択は交互でもランダムでも常にどちらか片方のみを選ぶとしてもよい。*1

また、この選択がいつ行われているのかはPERSONの外部からは分からない。コインを入れる前にすでに決まっていても、コインを入れた後に選択していても、外部にとっては同じである。つまり、次のように PERSON を記述してもまったく先と同様なプロセスとなる。

 PERSON = coin -> coke -> drink -> SKIP
          |~|
          coin -> lemonade -> drink -> SKIP

一方で、下記の自販機VMSはプロセスcoke->VMS, lemonade->VMSを外部選択としている。この選択はVMS自身だけで決定するのではなく coke, lemonade どちらのイベントが起きるかは外部（購入者）によるということである。

channel coin, coke, lemonade
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

プロセスPERSONにdrinkという動作（イベント）を定義したが、これはVMSとは関係がないイベントである。drinkは単なる動作としても良いが、例えば二人で乾杯するときなどは相互作用となるだろう。これは後の例で。

*1:内部選択で記述されたプロセスはこれらすべての可能性を考え検証している。

2009-04-22

external choice(外部選択)

代数演算子

external choice P[]Q はプロセスの選択を意味する。プロセスP,Q のどちらのイベントが先に起こるかによって実行するプロセスが決定される。
例えば、コインを入れた後、いくつかの種類が選べる自動販売機は次のようになる。

channel coin, coke, lemonade
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

プロセスVMSはイベント coin の後、coke->VMS, lemonade->VMS のexternal choice'[]'となっている。イベントcoke,lemonade のどちらが起きるかで次に実行されるプロセスが選択される。今回はどちらイベントが起きても再びVMSに戻る。external（外部）の意味は、この選択がVMS自身だけでなく外部の要因(今回は購入者？)が関与するということである。*1

括弧()をなくして記述してしまうと次のように coin と lemonade で選択が行われてしまうので注意。

channel coin, coke, lemonade
VMS = coin -> coke -> VMS
      []
      lemonade -> VMS   --lemonade は無料！？

external choiceは自然に拡張できる。イベントciderを加えた場合は次のようになる。

channel cider
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS
                []
                cider -> VMS )

boolean gard

external choiceの選択はboolean gard によりその選択をガードすることができる。

例えば、コインを何枚でも自由に入れることができ、その分だけジュースが買える自動販売機VMGを考えてみる。まず、変数nで自販機に入れられたコインの枚数をカウントすることにする。

VMG(n) = coin -> VMG(n+1)

VMGはコインを入れるかジュースを出すかを選択でき、ジュースを出せば保持しているコインの枚数が１枚減るはずなので上記のVMGを拡張し、

VMG(n) = coin -> VMG(n+1)
         []
         juice -> VMG(n-1)

となりそうだが、juiceのイベントが選べるのは n>0 の場合であるはず。このような場合は次のように書けば n>0 でないと juiceイベントが起きないようにできる。

 VMG(n) = coin -> VMG(n+1)
          []
          (n>0)&juice -> VMG(n-1)

 -- つまり、n=0 のときは VMG(0) = coin -> VMG(1) と同じ。

また次のように、コインの枚数をn、ジュースの在庫をmとし、その両方を保持することもできる。juiceのイベントを起こせるのはコインを入れており(n>0) かつジュースの在庫がある(m>0) ときであり、イベント後は両方とも１つ減る。

VMG2(m,n) = coin -> VMG2(m,n+1)
            []
            (m>0)and(n>0)&juice -> VMG2(m-1,n-1)

補足

boolean gard は conditional choiceの特別な場合の省略形であり、external choice との組み合わせでなくても使ってよい。

(condition)&PROC ≡ if (condition) then PROC else STOP

つまり、上記 VMG(n)の元の記述は次のようなる。

 VMG(n) = coin -> VMG(n+1)
          []
          if (n>0) then juice -> VMG(n-1)
          else          STOP

 -- n=0 のときは
 VMG(0) = (coin -> VMG(1)) [] STOP
 -- これは、VMG(0) = coin -> VMG(1) と同じ。
 -- CSPの代数法則 P[]STOP ≡ P による。

*1:詳しくは internal choice（内部選択）の説明時に

2009-04-22

recursion(再帰)

代数演算子

何度も繰り返し販売できる自動販売機は再帰を用いて次のように記述できる。

VMR = coin -> juice -> VMR

プロセスVMRはイベント coin,juice の後、再び自身VMRに移っている。VMRはcoin,juice,coin,juice,・・・を繰り返すプロセスである。

また、VMRは次のように書いても同じプロセスとなる。*1

VMR = coin -> juice -> coin -> juice -> VMR

また、プロセスは添え字（変数）を含んで定義することもできる。
例えば、ジュース残数を n で保持したい場合は次のように書ける。

VMCNT(n) = coin -> juice -> VMCNT(n-1)
VMR = VMCNT(10)

VMRは VMCNT(n) の n の値を10としたプロセスとして定義している。イベントcoin,juice が起きる毎に VMR は VMCNT(10),VMCNT(9),VMCNT(8)・・・と変化していく。

*1:”２つのプロセスが等しい”という定義は後述する。