tobast/L3-internship-report
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Done lCCS interpretation

Browse source
This commit is contained in:
Théophile Bastian 2016-07-21 12:42:17 +01:00
parent 090c60b4f1
commit 9266131494
1 changed files with 34 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
report.tex
View file

@ -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}