Changeset 3360


Ignore:
Timestamp:
Jun 14, 2013, 6:01:56 PM (4 years ago)
Author:
tranquil
Message:

aggiustate le figure

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec2.tex

    r3359 r3360  
    14901490    \matrix [diag] (m) {%
    14911491         \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'}; \\
    14931493    };
    14941494    {[-stealth]
     
    15181518         &\node (t1) {s_1'}; \\
    15191519         \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};\\   
    15221522    };
    15231523    {[-stealth]
     
    15301530    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
    15311531    \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);
    15331533\end{tikzpicture}
    15341534\qquad\qquad
     
    15371537        \node (s1) {s_1}; \\
    15381538        &\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'}; \\   
    15411541    };
    15421542    {[-stealth]
     
    22672267The equivalent of $|T|$ on fragments can be easily defined by mutual recursion
    22682268on 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
    22692376% There are three mutual structural recursive functions, one for each of
    22702377% \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
Note: See TracChangeset for help on using the changeset viewer.