Changeset 3360
 Timestamp:
 Jun 14, 2013, 6:01:56 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec2.tex
r3359 r3360 1490 1490 \matrix [diag] (m) {% 1491 1491 \node (s1) {s_1}; & \node (t1) {s_1'};\\ 1492 \node (s2) {s_2}; & \node (mid) {s_a}; & \node(t2) {s_2'}; \\1492 \node (s2) {s_2}; & \node [newn](mid) {s_a}; & \node [newn] (t2) {s_2'}; \\ 1493 1493 }; 1494 1494 {[stealth] … … 1518 1518 &\node (t1) {s_1'}; \\ 1519 1519 \node (s1) {s_1}; \\ 1520 && \node (l1) {s_b}; & \node (l2) {s_c}; & \node(t2) {s_2'};\\1521 \node (s2) {s_2}; & \node(c) {s_a};\\1520 && \node [newn] (l1) {s_b}; & \node [newn] (l2) {s_c}; & \node [newn] (t2) {s_2'};\\ 1521 \node [newn] (s2) {s_2}; & \node [newn] (c) {s_a};\\ 1522 1522 }; 1523 1523 {[stealth] … … 1530 1530 \draw (s1) to [bend right] node [rel] {$\S$} (s2); 1531 1531 \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); 1532 \draw [new] (s1) to [bend right] node [rel] {$\C$} (c);1532 \draw [new] (s1) to [bend left] node [rel] {$\C$} (c); 1533 1533 \end{tikzpicture} 1534 1534 \qquad\qquad … … 1537 1537 \node (s1) {s_1}; \\ 1538 1538 &\node (t1) {s_1'}; \\ 1539 \node (s2) {s_2}; & \node (c) {s_a};\\1540 && \node (r) {s_b}; & \node(t2) {s_2'}; \\1539 \node (s2) {s_2}; & \node [newn] (c) {s_a};\\ 1540 && \node [newn] (r) {s_b}; & \node [newn] (t2) {s_2'}; \\ 1541 1541 }; 1542 1542 {[stealth] … … 2267 2267 The equivalent of $T$ on fragments can be easily defined by mutual recursion 2268 2268 on the three types of traces defined in \autoref{fig:traces}. 2269 2270 \paragraph{The forward simulation result.} 2271 \begin{figure} 2272 \centering 2273 \tikzset{diag/.append style= 2274 {every node/.append style={is other, 2275 text height=0,text depth=0,text width=0, 2276 text opacity=0} 2277 }, 2278 } 2279 \begin{tabular}{@{}c@{}c@{}c@{}} 2280 % \begin{subfigure}{.475\linewidth} 2281 % \centering 2282 % \begin{tikzpicture}[every join/.style={ar}, join all, thick, 2283 % every label/.style=overlay, node distance=10mm] 2284 % \matrix [diag] (m) {% 2285 % \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ 2286 % \node (s2) {}; & \node (t2) {}; \\ 2287 % }; 2288 % \node [above=0 of t1, overlay] {$\alpha$}; 2289 % {[stealth] 2290 % \draw (s1)  (t1); 2291 % \draw [new] (s2)  node [above] {$*$} (t2); 2292 % } 2293 % \draw (s1) to node [rel] {$\S$} (s2); 2294 % \draw [new] (t1) to node [rel] {$\S,\L$} (t2); 2295 % \end{tikzpicture} 2296 % \caption{The \verb+cl_jump+ case.} 2297 % \label{subfig:cl_jump} 2298 % \end{subfigure} 2299 % & 2300 \begin{subfigure}{.25\linewidth} 2301 \centering 2302 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 2303 every label/.style=overlay, node distance=10mm] 2304 \matrix [diag] (m) {% 2305 \node (s1) {}; & \node (t1) {};\\ 2306 \node (s2) {}; & \node [newn] (t2) {}; \\ 2307 }; 2308 {[stealth] 2309 \draw (s1)  (t1); 2310 \draw [new] (s2)  node [above] {$*$} (t2); 2311 } 2312 \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); 2313 \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); 2314 \end{tikzpicture} 2315 \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} 2316 \label{subfig:cl_other_jump} 2317 \end{subfigure} 2318 & 2319 \begin{subfigure}{.375\linewidth} 2320 \centering 2321 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 2322 every label/.style=overlay, node distance=10mm] 2323 \matrix [diag, small gap] (m) {% 2324 &\node (t1) {}; \\ 2325 \node (s1) {}; \\ 2326 && \node [newn] (l) {}; & \node [newn] (t2) {};\\ 2327 \node (s2) {}; & \node [newn] (c) {};\\ 2328 }; 2329 {[stealth] 2330 \draw (s1)  node [above left] {$f$} (t1); 2331 \draw [new] (s2)  node [above] {$*$} (c); 2332 \draw [new] (c)  node [below right] {$f$} (l); 2333 \draw [new] (l)  node [above] {$*$} (t2); 2334 } 2335 \draw (s1) to [bend right] node [rel] {$\S$} (s2); 2336 \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); 2337 \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); 2338 \draw [new] (s1) to [bend left] node [rel] {$\C$} (c); 2339 \end{tikzpicture} 2340 \caption{The \verb+cl_call+ case.} 2341 \label{subfig:cl_call} 2342 \end{subfigure} 2343 & 2344 \begin{subfigure}{.375\linewidth} 2345 \centering 2346 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 2347 every label/.style=overlay, node distance=10mm] 2348 \matrix [diag, small gap] (m) {% 2349 \node (s1) {}; \\ 2350 &\node (t1) {}; \\ 2351 \node (s2) {}; & \node [newn] (c) {};\\ 2352 && \node [newn] (r) {}; & \node [newn] (t2) {}; \\ 2353 }; 2354 {[stealth] 2355 \draw (s1)  (t1); 2356 \draw [new] (s2)  node [above] {$*$} (c); 2357 \draw [new] (c)  (r); 2358 \draw [new] (r)  node [above] {$*$} (t2); 2359 } 2360 \draw (s1) to [bend right] node [rel] {$\S$} (s2); 2361 \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); 2362 \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); 2363 \end{tikzpicture} 2364 \caption{The \verb+cl_return+ case.} 2365 \label{subfig:cl_return} 2366 \end{subfigure} 2367 \end{tabular} 2368 \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces. 2369 Dashed lines 2370 and arrows indicates how the diagrams must be closed when solid relations 2371 are present. 2372 DA CAMBIARE: $\L$ va in conflitto con l'altra definizione} 2373 \label{fig:forwardsim} 2374 \end{figure} 2375 2269 2376 % There are three mutual structural recursive functions, one for each of 2270 2377 % \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
Note: See TracChangeset
for help on using the changeset viewer.