diff --git a/report.tex b/report.tex index 162afee..8e80570 100644 --- a/report.tex +++ b/report.tex @@ -456,31 +456,14 @@ execution, and one can synchronize processes on channels. \begin{figure}[h] \begin{align*} - \seman{\proc} = \seman{\chan} &\eqdef \begin{tikzpicture}[baseline] - \node (1) at (0,0.5) [draw=red,ellipse] {call}; - \node (2) at (0,-0.5) [draw=green,ellipse] {done}; - \draw [->] (1) -- (2); - \end{tikzpicture} - & - \seman{0} &\eqdef \begin{tikzpicture}[baseline] - \node (1) at (0,0.2) [draw=red,ellipse] {call}; - \end{tikzpicture} - & - \seman{1} &\eqdef \begin{tikzpicture}[baseline] - \node (1) at (0,0.5) [draw=red,ellipse] {call}; - \node (2) at (0,-0.5) [draw=green,ellipse] {done}; - \draw [->] (1) -- (2); - \end{tikzpicture} - & - \end{align*}\vspace{-1.5em}\begin{align*} \seman{P \parallel Q} &\eqdef \left( \begin{tikzpicture}[baseline, scale=0.8] - \node (4) at (0,0.5) [draw=green,ellipse] {callP}; - \node (5) at (0,-0.5) [draw=red,ellipse] {doneP}; - \node (2) at (2.5,0.5) [draw=green,ellipse] {callQ}; - \node (3) at (2.5,-0.5) [draw=red,ellipse] {doneQ}; - \node (0) at (5,0.5) [draw=red,ellipse] {call}; - \node (1) at (5,-0.5) [draw=green,ellipse] {done}; + \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 (0) at (5,0.65) [draw=red,ellipse] {call}; + \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] (0) edge (1) edge [bend right] (2) @@ -490,7 +473,56 @@ execution, and one can synchronize processes on channels. (3) edge [bend right] (1) (5) edge [bend right] (1); \end{tikzpicture} - \right) \strComp \left(\seman{P} \parallel \seman{Q}\right) + \right) \strComp \left(\seman{P} \parallel \seman{Q}\right) & + \seman{\proc} = \seman{\chan} &\eqdef \begin{tikzpicture}[baseline] + \node (1) at (0,0.5) [draw=red,ellipse] {call}; + \node (2) at (0,-0.5) [draw=green,ellipse] {done}; + \draw [->] (1) -- (2); + \end{tikzpicture} + \\ %%%%%%%%%%%%%%%%%%%%%%%%% + \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 (0) at (5,0.65) [draw=red,ellipse] {call}; + \node (1) at (5,-0.65) [draw=green,ellipse] {done}; + \path[->] + (0) edge (1) + edge [bend right] (4) + (2) edge (3) + (4) edge (5) + (3) edge [bend right] (1) + (5) edge (2); + \end{tikzpicture} + \right) \strComp \left(\seman{P} \parallel \seman{Q}\right) & + \seman{1} &\eqdef \begin{tikzpicture}[baseline] + \node (1) at (0,0.5) [draw=red,ellipse] {call}; + \node (2) at (0,-0.5) [draw=green,ellipse] {done}; + \draw [->] (1) -- (2); + \end{tikzpicture} + \\ %%%%%%%%%%%%%%%%%%%%%%%%% + \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 (0) at (5,0.65) [draw=red,ellipse] {call}; + \node (1) at (5,-0.65) [draw=green,ellipse] {done}; + \path[->] + (0) edge (1) + edge [bend right] (2) + (2) edge (3) + (4) edge (5) + (3) edge (4) + (5) edge [bend right] (1); + \end{tikzpicture} + \right) \strComp \left(\seman{P} \parallel \seman{a}\right) & + \seman{0} &\eqdef \begin{tikzpicture}[baseline] + \node (1) at (0,0.2) [draw=red,ellipse] {call}; + \end{tikzpicture} \end{align*} \caption{CCS interpretation as strategies}\label{fig:lccs:interp} \end{figure}