diff --git a/report.tex b/report.tex index 8e80570..ce51b5a 100644 --- a/report.tex +++ b/report.tex @@ -458,10 +458,10 @@ execution, and one can synchronize processes on channels. \begin{align*} \seman{P \parallel Q} &\eqdef \left( \begin{tikzpicture}[baseline, scale=0.8] - \node (4) at (0,0.65) [draw=green,ellipse] {callP}; - \node (5) at (0,-0.65) [draw=red,ellipse] {doneP}; - \node (2) at (2.5,0.65) [draw=green,ellipse] {callQ}; - \node (3) at (2.5,-0.65) [draw=red,ellipse] {doneQ}; + \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; + \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; + \node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$}; + \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] @@ -482,10 +482,10 @@ execution, and one can synchronize processes on channels. \\ %%%%%%%%%%%%%%%%%%%%%%%%% \seman{P \cdot Q} &\eqdef \left( \begin{tikzpicture}[baseline,scale=0.8] - \node (4) at (0,0.65) [draw=green,ellipse] {callP}; - \node (5) at (0,-0.65) [draw=red,ellipse] {doneP}; - \node (2) at (2.5,0.65) [draw=green,ellipse] {callQ}; - \node (3) at (2.5,-0.65) [draw=red,ellipse] {doneQ}; + \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; + \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; + \node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$}; + \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] @@ -505,10 +505,10 @@ execution, and one can synchronize processes on channels. \\ %%%%%%%%%%%%%%%%%%%%%%%%% \seman{(a : \chan) \cdot P} &\eqdef \left( \begin{tikzpicture}[baseline,scale=0.8] - \node (4) at (0,0.65) [draw=green,ellipse] {callP}; - \node (5) at (0,-0.65) [draw=red,ellipse] {doneP}; - \node (2) at (2.5,0.65) [draw=green,ellipse] {call\_a}; - \node (3) at (2.5,-0.65) [draw=red,ellipse] {done\_a}; + \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; + \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; + \node (2) at (2.5,0.65) [draw=green,ellipse] {call $a$}; + \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $a$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] @@ -523,6 +523,28 @@ execution, and one can synchronize processes on channels. \seman{0} &\eqdef \begin{tikzpicture}[baseline] \node (1) at (0,0.2) [draw=red,ellipse] {call}; \end{tikzpicture} + \\ %%%%%%%%%%%%%%%%%%%%%%%%% + \seman{(\nu a) P} &\eqdef \left( + \begin{tikzpicture}[baseline,scale=0.8] + \node (6) at (0,0.65) [draw=green,ellipse] {call $a$}; + \node (7) at (0,-0.65) [draw=red,ellipse] {done $a$}; + \node (4) at (2.5,0.65) [draw=green,ellipse] {call $\bar{a}$}; + \node (5) at (2.5,-0.65) [draw=red,ellipse] {done $\bar{a}$}; + \node (2) at (5,0.65) [draw=green,ellipse] {call $P$}; + \node (3) at (5,-0.65) [draw=red,ellipse] {done $P$}; + \node (0) at (7.5,0.65) [draw=red,ellipse] {call}; + \node (1) at (7.5,-0.65) [draw=green,ellipse] {done}; + \path[->] + (0) edge (1) + edge [bend right] (2) + (2) edge (3) + (3) edge [bend right] (1) + (4) edge (5) + edge (7) + (6) edge (7) + edge (5); + \end{tikzpicture} + \right) \strComp \seman{P} & \end{align*} \caption{CCS interpretation as strategies}\label{fig:lccs:interp} \end{figure}