summaryrefslogtreecommitdiff
path: root/Assignment1/syntax.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment1/syntax.tex')
-rw-r--r--Assignment1/syntax.tex27
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}