アルファベット プロセスのアルファベットを定義しておく。プロセスP のアルファベットαP とは P の持つべきイベントの集合である。例えば、 channel coin, coke, lemonade,drink VMS = coin -> ( coke -> VMS [] lemonade -> VMS ) aVMS = {coin, coke, lem…

internal choice '|~|'はプロセスの内部選択を表す。外部選択との違いを購入者の例を使って説明する。購入者はコインを入れ、コーラかレモネードを購入した後にそれを飲む。コーラとレモネードの選択は購入者自身の好みや気分によって決定されるとする。 cha…