diff options
| author | Camil Staps | 2018-04-18 20:40:46 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-04-18 20:40:46 +0200 |
| commit | 341ac08515644afb57aa30073a75bace2ec41a7b (patch) | |
| tree | 35eb9aa80765c4e102866a62225e7772b9f51ce6 /Assignment1 | |
| parent | Check syntactic elimination rules (diff) | |
(for me) more intuitive intuitive semantics
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/syntax.tex | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 708d3b8..3f3430c 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -105,8 +105,8 @@ we include an arrow that points to the state for which the formula holds. \node[arbitrary] (1) [right of=0] {}; \node[state,label=$b$] (2) [right of=1] {}; \node[state,label=$a$] (3) [right of=2] {}; - \node[state,label=$a$,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (4) [right of=3] {\dots}; + \node[state,label=$a$,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ @@ -115,9 +115,9 @@ we include an arrow that points to the state for which the formula holds. \node (0) {\dots}; \node[arbitrary] (1) [right of=0] {}; \node[arbitrary] (2) [right of=1] {}; - \node[state,label=$a$] (3) [right of=2] {}; - \node[arbitrary,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node[arbitrary] (3) [right of=2] {}; + \node[state,label=$a$] (4) [right of=3] {}; + \node[arbitrary,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ @@ -127,24 +127,27 @@ we include an arrow that points to the state for which the formula holds. \node[arbitrary] (1) [right of=0] {}; \node[state,label=$a$] (2) [right of=1] {}; \node[arbitrary] (3) [right of=2] {}; - \node[arbitrary,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (4) [right of=3] {\dots}; + \node[arbitrary,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ \text{was always} & \Gop^{-1} a & \begin{tikzpicture}[intuitive semantics] - \node (0) {\dots}; + \node[state,label=$a$] (0) {}; \node[state,label=$a$] (1) [right of=0] {}; \node[state,label=$a$] (2) [right of=1] {}; - \node[state,label=$a$] (3) [right of=2] {}; - \node[state,label=$a$,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (3) [right of=2] {\dots}; + \node[state,label=$a$] (4) [right of=3] {}; + \node[state,label=$a$,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture} \end{array}\] - \caption{Intuitive semantics of past modalities.} + \caption{% + Intuitive semantics of past modalities. + The current state is indicated with an arrow below. + All states following the current state are arbitrary.} \label{fig:PLTL_intuitive} \end{figure} |