Input/Output(入出力)
CSPではプロセス間の様々なデータの受け渡しをチャネルを用いたメッセージパッシング方式で行う。
channel ch:{0..7} -- チャネルchの型を{0,1,・・,6,7}とする。 P = ch!5 -> SKIP -- '!'は送信を意味する。 Q = ch?x -> SKIP -- '?'は受信を意味する。 SYSTEM = P[|{|ch|}|]Q -- {|ch|} = {ch.0,ch.1,・・ch.6,ch.7}
プロセスPはチャンネルchに５を出力するだけのプロセスである。また、このプロセスの起こすイベントはch.5である。
プロセスQはチャンネルchから値を変数x*1で受け取るだけのプロセスである。
SYSTEMはPとQがチャンネルchで同期する*2プロセスでありイベントch.5を起こした後、正常終了する。
これまで自販機の例では入金をイベントcoinで抽象化してきたが、もう少し詳しくチャネルinを通して小銭を入れることにすると
channel juice Coin = {10,50,100,500} --小銭は10円以上の４種類 channel in:Coin VM(n) = if n<120 then in?x -> VM(n+x) --入金 x を保持している金額に加算 else juice -> VM(n-120) --ジュース1本120円
自販機はチャネルinで受け取った値xを変数nに加算する。120円以上入金されるとジュースを出す。
PERSON = juice -> SKIP [] |~|i:Coin@ in!i -> PERSON {- 次のように書いても同じ。 PERSON = juice -> SKIP [] ( in!10 -> PERSON |~| in!50 -> PERSON |~| in!100 -> PERSON |~| in!500 -> PERSON ) -} SYSTEM = PERSON[|{|in,juice|}|]VM(0)
プロセスPERSONはjuiceボタンを押すか、小銭を適当に入れる。
PERSONとVMはチャネルin およびイベントjuice で同期しながら動作するので、結果的に120円以上になるまで小銭が入れられた後ジュースが出て終了する。なお、釣銭は出ないので注意。
