Communicating Sequential Processes
CSPの主な表示的モデルとして、トレースモデル、安定失敗モデル、失敗/発散モデルの3つがある。プロセス表現とこれらモデルとの意味論的マッピングがCSPの表示的意味論となる。
トレースモデルは、そのプロセスが扱う一連のイベント(トレース)でプロセス表現の意味を定義する。例えば、
t r a c e s ( S T O P ) = { ⟨ ⟩ } {\displaystyle traces\left(STOP\right)=\left\{\langle \rangle \right\}} 何故なら S T O P {\displaystyle STOP} は何のイベントも扱わないから t r a c e s ( a → b → S T O P ) = { ⟨ ⟩ , ⟨ a ⟩ , ⟨ a , b ⟩ } {\displaystyle traces\left(a\rightarrow b\rightarrow STOP\right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}} 何故ならプロセス ( a → b → S T O P ) {\displaystyle (a\rightarrow b\rightarrow STOP)} は、何のイベントも扱わない場合、イベント a {\displaystyle a} を受け付ける場合、イベント a {\displaystyle a} を受け付けた後でイベント b {\displaystyle b} を受け付ける場合の3つのケースがありうるから
プレフィックス演算子は、イベントとプロセスを結合して新たなプロセスを生成する。たとえば、
a → P {\displaystyle a\rightarrow P}
は、 a {\displaystyle {\mathit {a}}} にその環境と通信させようとするプロセスであり、 a {\displaystyle {\mathit {a}}} の後では、プロセス P {\displaystyle {\mathit {P}}} として振舞う。
イベントとは、通信あるいは相互作用を意味する。不可分で瞬間的なものと見なされる。不可分名(たとえば、 o n {\displaystyle {\mathit {on}}} 、 o f f {\displaystyle {\mathit {off}}} )、複合名(たとえば、 v a l v e . o p e n {\displaystyle valve.open} 、 v a l v e . c l o s e {\displaystyle valve.close} )、入出力イベント(たとえば、 m o u s e ? x y {\displaystyle mouse?xy} 、 s c r e e n ! b i t m a p {\displaystyle screen!bitmap} )などがある。