diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 16:27:27 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 16:28:04 +0000 |
commit | 11b2a38aec9323ad4bc69ff7505e7f24f6833b39 (patch) | |
tree | bdd77b1aa2b3556821d955a70e1bd260b279701f /proof.tex | |
parent | cacf357e849c0cc3f18b714d9fadbb161912639f (diff) | |
download | oopsla21_fvhls-11b2a38aec9323ad4bc69ff7505e7f24f6833b39.tar.gz oopsla21_fvhls-11b2a38aec9323ad4bc69ff7505e7f24f6833b39.zip |
Continue on simulation diagram
Diffstat (limited to 'proof.tex')
-rw-r--r-- | proof.tex | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -68,13 +68,13 @@ Using the \texttt{match\_states}, we can then define the correctness theorem for \begin{tikzpicture} \begin{scope} \node[circle] (s1) at (0,1.5) {$R, M, \textit{pc}$}; - \node[circle] (r1) at (6,1.5) {$\Gamma_{r}, \Gamma_{a}, \Gamma_{r}!\sigma$}; + \node[circle] (r1) at (6.5,1.5) {$\Gamma_{r}, \Gamma_{a}$}; \node[circle] (s2) at (0,0) {$R', M', \textit{pc}'$}; - \node[circle] (r2) at (6,0) {$\Gamma_{r}', \Gamma_{a}', \Gamma_{r}'!\sigma$}; - \node at (6.3,0.75) {+}; + \node[circle] (r2) at (6.5,0) {$\Gamma_{r}', \Gamma_{a}'$}; + \node at (6.8,0.75) {+}; \draw (s1) -- node[above] {$R \le \Gamma_{r} \land M \le \Gamma_{a} \land \textit{pc} = \Gamma_{r}!\sigma$} ++ (r1); - \draw[-{Latex}] ($(s1.south) + (0,0.3)$) -- ($(s2.north) - (0,0.3)$); - \draw[-{Latex},dashed] ($(r1.south) + (0,0.4)$) -- ($(r2.north) - (0,0.4)$); + \draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$); + \draw[-{Latex},dashed] ($(r1.south) + (0,0.2)$) -- ($(r2.north) - (0,0.2)$); \draw[dashed] (s2) -- node[above] {$R' \le \Gamma_{r}' \land M' \le \Gamma_{a}' \land \textit{pc}' = \Gamma_{r}'!\sigma$} ++ (r2); \end{scope} \end{tikzpicture} |