From 2e0274e4d501fde70714525f86291d6aa7c0d4ec Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 27 May 2024 21:44:40 +0200 Subject: [PATCH] release symbenc --- compile | 2 +- symbolic_encoding/0001.tex | 6 + symbolic_encoding/0001_sol.tex | 29 ++++ symbolic_encoding/0002.tex | 38 ++++++ symbolic_encoding/0002_sol.tex | 44 ++++++ symbolic_encoding/0003.tex | 1 + symbolic_encoding/0003_sol.tex | 6 + symbolic_encoding/0004.tex | 2 + symbolic_encoding/0004_sol.tex | 6 + symbolic_encoding/0005.tex | 24 ++++ symbolic_encoding/0005_sol.tex | 13 ++ symbolic_encoding/0006.tex | 24 ++++ symbolic_encoding/0006_sol.tex | 15 ++ symbolic_encoding/0007.tex | 39 ++++++ symbolic_encoding/0007_sol.tex | 7 + symbolic_encoding/0008.tex | 9 ++ symbolic_encoding/0008_sol.tex | 4 + symbolic_encoding/1000.tex | 17 +++ symbolic_encoding/1001.tex | 8 ++ symbolic_encoding/1002.tex | 1 + symbolic_encoding/1003.tex | 2 + symbolic_encoding/1004.tex | 25 ++++ symbolic_encoding/1005.tex | 25 ++++ symbolic_encoding/1006.tex | 25 ++++ symbolic_encoding/1007.tex | 7 + symbolic_encoding/1008.tex | 7 + symbolic_encoding/1009.tex | 3 + symbolic_encoding/1010.tex | 17 +++ symbolic_encoding/1011.tex | 1 + symbolic_encoding/1012.tex | 15 ++ symbolic_encoding/1013.tex | 36 +++++ symbolic_encoding/1014.tex | 41 ++++++ symbolic_encoding/1015.tex | 14 ++ symbolic_encoding/1016.tex | 15 ++ symbolic_encoding/1017.tex | 15 ++ symbolic_encoding/1018.tex | 4 + symbolic_encoding/1019.tex | 5 + symbolic_encoding/1020.tex | 3 + symbolic_encoding/1021.tex | 2 + .../multiple_choice/2_1_symbrep_lect.tex | 8 ++ .../multiple_choice/2_1_symbrep_self.tex | 8 ++ .../practical_questions/1_10_kripke_self.tex | 8 ++ .../practical_questions/1_1_kripke_lect.tex | 4 + .../1_1_kripke_lect_sol.tex | 29 ++++ .../practical_questions/1_1_kripke_self.tex | 5 + .../practical_questions/1_1_symbrep.tex | 1 + .../practical_questions/1_1_symbrep_self.tex | 1 + .../practical_questions/1_2_kripke_lect.tex | 38 ++++++ .../1_2_kripke_lect_sol.tex | 44 ++++++ .../practical_questions/1_2_kripke_self.tex | 25 ++++ .../practical_questions/1_2_symbrep_self.tex | 2 + .../practical_questions/1_3_kripke_self.tex | 25 ++++ .../practical_questions/1_4_kripke_self.tex | 25 ++++ .../practical_questions/2_05_symbrep_self.tex | 32 +++++ .../practical_questions/2_10_symbrep_lect.tex | 39 ++++++ .../2_10_symbrep_lect_sol.tex | 7 + .../practical_questions/2_10_symbrep_self.tex | 1 + .../practical_questions/2_11_symbrep_lect.tex | 9 ++ .../2_11_symbrep_lect_sol.tex | 4 + .../practical_questions/2_11_symbrep_self.tex | 21 +++ .../practical_questions/2_12_symbrep_lect.tex | 7 + .../practical_questions/2_12_symbrep_self.tex | 15 ++ .../practical_questions/2_13_symbrep_lect.tex | 24 ++++ .../2_13_symbrep_lect_sol.tex | 15 ++ .../practical_questions/2_13_symbrep_self.tex | 15 ++ .../practical_questions/2_17_symbrep_self.tex | 33 +++++ .../practical_questions/2_18_symbrep_self.tex | 7 + .../practical_questions/2_1_symbrep_lect.tex | 1 + .../2_1_symbrep_lect_sol.tex | 6 + .../practical_questions/2_1_symbrep_self.tex | 7 + .../practical_questions/2_20_symbrep_self.tex | 9 ++ .../practical_questions/2_2_symbrep_lect.tex | 2 + .../2_2_symbrep_lect_sol.tex | 6 + .../practical_questions/2_2_symbrep_self.tex | 8 ++ .../practical_questions/2_3_symbrep_lect.tex | 40 ++++++ .../practical_questions/2_3_symbrep_self.tex | 48 +++++++ .../practical_questions/2_4_symbrep_lect.tex | 15 ++ .../practical_questions/2_4_symbrep_self.tex | 17 +++ .../practical_questions/2_5_symbrep_self.tex | 36 +++++ .../practical_questions/2_6_symbrep_lect.tex | 2 + .../practical_questions/2_6_symbrep_self.tex | 41 ++++++ .../practical_questions/2_7_symbrep_lect.tex | 14 ++ .../practical_questions/2_7_symbrep_self.tex | 37 +++++ .../practical_questions/2_8_symbrep_self.tex | 1 + .../practical_questions/2_9_symbrep_lect.tex | 24 ++++ .../2_9_symbrep_lect_sol.tex | 13 ++ .../practical_questions/2_9_symbrep_self.tex | 3 + symbolic_encoding/symbolic_encoding.tex | 128 ++++++++++++++++++ .../theory_questions/0_1_symb_lect.tex | 1 + .../theory_questions/0_1_symb_self.tex | 1 + .../theory_questions/1_0_kripke_self.tex | 2 + .../theory_questions/2_01_symbrep_self.tex | 3 + .../theory_questions/2_1_symbrep_self.tex | 1 + .../theory_questions/2_2_symbrep_self.tex | 4 + .../theory_questions/2_3_symbrep_lect.tex | 1 + .../theory_questions/2_3_symbrep_self.tex | 5 + 96 files changed, 1484 insertions(+), 1 deletion(-) create mode 100644 symbolic_encoding/0001.tex create mode 100644 symbolic_encoding/0001_sol.tex create mode 100644 symbolic_encoding/0002.tex create mode 100644 symbolic_encoding/0002_sol.tex create mode 100644 symbolic_encoding/0003.tex create mode 100644 symbolic_encoding/0003_sol.tex create mode 100644 symbolic_encoding/0004.tex create mode 100644 symbolic_encoding/0004_sol.tex create mode 100644 symbolic_encoding/0005.tex create mode 100644 symbolic_encoding/0005_sol.tex create mode 100644 symbolic_encoding/0006.tex create mode 100644 symbolic_encoding/0006_sol.tex create mode 100644 symbolic_encoding/0007.tex create mode 100644 symbolic_encoding/0007_sol.tex create mode 100644 symbolic_encoding/0008.tex create mode 100644 symbolic_encoding/0008_sol.tex create mode 100644 symbolic_encoding/1000.tex create mode 100644 symbolic_encoding/1001.tex create mode 100644 symbolic_encoding/1002.tex create mode 100644 symbolic_encoding/1003.tex create mode 100644 symbolic_encoding/1004.tex create mode 100644 symbolic_encoding/1005.tex create mode 100644 symbolic_encoding/1006.tex create mode 100644 symbolic_encoding/1007.tex create mode 100644 symbolic_encoding/1008.tex create mode 100644 symbolic_encoding/1009.tex create mode 100644 symbolic_encoding/1010.tex create mode 100644 symbolic_encoding/1011.tex create mode 100644 symbolic_encoding/1012.tex create mode 100644 symbolic_encoding/1013.tex create mode 100644 symbolic_encoding/1014.tex create mode 100644 symbolic_encoding/1015.tex create mode 100644 symbolic_encoding/1016.tex create mode 100644 symbolic_encoding/1017.tex create mode 100644 symbolic_encoding/1018.tex create mode 100644 symbolic_encoding/1019.tex create mode 100644 symbolic_encoding/1020.tex create mode 100644 symbolic_encoding/1021.tex create mode 100644 symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex create mode 100644 symbolic_encoding/multiple_choice/2_1_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/1_10_kripke_self.tex create mode 100644 symbolic_encoding/practical_questions/1_1_kripke_lect.tex create mode 100644 symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/1_1_kripke_self.tex create mode 100644 symbolic_encoding/practical_questions/1_1_symbrep.tex create mode 100644 symbolic_encoding/practical_questions/1_1_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/1_2_kripke_lect.tex create mode 100644 symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/1_2_kripke_self.tex create mode 100644 symbolic_encoding/practical_questions/1_2_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/1_3_kripke_self.tex create mode 100644 symbolic_encoding/practical_questions/1_4_kripke_self.tex create mode 100644 symbolic_encoding/practical_questions/2_05_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_12_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_12_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_17_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_18_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_20_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_3_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_3_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_4_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_4_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_5_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_6_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_6_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_7_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_7_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_8_symbrep_self.tex create mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_lect.tex create mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex create mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_self.tex create mode 100644 symbolic_encoding/symbolic_encoding.tex create mode 100644 symbolic_encoding/theory_questions/0_1_symb_lect.tex create mode 100644 symbolic_encoding/theory_questions/0_1_symb_self.tex create mode 100644 symbolic_encoding/theory_questions/1_0_kripke_self.tex create mode 100644 symbolic_encoding/theory_questions/2_01_symbrep_self.tex create mode 100644 symbolic_encoding/theory_questions/2_1_symbrep_self.tex create mode 100644 symbolic_encoding/theory_questions/2_2_symbrep_self.tex create mode 100644 symbolic_encoding/theory_questions/2_3_symbrep_lect.tex create mode 100644 symbolic_encoding/theory_questions/2_3_symbrep_self.tex diff --git a/compile b/compile index 68eae9f..793bf57 100755 --- a/compile +++ b/compile @@ -102,7 +102,7 @@ compile_wrapper() { compile_chapter() { #for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal - for chapter in smt + for chapter in symbenc do set_chapter "\\chapter${chapter}true" compile_wrapper "$chapter" "$@" diff --git a/symbolic_encoding/0001.tex b/symbolic_encoding/0001.tex new file mode 100644 index 0000000..b6db9ee --- /dev/null +++ b/symbolic_encoding/0001.tex @@ -0,0 +1,6 @@ +\item \lect Draw the graph for the \emph{transition system} $\mathcal{T}$ with: +\begin{itemize}[itemsep=-0.9em, leftmargin=0.8em] +\item $S = \{s_1, s_2, s_3, s_4\}, $\\ +\item $S_0 = \{s_2\}, $\\ +\item $R = \{\{s_1, s_2\}, \{s_1, s_1\}, \{s_2, s_4\}, \{s_2, s_3\}, \{s_3, s_1\}, \{s_4, s_2\}, \{s_4, s_3\}\}, $ +\end{itemize} diff --git a/symbolic_encoding/0001_sol.tex b/symbolic_encoding/0001_sol.tex new file mode 100644 index 0000000..11f08e8 --- /dev/null +++ b/symbolic_encoding/0001_sol.tex @@ -0,0 +1,29 @@ +\begin{center} +\begin{tikzpicture}[scale=0.2] +\tikzstyle{every node}+=[inner sep=0pt] +\draw [black] (11,-26.9) circle (3); +\draw (11,-26.9) node {$s_2$}; +\draw [black] (23.6,-15) circle (3); +\draw (23.6,-15) node {$s_1$}; +\draw [black] (23.6,-38) circle (3); +\draw (23.6,-38) node {$s_4$}; +\draw [black] (36.7,-26.9) circle (3); +\draw (36.7,-26.9) node {$s_3$}; +\draw [black] (21.42,-17.06) -- (13.18,-24.84); +\fill [black] (13.18,-24.84) -- (14.11,-24.65) -- (13.42,-23.93); +\draw [black] (3.7,-26.9) -- (8,-26.9); +\fill [black] (8,-26.9) -- (7.2,-26.4) -- (7.2,-27.4); +\draw [black] (25.89,-36.06) -- (34.41,-28.84); +\fill [black] (34.41,-28.84) -- (33.48,-28.98) -- (34.12,-29.74); +\draw [black] (34.48,-24.88) -- (25.82,-17.02); +\fill [black] (25.82,-17.02) -- (26.08,-17.93) -- (26.75,-17.18); +\draw [black] (14,-26.9) -- (33.7,-26.9); +\fill [black] (33.7,-26.9) -- (32.9,-26.4) -- (32.9,-27.4); +\draw [black] (21.35,-36.02) -- (13.25,-28.88); +\fill [black] (13.25,-28.88) -- (13.52,-29.79) -- (14.18,-29.04); +\draw [black] (13.25,-28.88) -- (21.35,-36.02); +\fill [black] (21.35,-36.02) -- (21.08,-35.11) -- (20.42,-35.86); +\draw [black] (25.456,-12.658) arc (169.34618:-118.65382:2.25); +\fill [black] (26.59,-15.05) -- (27.28,-15.69) -- (27.47,-14.7); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/0002.tex b/symbolic_encoding/0002.tex new file mode 100644 index 0000000..1d33b8b --- /dev/null +++ b/symbolic_encoding/0002.tex @@ -0,0 +1,38 @@ + +\item \lect +Consider the example of an elevator. +Initially, the elevator is in the ground floor. +From the ground floor, it can either go basement, stay there for a while, +and then go back to the ground floor, or it can go from the ground floor +to the second floor, stay there for a while, and go back to the ground floor. +While traveling between ground floor to second floor, the elevator passes the first floor, but it cannot stop there. + +Model this elevator as \emph{transition system}. + + + + +\iffalse +\item \lect + Given the following graph representation of a \textit{transition system}, state the contents of the sets $S, S_0 and R$ + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=20pt}] + \node[node] (s0) {$s0$}; + \node (s0s2) [below= 1cm of s0] {}; + \node[node] (s1) [right of=s0s2] {$s1$}; + \node[node] (s2) [below of=s0] {$s2$}; + \node (start1) [left=1cm of s0] {}; + + \path[->] (start1) edge (s0); + \path[->] (s1) edge (s0); + \path[->] (s0) edge [bend left] (s2); + \path[->] (s2) edge (s1); + \path[->] (s2) edge [bend left] (s0); + \path[->] (s0.30) edge[bend right=90, looseness=15, out=240, in=300] (s0.60); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); +\end{tikzpicture} +\end{center} +\fi \ No newline at end of file diff --git a/symbolic_encoding/0002_sol.tex b/symbolic_encoding/0002_sol.tex new file mode 100644 index 0000000..87eeeb8 --- /dev/null +++ b/symbolic_encoding/0002_sol.tex @@ -0,0 +1,44 @@ +We use the following states: +%ground floor, basement,second floor, passing ground floor +\begin{itemize} +\item $s_g$ indicates that the elevator is on the ground floor. +\item $s_b$ indicates that the elevator is in the basement. +\item $s_s$ indicates that the elevator is on the second floor. +\item $s_f$ indicates that the elevator is passing the first floor. +\end{itemize} +The transition system is then given by: $\mathcal{T}$ = ($S$, $S_0$, $R$) with $S$ = $\{s_g, s_b, s_s, s_f\}$, $S_0$ = $\{s_g\}$, $R$ = $\{(s_g, s_g), (s_g, s_b), (s_b, s_b), (s_b, s_g), (s_g, s_f), (s_f, s_s), (s_s, s_s), (s_s, s_f), (s_f, s_g)\}$\\ + + +\begin{center} +\begin{tikzpicture}[scale=0.2] +\tikzstyle{every node}+=[inner sep=0pt] +\draw [black] (13.9,-26) circle (3); +\draw (13.9,-26) node {$s_g$}; +\draw [black] (27.8,-35.6) circle (3); +\draw (27.8,-35.6) node {$s_b$}; +\draw [black] (27.8,-26) circle (3); +\draw (27.8,-26) node {$s_f$}; +\draw [black] (27.8,-15.8) circle (3); +\draw (27.8,-15.8) node {$s_s$}; +\draw [black] (4.8,-26) -- (10.9,-26); +\fill [black] (10.9,-26) -- (10.1,-25.5) -- (10.1,-26.5); +\draw [black] (11.501,-24.218) arc (261.13116:-26.86884:2.25); +\fill [black] (13.85,-23.01) -- (14.47,-22.3) -- (13.48,-22.14); +\draw [black] (16.37,-27.7) -- (25.33,-33.9); +\fill [black] (25.33,-33.9) -- (24.96,-33.03) -- (24.39,-33.85); +\draw [black] (26.957,-38.467) arc (11.34364:-276.65636:2.25); +\fill [black] (25.01,-36.67) -- (24.13,-36.34) -- (24.33,-37.32); +\draw [black] (25.33,-33.9) -- (16.37,-27.7); +\fill [black] (16.37,-27.7) -- (16.74,-28.57) -- (17.31,-27.75); +\draw [black] (16.9,-26) -- (24.8,-26); +\fill [black] (24.8,-26) -- (24,-25.5) -- (24,-26.5); +\draw [black] (27.8,-23) -- (27.8,-18.8); +\fill [black] (27.8,-18.8) -- (27.3,-19.6) -- (28.3,-19.6); +\draw [black] (28.483,-12.891) arc (194.52895:-93.47105:2.25); +\fill [black] (30.52,-14.57) -- (31.42,-14.86) -- (31.17,-13.89); +\draw [black] (27.8,-18.8) -- (27.8,-23); +\fill [black] (27.8,-23) -- (28.3,-22.2) -- (27.3,-22.2); +\draw [black] (24.8,-26) -- (16.9,-26); +\fill [black] (16.9,-26) -- (17.7,-26.5) -- (17.7,-25.5); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/0003.tex b/symbolic_encoding/0003.tex new file mode 100644 index 0000000..7d625ca --- /dev/null +++ b/symbolic_encoding/0003.tex @@ -0,0 +1 @@ +\item \lect Given a state space of size $|S| = 2^4 = 16$, give the symbolic encoding for the following states: (a) $s_{7}$, (b) $s_{15}$, and (c) $s_{10}$. \ No newline at end of file diff --git a/symbolic_encoding/0003_sol.tex b/symbolic_encoding/0003_sol.tex new file mode 100644 index 0000000..e574485 --- /dev/null +++ b/symbolic_encoding/0003_sol.tex @@ -0,0 +1,6 @@ +For the symbolic encoding we need 4 Boolean variables, \{$v_3$, . . . , $v_0$\}. +Let $v_3$ be the most significant bit, and $v_0$ the least significant bit.\\ + +(a) $s_{7}$ = $\lnot v_3 \land v_2 \land v_1 \land v_0$\\ +(b) $s_{15}$ = $v_3 \land v_2 \land v_1 \land v_0$\\ +(c) $s_{10}$ = $v_3 \land \lnot v_2 \land v_1 \land \lnot v_0$ \ No newline at end of file diff --git a/symbolic_encoding/0004.tex b/symbolic_encoding/0004.tex new file mode 100644 index 0000000..549492f --- /dev/null +++ b/symbolic_encoding/0004.tex @@ -0,0 +1,2 @@ +\item \lect Given is the set of states $S=\{s_0,\dots,s_7\}$. +Find formulas in propositional logic that symbolically represent the sets $A = \{s_7, s_6,s_3, s_2 \}$, $B=\{s_1, s_3,s_5, s_7\}$, and $C=\{s_7, s_6,s_0, s_1\}$. diff --git a/symbolic_encoding/0004_sol.tex b/symbolic_encoding/0004_sol.tex new file mode 100644 index 0000000..02c3d2c --- /dev/null +++ b/symbolic_encoding/0004_sol.tex @@ -0,0 +1,6 @@ +$A = \{s_7, s_6,s_3, s_2 \}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land \lnot v_0)$\\ +\hspace*{0,34cm} = $v_1$\\\\ +$B=\{s_1, s_3,s_5, s_7\}$ = $(\lnot v_2 \land \lnot v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (v_2 \land \lnot v_1 \land v_0) \lor (v_2 \land v_1 \land v_0)$\\ +\hspace*{0,34cm} = $v_0$\\\\ +$C=\{s_7, s_6,s_0, s_1\}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land v_0)$ \\ +\hspace*{0,34cm} = $(v_2 \land v_1) \lor (\lnot v_2 \land \lnot v_1)$ \ No newline at end of file diff --git a/symbolic_encoding/0005.tex b/symbolic_encoding/0005.tex new file mode 100644 index 0000000..255e6f3 --- /dev/null +++ b/symbolic_encoding/0005.tex @@ -0,0 +1,24 @@ +\item \lect Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v_1 \land \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + %\path[<->] (s0) edge (s1); + \path[->] (s0) edge (s2); + \path[<-] (s0) edge (s3); + %\path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + \path[<-] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + %\path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + % \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/0005_sol.tex b/symbolic_encoding/0005_sol.tex new file mode 100644 index 0000000..d8af7cc --- /dev/null +++ b/symbolic_encoding/0005_sol.tex @@ -0,0 +1,13 @@ +Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ +\begin{center} + $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ + $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0)$\\ +\end{center} + +We can further simplify the formula to: +\begin{center} + $\lnot v_1 \land \lnot v_0 \land \lnot v'_0 \ \lor$\\ + $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_0)$\\ +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/0006.tex b/symbolic_encoding/0006.tex new file mode 100644 index 0000000..25fc139 --- /dev/null +++ b/symbolic_encoding/0006.tex @@ -0,0 +1,24 @@ +\item \lect Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v_1 \land \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[->] (s0) edge (s1); + \path[<->] (s0) edge (s2); + \path[<->] (s0) edge (s3); + \path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + \path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/0006_sol.tex b/symbolic_encoding/0006_sol.tex new file mode 100644 index 0000000..bd9c552 --- /dev/null +++ b/symbolic_encoding/0006_sol.tex @@ -0,0 +1,15 @@ +Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ +\begin{center} + $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $\lnot v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0)$ +\end{center} + +We can further simplify the formula to: +\begin{center} + $\lnot v_1 \land \lnot v_0 \lor$\\ + $\lnot v_1 \land v_0 \land (v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ + $v_1 \land \lnot v_0 \land (\lnot v'_1 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land v_0$ +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/0007.tex b/symbolic_encoding/0007.tex new file mode 100644 index 0000000..a9ea243 --- /dev/null +++ b/symbolic_encoding/0007.tex @@ -0,0 +1,39 @@ + +\item \lect +Consider the domain $A=\{Spain, France, Italy, Germany\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter symbolic representation for the set + $B=\{France, Germany\}$? Illustrate your answer by giving the + representing formulas for $B$ in both encodings. + +\vspace{.5cm} + +% \begin{minipage} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $0$ & $1$ \\ + Germany & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $1$ & $1$ \\ + Germany & $0$ & $1$ + \end{tabular} +%\end{minipage} + + \ No newline at end of file diff --git a/symbolic_encoding/0007_sol.tex b/symbolic_encoding/0007_sol.tex new file mode 100644 index 0000000..d6b73f7 --- /dev/null +++ b/symbolic_encoding/0007_sol.tex @@ -0,0 +1,7 @@ +Using encoding 1, we end up in the following formula:\\ +$b = v_1$\\\\ +Using encoding 2, we end up in the following formula:\\ +$b = (v_1 \land \lnot v_0) \lor (\lnot v_1 \land v_0)$\\ + +Encoding 1 gives a shorter symbolic representation +for the set $B=\{France, Germany\}$. diff --git a/symbolic_encoding/0008.tex b/symbolic_encoding/0008.tex new file mode 100644 index 0000000..0f137e4 --- /dev/null +++ b/symbolic_encoding/0008.tex @@ -0,0 +1,9 @@ +\item \lect +Find a symbolic binary encoding for $X = \{ 0,1, \ldots, 31 \}$. + Use it to find formulas that symbolically represent the sets $A$ and $B$ and simplify the formulas: + \begin{itemize} + \item $A =\{ 12, 13, 14, 15, 28, 29, 30, 31 \}$ + \item $B =\{x \in X \mid 0 \leq x \leq 15\}$ + \end{itemize} + Furthermore, give the formulas representing the sets + $C=A\cap B$ and $D = A \cup B$. \ No newline at end of file diff --git a/symbolic_encoding/0008_sol.tex b/symbolic_encoding/0008_sol.tex new file mode 100644 index 0000000..db46cc5 --- /dev/null +++ b/symbolic_encoding/0008_sol.tex @@ -0,0 +1,4 @@ +We use 5 Boolean variables, \{$v_4$, . . . , $v_0$\}, for the encoding.\\ + +$A = (v_2 \land v_3)$\\ +$B = \lnot v_4$ \ No newline at end of file diff --git a/symbolic_encoding/1000.tex b/symbolic_encoding/1000.tex new file mode 100644 index 0000000..ea247e3 --- /dev/null +++ b/symbolic_encoding/1000.tex @@ -0,0 +1,17 @@ +\item \self +Listed are the participants of a seminar as well as their choice of snacks. Find a symbolic encodings for the participants. +For for this encoding, give the symbolic representation of the set $B$ of all participants that ordered \emph{bananas}, and the set $C$ of all participants that ordered cake. + + \begin{tabular}{l|l} + Name & Snack \\ + \hline + Alice & banana \\ + Bob & cake \\ + Carl & banana \\ + David & banana \\ + Eve & cake \\ + Frank & cake \\ + Greg & orange \\ + Hank & cake \\ + \end{tabular} + diff --git a/symbolic_encoding/1001.tex b/symbolic_encoding/1001.tex new file mode 100644 index 0000000..4f8f219 --- /dev/null +++ b/symbolic_encoding/1001.tex @@ -0,0 +1,8 @@ +\item \self + +Consider the example of a controller for a lamp. + +Initially the light is off. Pressing the button once turns on the light and the light glows white. From this state, any short-lasting pressure of the button causes the light to switch its color randomly between white, red, green, blue, and yellow. +At any state, pressing the button for a longer time turns the light off. + +Model the lamp controller as \emph{transition system}. diff --git a/symbolic_encoding/1002.tex b/symbolic_encoding/1002.tex new file mode 100644 index 0000000..2ac3f2b --- /dev/null +++ b/symbolic_encoding/1002.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 2^4 = 16$. Give the symbolic encoding for the following states: (a) $s_{4}$, (b) $s_{9}$, and (c) $s_{13}$. diff --git a/symbolic_encoding/1003.tex b/symbolic_encoding/1003.tex new file mode 100644 index 0000000..65d9ca2 --- /dev/null +++ b/symbolic_encoding/1003.tex @@ -0,0 +1,2 @@ +\item \self Given is the set of states $S=\{s_0,\dots,s_7\}$. +Find formulas in propositional logic that symbolically represent the sets $A = \{s_0, s_2,s_4, s_6 \}$, $B=\{s_0, s_1,s_2, s_3\}$, and $C=\{s_7, s_1\}$. diff --git a/symbolic_encoding/1004.tex b/symbolic_encoding/1004.tex new file mode 100644 index 0000000..194a30a --- /dev/null +++ b/symbolic_encoding/1004.tex @@ -0,0 +1,25 @@ +\item \self + Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + %\path[->] (s0) edge (s1); + \path[->] (s0) edge (s2); + \path[->] (s0) edge (s3); + \path[->] (s1) edge (s2); + \path[->] (s1) edge (s3); + %\path[->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + %\path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + %\path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/1005.tex b/symbolic_encoding/1005.tex new file mode 100644 index 0000000..818e444 --- /dev/null +++ b/symbolic_encoding/1005.tex @@ -0,0 +1,25 @@ +\item \self + Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[<->] (s0) edge (s1); + \path[<->] (s0) edge (s2); + \path[<->] (s0) edge (s3); + \path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + %\path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/1006.tex b/symbolic_encoding/1006.tex new file mode 100644 index 0000000..6bc3ff4 --- /dev/null +++ b/symbolic_encoding/1006.tex @@ -0,0 +1,25 @@ +\item \self +Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[<->] (s0) edge (s2); + %\path[<->] (s0) edge (s2); + %\path[<->] (s0) edge (s3); + %\path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + %\path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/1007.tex b/symbolic_encoding/1007.tex new file mode 100644 index 0000000..e9ab01b --- /dev/null +++ b/symbolic_encoding/1007.tex @@ -0,0 +1,7 @@ +\item \self Define the \textit{transition system} from the following symbolically encoded transition relations and draw the + corresponding graph: + \begin{align*} + (v_1 \land v_0 \land \lnot v'_1 \land \neg v'_0) & \enspace \lor \\ + (\neg v_1 \land v_0 \land \lnot v'_1 \land v'_0) & \enspace \lor \\ + (v_1 \land v_0 \land v'_1 \land v'_0) & + \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/1008.tex b/symbolic_encoding/1008.tex new file mode 100644 index 0000000..e79edba --- /dev/null +++ b/symbolic_encoding/1008.tex @@ -0,0 +1,7 @@ +\item \self Define the \textit{transition system} from the following symbolically encoded transition relations and draw the + corresponding graph: + \begin{align*} + (\lnot v_1 \land \lnot v_0 \land v'_1 \land v'_0) & \enspace \lor \\ + (\neg v_1 \land v_0 \land \lnot v'_1 \land \lnot v'_0) & \enspace \lor \\ + (\lnot v_1 \land \lnot v_0 \land \lnot v'_1 \land \lnot v'_0) & + \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/1009.tex b/symbolic_encoding/1009.tex new file mode 100644 index 0000000..ce68361 --- /dev/null +++ b/symbolic_encoding/1009.tex @@ -0,0 +1,3 @@ +\item \self What is the main advantage of symbolic set operations over + non-symbolic operations that enumerate all set elements + explicitly? diff --git a/symbolic_encoding/1010.tex b/symbolic_encoding/1010.tex new file mode 100644 index 0000000..ea247e3 --- /dev/null +++ b/symbolic_encoding/1010.tex @@ -0,0 +1,17 @@ +\item \self +Listed are the participants of a seminar as well as their choice of snacks. Find a symbolic encodings for the participants. +For for this encoding, give the symbolic representation of the set $B$ of all participants that ordered \emph{bananas}, and the set $C$ of all participants that ordered cake. + + \begin{tabular}{l|l} + Name & Snack \\ + \hline + Alice & banana \\ + Bob & cake \\ + Carl & banana \\ + David & banana \\ + Eve & cake \\ + Frank & cake \\ + Greg & orange \\ + Hank & cake \\ + \end{tabular} + diff --git a/symbolic_encoding/1011.tex b/symbolic_encoding/1011.tex new file mode 100644 index 0000000..2b8ff64 --- /dev/null +++ b/symbolic_encoding/1011.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 2048$, find a symbolic binary encoding for this state space and compute the characteristic function for the sets of states $$B = \{s_0, s_1, s_2, ..., s_{1023}\} \enspace \text{and} \enspace C = \{s_{512}, s_{513},, s_{514}, ..., s_{1535}.\}$$ Then compute the characteristic function for the sets $D = B \cup C$ and $E = B \setminus C$. If possible, simplify the formulas. \ No newline at end of file diff --git a/symbolic_encoding/1012.tex b/symbolic_encoding/1012.tex new file mode 100644 index 0000000..58c4515 --- /dev/null +++ b/symbolic_encoding/1012.tex @@ -0,0 +1,15 @@ +\item \self The following table shows eight students and their means of transportation. Find a symbolic encodings representing the list of students. +For this encoding, give the symbolic representation of the set $B$ of all students that go by \emph{bike}, and the set $C$ of all students that go by \emph{car}. + + \begin{tabular}{l|l} + Name & Transportation \\ + \hline + Alice & Car \\ + Bob & Bike \\ + Carl & Tram \\ + David & Bike \\ + Eve & Tram \\ + Frank & Bike \\ + Greg & Tram \\ + Hank & Bike \\ + \end{tabular} \ No newline at end of file diff --git a/symbolic_encoding/1013.tex b/symbolic_encoding/1013.tex new file mode 100644 index 0000000..e84fc59 --- /dev/null +++ b/symbolic_encoding/1013.tex @@ -0,0 +1,36 @@ +\item \self +Consider the domain $A=\{Spain, France, Italy, Germany\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter symbolic representation for the set + $B=\{France, Italy\}$? Illustrate your answer by giving the + representing formulas for $B$ in both encodings. + +\vspace{.5cm} + +% \begin{minipage} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $0$ & $1$ \\ + Germany & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $1$ & $1$ \\ + Germany & $0$ & $1$ + \end{tabular} +%\end{minipage} diff --git a/symbolic_encoding/1014.tex b/symbolic_encoding/1014.tex new file mode 100644 index 0000000..97cdec2 --- /dev/null +++ b/symbolic_encoding/1014.tex @@ -0,0 +1,41 @@ +\item \self Consider the following set operations and relations between + two sets $X$ and $Y$, and an element $a$: +\begin{enumerate} +\item Union: $X \cup Y$ +\item Intersection: $X \cap Y$ +\item Set Difference: $X \setminus Y$ +\item Containment: $a \in X$? +\item Subset: $X \subseteq Y$? +\item Strict Subset: $X \subset Y$? +\item Emptiness: $X=\emptyset$? +\item Equality: $X=Y$? +\end{enumerate} +Let $x$ and $y$ be the symbolic representations of $X$ and $Y$ +respectively, and let $\alpha$ be the symbolic encoding of element +$a$. For each of the following items, state which of the above +operations is performed, or which of the above questions is answered. +Write the letters of the corresponding operation/question into the +boxes of the items below. Note that some of the items below do not +perform any of the above operations or answer any of the above +questions. Put a ``--'' in the box of these items. Also note that +some of the items below might do the same computation or answer the +same question. +\begin{itemize} +\item[\Huge{$\square$}] $\neg x \vee y$ +\item[\Huge{$\square$}] $x \wedge y$ +\item[\Huge{$\square$}] $x\equiv \top$? +\item[\Huge{$\square$}] $x\equiv y$? +\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (y \rightarrow + x)$? +\item[\Huge{$\square$}] $x\equiv \bot$? +\item[\Huge{$\square$}] $y \wedge \neg x$ +\item[\Huge{$\square$}] $x \rightarrow \bot$? +\item[\Huge{$\square$}] $\alpha \models x$? +\item[\Huge{$\square$}] $\alpha \models \neg x$? +\item[\Huge{$\square$}] $\neg \alpha \models x$? +\item[\Huge{$\square$}] $x \rightarrow \alpha$? +\item[\Huge{$\square$}] $y \rightarrow x$? +\item[\Huge{$\square$}] $x \rightarrow y$? +\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (x\not \equiv + y)$? +\end{itemize} diff --git a/symbolic_encoding/1015.tex b/symbolic_encoding/1015.tex new file mode 100644 index 0000000..e61733e --- /dev/null +++ b/symbolic_encoding/1015.tex @@ -0,0 +1,14 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. + + \begin{itemize} + \item $B =\{4, 5, 12, 13, 20, 21, 28, 29 \}$ + \item $C =\{1, 2, 13, 14 \}$ + \end{itemize} + + Compute the characteristic functions of the following sets by symbolic operations, using your results from before. + \begin{enumerate} + \item $D = B \cup C$ + \item $E = X \setminus D$ + \end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/1016.tex b/symbolic_encoding/1016.tex new file mode 100644 index 0000000..7b8fe3c --- /dev/null +++ b/symbolic_encoding/1016.tex @@ -0,0 +1,15 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. +\begin{itemize} + \item $B =\{x \in X \mid \text{x is even}\}$ + \item $C =\{x \in X \mid \text{x is odd}\}$ + \item $D =\{0,1,2,3,4,5,6,7\}$ +\end{itemize} + +Compute the characteristic functions of the following sets by symbolic operations, using your results from before. +\begin{enumerate} + \item $E = B \cup D$ + \item $F = C \cap E$ + \item $G = E \setminus F$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/1017.tex b/symbolic_encoding/1017.tex new file mode 100644 index 0000000..81e580d --- /dev/null +++ b/symbolic_encoding/1017.tex @@ -0,0 +1,15 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. + +\begin{itemize} + \item $B =\{8, 9, 10, 11, 12, 13, 14, 15\}$ + \item $C =\{x \in X \mid 0 \leq x \leq 15\}$ +\end{itemize} + +Compute the characteristic functions of the following sets by symbolic operations, using your results from before. +\begin{enumerate} + \item $D = B \cup C$ + \item $E = B \cap C$ + \item $F = C \setminus B$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/1018.tex b/symbolic_encoding/1018.tex new file mode 100644 index 0000000..054efd0 --- /dev/null +++ b/symbolic_encoding/1018.tex @@ -0,0 +1,4 @@ +\item \self Assume you are given the formulas $a$ and + $b$, which symbolically represent the sets $A$ and $B$, + respectively. Give the formula + $c$, which symbolically represents the set $C= A \setminus B$. diff --git a/symbolic_encoding/1019.tex b/symbolic_encoding/1019.tex new file mode 100644 index 0000000..115d9de --- /dev/null +++ b/symbolic_encoding/1019.tex @@ -0,0 +1,5 @@ +\item \self Assume you are given the formulas $a$ and + $b$, which symbolically represent the sets $A$ and $B$, + respectively. What would you have to check on $a, b$ to test + whether or not $A$ is a strict subset of $B$, i.e., $A \subset + B$? diff --git a/symbolic_encoding/1020.tex b/symbolic_encoding/1020.tex new file mode 100644 index 0000000..84a036d --- /dev/null +++ b/symbolic_encoding/1020.tex @@ -0,0 +1,3 @@ +\item \self Given a state space of size $|S| = 64$. Find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets $$B = \{s_{32}, s_{33}, s_{34}, ..., s_{63}\} \enspace \text{and} \enspace C = \{s_{16}, s_{17},, s_{18}, ..., s_{40}\}.$$ + +Following, compute the formulas that represent the sets $D = B \cap C$, $E = B \cup C$, $F = B \setminus C$ and $G = C \setminus B$. \ No newline at end of file diff --git a/symbolic_encoding/1021.tex b/symbolic_encoding/1021.tex new file mode 100644 index 0000000..a654fb9 --- /dev/null +++ b/symbolic_encoding/1021.tex @@ -0,0 +1,2 @@ +\item \self + Given a state space of size $|S| = 64$, find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets of states $$B = \{s_{16}, s_{17}, s_{18}, ..., s_{32}\} \enspace \text{and} \enspace C = \{s_{24}, s_{25},, s_{26}, ..., s_{64}.\}$$ Then compute the formulas that symbolically represent the sets $D = B \cap C$ and $E = B \cup C$. \ No newline at end of file diff --git a/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex b/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex new file mode 100644 index 0000000..3af6ca1 --- /dev/null +++ b/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex @@ -0,0 +1,8 @@ +\item \lect Given a state space of the size $|S| = 2^5 = 32$ and assuming $v_4$ is the most significant bit and $v_0$ is the least significant bit, which of the following symbolic representations or the given states is correct? + +\begin{enumerate} + \item[$\square$] State $s_{15}$ is represented by: $\lnot v_4 \land v_3 \land v_3, \land v_1 \land \lnot v_0$ + \item[$\square$] State $s_{31}$ is represented by: $v_4 \land v_3 \land v_3 \land v_1 \land v_0$ + \item[$\square$] State $s_{4}$ is represented by: $\lnot v_4 \land \lnot v_3 \land \lnot v_2, \land v_1 \land \lnot v_0$ + \item[$\square$] State $s_{10}$ is represented by: $v_4 \land v_3 \land \lnot v_3 \land \lnot v_1 \land v_0$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex b/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex new file mode 100644 index 0000000..e924dbf --- /dev/null +++ b/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex @@ -0,0 +1,8 @@ +\item \self Given a state space of the size $|S| = 2^9 = 512$ and assuming $v_8$ is the most significant bit and $v_0$ is the least significant bit, which of the following symbolic representations or the given states is correct? + +\begin{enumerate} + \item[$\square$] State $s_{214}$ is represented by: $\lnot v_8 \land v_7 \land v_6 \land \lnot v_5 \land v_4 \land \lnot v_3 \land v_2 \land v_1 \land \lnot v_0$ + \item[$\square$] State $s_{501}$ is represented by: $v_8 \land v_7 \land v_6 \land v_5 \land v_4 \land \lnot v_3 \land v_2 \land \lnot v_1 \land v_0$ + \item[$\square$] State $s_{0}$ is represented by: $\lnot v_8 \land \lnot v_7 \land \lnot v_6 \land \lnot v_5 \land \lnot v_4 \land \lnot v_3 \land \lnot v_2 \land \lnot v_1 \land \lnot v_0$ + \item[$\square$] State $s_{448}$ is represented by: $v_8 \land v_7 \land v_6 \land \lnot v_5 \land \lnot v_4 \land \lnot v_3 \land \lnot v_2 \land v_1 \land \lnot v_0$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_10_kripke_self.tex b/symbolic_encoding/practical_questions/1_10_kripke_self.tex new file mode 100644 index 0000000..4f8f219 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_10_kripke_self.tex @@ -0,0 +1,8 @@ +\item \self + +Consider the example of a controller for a lamp. + +Initially the light is off. Pressing the button once turns on the light and the light glows white. From this state, any short-lasting pressure of the button causes the light to switch its color randomly between white, red, green, blue, and yellow. +At any state, pressing the button for a longer time turns the light off. + +Model the lamp controller as \emph{transition system}. diff --git a/symbolic_encoding/practical_questions/1_1_kripke_lect.tex b/symbolic_encoding/practical_questions/1_1_kripke_lect.tex new file mode 100644 index 0000000..a199b5d --- /dev/null +++ b/symbolic_encoding/practical_questions/1_1_kripke_lect.tex @@ -0,0 +1,4 @@ +\item \lect Draw the graph for a \emph{transition system} $\mathcal{T}$ with: +$S = \{s_1, s_2, s_3, s_4\}, $\\ +$S_0 = \{s_2\}, $\\ +$R = \{\{s_1, s_2\}, \{s_1, s_1\}, \{s_2, s_4\}, \{s_2, s_3\}, \{s_3, s_1\}, \{s_4, s_2\}, \{s_4, s_3\}\}, $ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex b/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex new file mode 100644 index 0000000..11f08e8 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex @@ -0,0 +1,29 @@ +\begin{center} +\begin{tikzpicture}[scale=0.2] +\tikzstyle{every node}+=[inner sep=0pt] +\draw [black] (11,-26.9) circle (3); +\draw (11,-26.9) node {$s_2$}; +\draw [black] (23.6,-15) circle (3); +\draw (23.6,-15) node {$s_1$}; +\draw [black] (23.6,-38) circle (3); +\draw (23.6,-38) node {$s_4$}; +\draw [black] (36.7,-26.9) circle (3); +\draw (36.7,-26.9) node {$s_3$}; +\draw [black] (21.42,-17.06) -- (13.18,-24.84); +\fill [black] (13.18,-24.84) -- (14.11,-24.65) -- (13.42,-23.93); +\draw [black] (3.7,-26.9) -- (8,-26.9); +\fill [black] (8,-26.9) -- (7.2,-26.4) -- (7.2,-27.4); +\draw [black] (25.89,-36.06) -- (34.41,-28.84); +\fill [black] (34.41,-28.84) -- (33.48,-28.98) -- (34.12,-29.74); +\draw [black] (34.48,-24.88) -- (25.82,-17.02); +\fill [black] (25.82,-17.02) -- (26.08,-17.93) -- (26.75,-17.18); +\draw [black] (14,-26.9) -- (33.7,-26.9); +\fill [black] (33.7,-26.9) -- (32.9,-26.4) -- (32.9,-27.4); +\draw [black] (21.35,-36.02) -- (13.25,-28.88); +\fill [black] (13.25,-28.88) -- (13.52,-29.79) -- (14.18,-29.04); +\draw [black] (13.25,-28.88) -- (21.35,-36.02); +\fill [black] (21.35,-36.02) -- (21.08,-35.11) -- (20.42,-35.86); +\draw [black] (25.456,-12.658) arc (169.34618:-118.65382:2.25); +\fill [black] (26.59,-15.05) -- (27.28,-15.69) -- (27.47,-14.7); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_1_kripke_self.tex b/symbolic_encoding/practical_questions/1_1_kripke_self.tex new file mode 100644 index 0000000..7771977 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_1_kripke_self.tex @@ -0,0 +1,5 @@ +\item \self Draw the graph for a \emph{transition system} $\mathcal{T}$ with: + +$S = \{s_0, s_1, s_2\}, $\\ +$S_0 = \{s_0, s_1\}, $\\ +$R = \{\{s_0, s_0\}, \{s_0, s_1\}, \{s_0, s_2\}, \{s_1, s_0\}, \{s_1, s_1\}, \{s_1, s_2\}, \{s_2, s_0\}, \{s_2, s_1\}, \{s_2, s_2\}\}$. diff --git a/symbolic_encoding/practical_questions/1_1_symbrep.tex b/symbolic_encoding/practical_questions/1_1_symbrep.tex new file mode 100644 index 0000000..2ac3f2b --- /dev/null +++ b/symbolic_encoding/practical_questions/1_1_symbrep.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 2^4 = 16$. Give the symbolic encoding for the following states: (a) $s_{4}$, (b) $s_{9}$, and (c) $s_{13}$. diff --git a/symbolic_encoding/practical_questions/1_1_symbrep_self.tex b/symbolic_encoding/practical_questions/1_1_symbrep_self.tex new file mode 100644 index 0000000..2ac3f2b --- /dev/null +++ b/symbolic_encoding/practical_questions/1_1_symbrep_self.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 2^4 = 16$. Give the symbolic encoding for the following states: (a) $s_{4}$, (b) $s_{9}$, and (c) $s_{13}$. diff --git a/symbolic_encoding/practical_questions/1_2_kripke_lect.tex b/symbolic_encoding/practical_questions/1_2_kripke_lect.tex new file mode 100644 index 0000000..1d33b8b --- /dev/null +++ b/symbolic_encoding/practical_questions/1_2_kripke_lect.tex @@ -0,0 +1,38 @@ + +\item \lect +Consider the example of an elevator. +Initially, the elevator is in the ground floor. +From the ground floor, it can either go basement, stay there for a while, +and then go back to the ground floor, or it can go from the ground floor +to the second floor, stay there for a while, and go back to the ground floor. +While traveling between ground floor to second floor, the elevator passes the first floor, but it cannot stop there. + +Model this elevator as \emph{transition system}. + + + + +\iffalse +\item \lect + Given the following graph representation of a \textit{transition system}, state the contents of the sets $S, S_0 and R$ + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=20pt}] + \node[node] (s0) {$s0$}; + \node (s0s2) [below= 1cm of s0] {}; + \node[node] (s1) [right of=s0s2] {$s1$}; + \node[node] (s2) [below of=s0] {$s2$}; + \node (start1) [left=1cm of s0] {}; + + \path[->] (start1) edge (s0); + \path[->] (s1) edge (s0); + \path[->] (s0) edge [bend left] (s2); + \path[->] (s2) edge (s1); + \path[->] (s2) edge [bend left] (s0); + \path[->] (s0.30) edge[bend right=90, looseness=15, out=240, in=300] (s0.60); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); +\end{tikzpicture} +\end{center} +\fi \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex b/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex new file mode 100644 index 0000000..87eeeb8 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex @@ -0,0 +1,44 @@ +We use the following states: +%ground floor, basement,second floor, passing ground floor +\begin{itemize} +\item $s_g$ indicates that the elevator is on the ground floor. +\item $s_b$ indicates that the elevator is in the basement. +\item $s_s$ indicates that the elevator is on the second floor. +\item $s_f$ indicates that the elevator is passing the first floor. +\end{itemize} +The transition system is then given by: $\mathcal{T}$ = ($S$, $S_0$, $R$) with $S$ = $\{s_g, s_b, s_s, s_f\}$, $S_0$ = $\{s_g\}$, $R$ = $\{(s_g, s_g), (s_g, s_b), (s_b, s_b), (s_b, s_g), (s_g, s_f), (s_f, s_s), (s_s, s_s), (s_s, s_f), (s_f, s_g)\}$\\ + + +\begin{center} +\begin{tikzpicture}[scale=0.2] +\tikzstyle{every node}+=[inner sep=0pt] +\draw [black] (13.9,-26) circle (3); +\draw (13.9,-26) node {$s_g$}; +\draw [black] (27.8,-35.6) circle (3); +\draw (27.8,-35.6) node {$s_b$}; +\draw [black] (27.8,-26) circle (3); +\draw (27.8,-26) node {$s_f$}; +\draw [black] (27.8,-15.8) circle (3); +\draw (27.8,-15.8) node {$s_s$}; +\draw [black] (4.8,-26) -- (10.9,-26); +\fill [black] (10.9,-26) -- (10.1,-25.5) -- (10.1,-26.5); +\draw [black] (11.501,-24.218) arc (261.13116:-26.86884:2.25); +\fill [black] (13.85,-23.01) -- (14.47,-22.3) -- (13.48,-22.14); +\draw [black] (16.37,-27.7) -- (25.33,-33.9); +\fill [black] (25.33,-33.9) -- (24.96,-33.03) -- (24.39,-33.85); +\draw [black] (26.957,-38.467) arc (11.34364:-276.65636:2.25); +\fill [black] (25.01,-36.67) -- (24.13,-36.34) -- (24.33,-37.32); +\draw [black] (25.33,-33.9) -- (16.37,-27.7); +\fill [black] (16.37,-27.7) -- (16.74,-28.57) -- (17.31,-27.75); +\draw [black] (16.9,-26) -- (24.8,-26); +\fill [black] (24.8,-26) -- (24,-25.5) -- (24,-26.5); +\draw [black] (27.8,-23) -- (27.8,-18.8); +\fill [black] (27.8,-18.8) -- (27.3,-19.6) -- (28.3,-19.6); +\draw [black] (28.483,-12.891) arc (194.52895:-93.47105:2.25); +\fill [black] (30.52,-14.57) -- (31.42,-14.86) -- (31.17,-13.89); +\draw [black] (27.8,-18.8) -- (27.8,-23); +\fill [black] (27.8,-23) -- (28.3,-22.2) -- (27.3,-22.2); +\draw [black] (24.8,-26) -- (16.9,-26); +\fill [black] (16.9,-26) -- (17.7,-26.5) -- (17.7,-25.5); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_2_kripke_self.tex b/symbolic_encoding/practical_questions/1_2_kripke_self.tex new file mode 100644 index 0000000..194a30a --- /dev/null +++ b/symbolic_encoding/practical_questions/1_2_kripke_self.tex @@ -0,0 +1,25 @@ +\item \self + Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + %\path[->] (s0) edge (s1); + \path[->] (s0) edge (s2); + \path[->] (s0) edge (s3); + \path[->] (s1) edge (s2); + \path[->] (s1) edge (s3); + %\path[->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + %\path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + %\path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/practical_questions/1_2_symbrep_self.tex b/symbolic_encoding/practical_questions/1_2_symbrep_self.tex new file mode 100644 index 0000000..65d9ca2 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_2_symbrep_self.tex @@ -0,0 +1,2 @@ +\item \self Given is the set of states $S=\{s_0,\dots,s_7\}$. +Find formulas in propositional logic that symbolically represent the sets $A = \{s_0, s_2,s_4, s_6 \}$, $B=\{s_0, s_1,s_2, s_3\}$, and $C=\{s_7, s_1\}$. diff --git a/symbolic_encoding/practical_questions/1_3_kripke_self.tex b/symbolic_encoding/practical_questions/1_3_kripke_self.tex new file mode 100644 index 0000000..818e444 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_3_kripke_self.tex @@ -0,0 +1,25 @@ +\item \self + Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[<->] (s0) edge (s1); + \path[<->] (s0) edge (s2); + \path[<->] (s0) edge (s3); + \path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + %\path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/practical_questions/1_4_kripke_self.tex b/symbolic_encoding/practical_questions/1_4_kripke_self.tex new file mode 100644 index 0000000..6bc3ff4 --- /dev/null +++ b/symbolic_encoding/practical_questions/1_4_kripke_self.tex @@ -0,0 +1,25 @@ +\item \self +Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[<->] (s0) edge (s2); + %\path[<->] (s0) edge (s2); + %\path[<->] (s0) edge (s3); + %\path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + %\path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} diff --git a/symbolic_encoding/practical_questions/2_05_symbrep_self.tex b/symbolic_encoding/practical_questions/2_05_symbrep_self.tex new file mode 100644 index 0000000..b9b1458 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_05_symbrep_self.tex @@ -0,0 +1,32 @@ +\item \self Let $x$ and $y$ be the symbolic representations of the sets $X$ and + $Y$ respectively, and let $\alpha$ be the symbolic encoding of an + element $a$. Consider the following operations and relations + between $x$, $y$, and $\alpha$: + +\begin{enumerate}[A.] +\item $x \rightarrow y$ +\item $\alpha \models x$ ? +\item $x \wedge \neg y$ +\item $\alpha \nvDash y$ ? +\item $x \equiv \bot$ ? +\item $x \vee y$ +\end{enumerate} + +For each of the following items, state which of the above operations +symbolically performs the respective set operation or answers the +respective set-specific question. Write the letters of the +corresponding operation/question into the boxes of the items below. +Note that some of the items below do not correspond to any of the +above operations or questions. Put a ``--'' in the box of these +items. + +\begin{itemize} +\item[\Huge{$\square$}] Union: $X \cup Y$ +\item[\Huge{$\square$}] Intersection: $X \cap Y$ +\item[\Huge{$\square$}] Set Difference: $X \setminus Y$ +\item[\Huge{$\square$}] Containment: $a \in X$? +\item[\Huge{$\square$}] Subset: $X \subseteq Y$? +\item[\Huge{$\square$}] Strict Subset: $X \subset Y$? +\item[\Huge{$\square$}] Emptiness: $X=\emptyset$? +\item[\Huge{$\square$}] Equality: $X=Y$? +\end{itemize} diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex new file mode 100644 index 0000000..a9ea243 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex @@ -0,0 +1,39 @@ + +\item \lect +Consider the domain $A=\{Spain, France, Italy, Germany\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter symbolic representation for the set + $B=\{France, Germany\}$? Illustrate your answer by giving the + representing formulas for $B$ in both encodings. + +\vspace{.5cm} + +% \begin{minipage} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $0$ & $1$ \\ + Germany & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $1$ & $1$ \\ + Germany & $0$ & $1$ + \end{tabular} +%\end{minipage} + + \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex new file mode 100644 index 0000000..d6b73f7 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex @@ -0,0 +1,7 @@ +Using encoding 1, we end up in the following formula:\\ +$b = v_1$\\\\ +Using encoding 2, we end up in the following formula:\\ +$b = (v_1 \land \lnot v_0) \lor (\lnot v_1 \land v_0)$\\ + +Encoding 1 gives a shorter symbolic representation +for the set $B=\{France, Germany\}$. diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_self.tex b/symbolic_encoding/practical_questions/2_10_symbrep_self.tex new file mode 100644 index 0000000..b9d0410 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_10_symbrep_self.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 16$, find a symbolic binary encoding for this state space and compute the characteristic function for the sets of states $$C = \{s_{0}, s_{2}, s_{8}, s_{10}\} \enspace \text{and} \enspace C = \{s_{0}, s_{2}, s_{8}, s_{10}\}$$ Then compute the characteristic function for the sets $D = C \subseteq B$, $E = B \setminus C$ and $F = S \setminus E$. If possible, simplify the formulas. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex new file mode 100644 index 0000000..0f137e4 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex @@ -0,0 +1,9 @@ +\item \lect +Find a symbolic binary encoding for $X = \{ 0,1, \ldots, 31 \}$. + Use it to find formulas that symbolically represent the sets $A$ and $B$ and simplify the formulas: + \begin{itemize} + \item $A =\{ 12, 13, 14, 15, 28, 29, 30, 31 \}$ + \item $B =\{x \in X \mid 0 \leq x \leq 15\}$ + \end{itemize} + Furthermore, give the formulas representing the sets + $C=A\cap B$ and $D = A \cup B$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex new file mode 100644 index 0000000..db46cc5 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex @@ -0,0 +1,4 @@ +We use 5 Boolean variables, \{$v_4$, . . . , $v_0$\}, for the encoding.\\ + +$A = (v_2 \land v_3)$\\ +$B = \lnot v_4$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_self.tex b/symbolic_encoding/practical_questions/2_11_symbrep_self.tex new file mode 100644 index 0000000..6438172 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_11_symbrep_self.tex @@ -0,0 +1,21 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to find characteristic functions for the following sets. If possible, simplify the formulas. + + \begin{enumerate} + \item $B =\{x \in X \mid 24 \leq x < 32\}$ + \item + $C = \left\{ x \in X \middle| \enspace + \begin{array}{lll} + 4 & \leq \enspace x & < 8 \\ + 12 & \leq \enspace x & < 16 \\ + 20 & \leq \enspace x & < 24 + \end{array} + \right\}$ + \end{enumerate} + + Compute the characteristic functions of the following sets by symbolic operations, using your results from before and simplify your formulas. + \begin{enumerate} + \item $D = B \cup C$ + \item $E = B \cap C$ + \end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex new file mode 100644 index 0000000..e79edba --- /dev/null +++ b/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex @@ -0,0 +1,7 @@ +\item \self Define the \textit{transition system} from the following symbolically encoded transition relations and draw the + corresponding graph: + \begin{align*} + (\lnot v_1 \land \lnot v_0 \land v'_1 \land v'_0) & \enspace \lor \\ + (\neg v_1 \land v_0 \land \lnot v'_1 \land \lnot v'_0) & \enspace \lor \\ + (\lnot v_1 \land \lnot v_0 \land \lnot v'_1 \land \lnot v'_0) & + \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_12_symbrep_self.tex b/symbolic_encoding/practical_questions/2_12_symbrep_self.tex new file mode 100644 index 0000000..81e580d --- /dev/null +++ b/symbolic_encoding/practical_questions/2_12_symbrep_self.tex @@ -0,0 +1,15 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. + +\begin{itemize} + \item $B =\{8, 9, 10, 11, 12, 13, 14, 15\}$ + \item $C =\{x \in X \mid 0 \leq x \leq 15\}$ +\end{itemize} + +Compute the characteristic functions of the following sets by symbolic operations, using your results from before. +\begin{enumerate} + \item $D = B \cup C$ + \item $E = B \cap C$ + \item $F = C \setminus B$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex new file mode 100644 index 0000000..7c4e8d5 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex @@ -0,0 +1,24 @@ +\item \lect Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + \path[->] (s0) edge (s1); + \path[<->] (s0) edge (s2); + \path[<->] (s0) edge (s3); + \path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + \path[<->] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex new file mode 100644 index 0000000..bd9c552 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex @@ -0,0 +1,15 @@ +Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ +\begin{center} + $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $\lnot v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0)$ +\end{center} + +We can further simplify the formula to: +\begin{center} + $\lnot v_1 \land \lnot v_0 \lor$\\ + $\lnot v_1 \land v_0 \land (v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ + $v_1 \land \lnot v_0 \land (\lnot v'_1 \lor v'_1 \land v'_0) \ \lor$\\ + $v_1 \land v_0$ +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_self.tex b/symbolic_encoding/practical_questions/2_13_symbrep_self.tex new file mode 100644 index 0000000..7b8fe3c --- /dev/null +++ b/symbolic_encoding/practical_questions/2_13_symbrep_self.tex @@ -0,0 +1,15 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. +\begin{itemize} + \item $B =\{x \in X \mid \text{x is even}\}$ + \item $C =\{x \in X \mid \text{x is odd}\}$ + \item $D =\{0,1,2,3,4,5,6,7\}$ +\end{itemize} + +Compute the characteristic functions of the following sets by symbolic operations, using your results from before. +\begin{enumerate} + \item $E = B \cup D$ + \item $F = C \cap E$ + \item $G = E \setminus F$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_17_symbrep_self.tex b/symbolic_encoding/practical_questions/2_17_symbrep_self.tex new file mode 100644 index 0000000..48dd31b --- /dev/null +++ b/symbolic_encoding/practical_questions/2_17_symbrep_self.tex @@ -0,0 +1,33 @@ +\item \self Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \textit{Kripke structure} and +simplify your formulas. The labels of the states symbolize their symbolic encoding. +E.g. "110" = "$x_2 \land x_1 \land \lnot x_0$", i.e. the least significant bit corresponds to $x_0$, +the second-least significant bit to $x_1$, and so forth. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=2cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$000$}; + \node[node] (s1) [above right of=s0] {$001$}; + \node[node] (s2) [right of=s1] {$010$}; + \node[node] (s3) [below right of=s2] {$011$}; + \node[node] (s4) [below of=s3] {$100$}; + \node[node] (s5) [below left of=s4] {$101$}; + \node[node] (s6) [left of=s5] {$110$}; + \node[node] (s7) [above left of=s6] {$111$}; + + + + \path[->] (s0) edge (s1); + \path[->] (s1) edge (s2); + \path[<->] (s2) edge (s3); + \path[->] (s3) edge (s4); + \path[->] (s4) edge (s7); + \path[->] (s7) edge (s6); + \path[<->] (s6) edge (s5); + \path[->] (s3) edge (s6); + \path[->] (s5) edge (s0); + \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + \path[->] (s4.30) edge[bend right=90, looseness=15, out=240, in=300] (s4.60); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_18_symbrep_self.tex b/symbolic_encoding/practical_questions/2_18_symbrep_self.tex new file mode 100644 index 0000000..e9ab01b --- /dev/null +++ b/symbolic_encoding/practical_questions/2_18_symbrep_self.tex @@ -0,0 +1,7 @@ +\item \self Define the \textit{transition system} from the following symbolically encoded transition relations and draw the + corresponding graph: + \begin{align*} + (v_1 \land v_0 \land \lnot v'_1 \land \neg v'_0) & \enspace \lor \\ + (\neg v_1 \land v_0 \land \lnot v'_1 \land v'_0) & \enspace \lor \\ + (v_1 \land v_0 \land v'_1 \land v'_0) & + \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex new file mode 100644 index 0000000..7d625ca --- /dev/null +++ b/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex @@ -0,0 +1 @@ +\item \lect Given a state space of size $|S| = 2^4 = 16$, give the symbolic encoding for the following states: (a) $s_{7}$, (b) $s_{15}$, and (c) $s_{10}$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex new file mode 100644 index 0000000..e574485 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex @@ -0,0 +1,6 @@ +For the symbolic encoding we need 4 Boolean variables, \{$v_3$, . . . , $v_0$\}. +Let $v_3$ be the most significant bit, and $v_0$ the least significant bit.\\ + +(a) $s_{7}$ = $\lnot v_3 \land v_2 \land v_1 \land v_0$\\ +(b) $s_{15}$ = $v_3 \land v_2 \land v_1 \land v_0$\\ +(c) $s_{10}$ = $v_3 \land \lnot v_2 \land v_1 \land \lnot v_0$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_self.tex b/symbolic_encoding/practical_questions/2_1_symbrep_self.tex new file mode 100644 index 0000000..a6507b4 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_1_symbrep_self.tex @@ -0,0 +1,7 @@ +\item \self Given a state space of the size $|S| = 2^{11} = 2048$, give the symbolic encoding for the following states: + +\begin{enumerate} + \item $s_{435}$ + \item $s_{1467}$ + \item $s_{2022}$ +\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_20_symbrep_self.tex b/symbolic_encoding/practical_questions/2_20_symbrep_self.tex new file mode 100644 index 0000000..a735070 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_20_symbrep_self.tex @@ -0,0 +1,9 @@ +\item \self Build a \textit{Kripke structure} from the following symbolically encoded transition relations and draw the + corresponding graph: + + \begin{align*} + (\lnot x_2 \land \lnot x_1 \land \lnot x_0) \land (\lnot x_2' \land x_0') & \enspace \lor \\ + (\lnot x_2 \land x_1) \land ((x_2' \oplus x_1') \land x_0') & \enspace \lor \\ + (x_2 \land (x_1 \leftrightarrow x_0)) \land (x_2' \land (x_1' \oplus x_0')) & \enspace \lor \\ + (x_2 \land x_1 \land \lnot x_0) \land (x_2' \land (x_1' \lor x_0')) & + \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex new file mode 100644 index 0000000..549492f --- /dev/null +++ b/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex @@ -0,0 +1,2 @@ +\item \lect Given is the set of states $S=\{s_0,\dots,s_7\}$. +Find formulas in propositional logic that symbolically represent the sets $A = \{s_7, s_6,s_3, s_2 \}$, $B=\{s_1, s_3,s_5, s_7\}$, and $C=\{s_7, s_6,s_0, s_1\}$. diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex new file mode 100644 index 0000000..02c3d2c --- /dev/null +++ b/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex @@ -0,0 +1,6 @@ +$A = \{s_7, s_6,s_3, s_2 \}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land \lnot v_0)$\\ +\hspace*{0,34cm} = $v_1$\\\\ +$B=\{s_1, s_3,s_5, s_7\}$ = $(\lnot v_2 \land \lnot v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (v_2 \land \lnot v_1 \land v_0) \lor (v_2 \land v_1 \land v_0)$\\ +\hspace*{0,34cm} = $v_0$\\\\ +$C=\{s_7, s_6,s_0, s_1\}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land v_0)$ \\ +\hspace*{0,34cm} = $(v_2 \land v_1) \lor (\lnot v_2 \land \lnot v_1)$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_self.tex b/symbolic_encoding/practical_questions/2_2_symbrep_self.tex new file mode 100644 index 0000000..5841294 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_2_symbrep_self.tex @@ -0,0 +1,8 @@ +\item \self Consider the following set of states defined by the valuations: +\begin{align*} + (v_0 \imp \top, v_1 \imp \top, v_2 \imp \top, v_3 \imp \bot), + (v_0 \imp \top, v_1 \imp \bot, v_2 \imp \top, v_3 \imp \bot),\\ + (v_0 \imp \top, v_1 \imp \bot, v_2 \imp \bot, v_3 \imp \bot), + (v_0 \imp \top, v_1 \imp \top, v_2 \imp \bot, v_3 \imp \bot), +\end{align*} +Represent this set of states symbolically using a propositional formula and simplify this formula as best as possible. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex new file mode 100644 index 0000000..0720fb4 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex @@ -0,0 +1,40 @@ +\item \lect Consider the domain $A=\{Maths, \;English, \;Biology, \;Physical \; Education\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter characteristic function for the following sets? + \begin{enumerate} + \item $B = \{Maths, \; Biology\}$ + \item $C = \{English, \; Biology\}$ + \item $D = \{Maths, \;Physical \; Education\}$ + \end{enumerate} + Illustrate your answer by giving the + characteristic function for $B$, $C$ and $D$ in both encodings. + +\vspace{.5cm} + +%\begin{minipage} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & x & y \\ + \hline + Maths & $0$ & $0$ \\ + English & $1$ & $0$ \\ + Biology & $0$ & $1$ \\ + Physical Education & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & x & y \\ + \hline + Maths & $0$ & $0$ \\ + English & $1$ & $0$ \\ + Biology & $1$ & $1$ \\ + Physical Education & $0$ & $1$ + \end{tabular} +%\end{minipage} diff --git a/symbolic_encoding/practical_questions/2_3_symbrep_self.tex b/symbolic_encoding/practical_questions/2_3_symbrep_self.tex new file mode 100644 index 0000000..e52ce46 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_3_symbrep_self.tex @@ -0,0 +1,48 @@ +\item \self Consider the domain $A=\{Asparagus, \;Bell \; Pepper, \;Cabbage, \;Tomato, \\ \; Onion, \;Zucchini, \;Eggplant, \; Mushroom\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter characteristic function for the following sets? + \begin{enumerate} + \item $B = \{Asparagus, \; Mushroom\}$ + \item $C = \{Bell \; Pepper, \; Onion, \; Zucchini, \; Eggplant\}$ + \item $D = \{Cabbage, \; Tomato\}$ + \end{enumerate} + Illustrate your answer by giving the + characteristic function for $B$, $C$ and $D$ in both encodings. + +\vspace{.5cm} + +%\begin{minipage} + \begin{tabular}{l|l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & x & y & z\\ + \hline + Asparagus & $0$ & $0$ & $0$ \\ + Bell Pepper & $0$ & $0$ & $1$ \\ + Cabbage & $0$ & $1$ & $0$ \\ + Tomato & $0$ & $1$ & $1$ \\ + Onion & $1$ & $0$ & $0$ \\ + Zucchini & $1$ & $0$ & $1$ \\ + Eggplant & $1$ & $1$ & $0$ \\ + Mushroom & $1$ & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & x & y & z \\ + \hline + Asparagus & $1$ & $1$ & $0$ \\ + Bell Pepper & $1$ & $0$ & $1$ \\ + Cabbage & $0$ & $1$ & $0$ \\ + Tomato & $1$ & $1$ & $1$ \\ + Onion & $0$ & $0$ & $0$ \\ + Zucchini & $0$ & $0$ & $1$ \\ + Eggplant & $1$ & $0$ & $0$ \\ + Mushroom & $0$ & $1$ & $1$ + \end{tabular} +%\end{minipage} diff --git a/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex new file mode 100644 index 0000000..58c4515 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex @@ -0,0 +1,15 @@ +\item \self The following table shows eight students and their means of transportation. Find a symbolic encodings representing the list of students. +For this encoding, give the symbolic representation of the set $B$ of all students that go by \emph{bike}, and the set $C$ of all students that go by \emph{car}. + + \begin{tabular}{l|l} + Name & Transportation \\ + \hline + Alice & Car \\ + Bob & Bike \\ + Carl & Tram \\ + David & Bike \\ + Eve & Tram \\ + Frank & Bike \\ + Greg & Tram \\ + Hank & Bike \\ + \end{tabular} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_4_symbrep_self.tex b/symbolic_encoding/practical_questions/2_4_symbrep_self.tex new file mode 100644 index 0000000..ea247e3 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_4_symbrep_self.tex @@ -0,0 +1,17 @@ +\item \self +Listed are the participants of a seminar as well as their choice of snacks. Find a symbolic encodings for the participants. +For for this encoding, give the symbolic representation of the set $B$ of all participants that ordered \emph{bananas}, and the set $C$ of all participants that ordered cake. + + \begin{tabular}{l|l} + Name & Snack \\ + \hline + Alice & banana \\ + Bob & cake \\ + Carl & banana \\ + David & banana \\ + Eve & cake \\ + Frank & cake \\ + Greg & orange \\ + Hank & cake \\ + \end{tabular} + diff --git a/symbolic_encoding/practical_questions/2_5_symbrep_self.tex b/symbolic_encoding/practical_questions/2_5_symbrep_self.tex new file mode 100644 index 0000000..e84fc59 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_5_symbrep_self.tex @@ -0,0 +1,36 @@ +\item \self +Consider the domain $A=\{Spain, France, Italy, Germany\}$ and + the two different symbolic encodings for $A$ given below. + Which one gives a shorter symbolic representation for the set + $B=\{France, Italy\}$? Illustrate your answer by giving the + representing formulas for $B$ in both encodings. + +\vspace{.5cm} + +% \begin{minipage} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 1}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $0$ & $1$ \\ + Germany & $1$ & $1$ + \end{tabular} +%\end{minipage} +%\begin{minipage} +\hspace{3cm} + \begin{tabular}{l|l|l} + \hline + \multicolumn{3}{c}{\textbf{Encoding 2}} \\ + \hline + Element & $v_1$ & $v_0$ \\ + \hline + Spain & $0$ & $0$ \\ + France & $1$ & $0$ \\ + Italy & $1$ & $1$ \\ + Germany & $0$ & $1$ + \end{tabular} +%\end{minipage} diff --git a/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex new file mode 100644 index 0000000..a654fb9 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex @@ -0,0 +1,2 @@ +\item \self + Given a state space of size $|S| = 64$, find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets of states $$B = \{s_{16}, s_{17}, s_{18}, ..., s_{32}\} \enspace \text{and} \enspace C = \{s_{24}, s_{25},, s_{26}, ..., s_{64}.\}$$ Then compute the formulas that symbolically represent the sets $D = B \cap C$ and $E = B \cup C$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_6_symbrep_self.tex b/symbolic_encoding/practical_questions/2_6_symbrep_self.tex new file mode 100644 index 0000000..97cdec2 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_6_symbrep_self.tex @@ -0,0 +1,41 @@ +\item \self Consider the following set operations and relations between + two sets $X$ and $Y$, and an element $a$: +\begin{enumerate} +\item Union: $X \cup Y$ +\item Intersection: $X \cap Y$ +\item Set Difference: $X \setminus Y$ +\item Containment: $a \in X$? +\item Subset: $X \subseteq Y$? +\item Strict Subset: $X \subset Y$? +\item Emptiness: $X=\emptyset$? +\item Equality: $X=Y$? +\end{enumerate} +Let $x$ and $y$ be the symbolic representations of $X$ and $Y$ +respectively, and let $\alpha$ be the symbolic encoding of element +$a$. For each of the following items, state which of the above +operations is performed, or which of the above questions is answered. +Write the letters of the corresponding operation/question into the +boxes of the items below. Note that some of the items below do not +perform any of the above operations or answer any of the above +questions. Put a ``--'' in the box of these items. Also note that +some of the items below might do the same computation or answer the +same question. +\begin{itemize} +\item[\Huge{$\square$}] $\neg x \vee y$ +\item[\Huge{$\square$}] $x \wedge y$ +\item[\Huge{$\square$}] $x\equiv \top$? +\item[\Huge{$\square$}] $x\equiv y$? +\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (y \rightarrow + x)$? +\item[\Huge{$\square$}] $x\equiv \bot$? +\item[\Huge{$\square$}] $y \wedge \neg x$ +\item[\Huge{$\square$}] $x \rightarrow \bot$? +\item[\Huge{$\square$}] $\alpha \models x$? +\item[\Huge{$\square$}] $\alpha \models \neg x$? +\item[\Huge{$\square$}] $\neg \alpha \models x$? +\item[\Huge{$\square$}] $x \rightarrow \alpha$? +\item[\Huge{$\square$}] $y \rightarrow x$? +\item[\Huge{$\square$}] $x \rightarrow y$? +\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (x\not \equiv + y)$? +\end{itemize} diff --git a/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex new file mode 100644 index 0000000..e61733e --- /dev/null +++ b/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex @@ -0,0 +1,14 @@ +\item \self Find a symbolic binary encoding for +$X = \{ 0,1, \ldots, 31 \}$. +Use it to compute formulas in propositional logic that symbolically represent the following sets. + + \begin{itemize} + \item $B =\{4, 5, 12, 13, 20, 21, 28, 29 \}$ + \item $C =\{1, 2, 13, 14 \}$ + \end{itemize} + + Compute the characteristic functions of the following sets by symbolic operations, using your results from before. + \begin{enumerate} + \item $D = B \cup C$ + \item $E = X \setminus D$ + \end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_7_symbrep_self.tex b/symbolic_encoding/practical_questions/2_7_symbrep_self.tex new file mode 100644 index 0000000..c01c81d --- /dev/null +++ b/symbolic_encoding/practical_questions/2_7_symbrep_self.tex @@ -0,0 +1,37 @@ +\item \self Consider the set $\mathbb{N}_{16} = \{0,1,2,3,\dots,14,15\}$. + Let $x_0$, $x_1$, $x_2$, and $x_3$ be propositional variables, + used for symbolic encoding of the elements of $\mathbb{N}_{16}$, + using standard binary encoding, with $x_0$ being the least + significant ($2^0$) bit, and $x_3$ being the most significant + ($2^3$) bit. + + Now, consider the following subsets of $\mathbb{N}_{16}$. + +\begin{itemize} +\item $A = \{0, 1, 2, 3\}$ +\item $B = \{0, 1, 2, 3, 4, 5, 6, 7\}$ +\item $C = \{0, 2, 4, 6, 8, 10, 12, 14\}$ +\item $D = \{8, 10, 12, 14\}$ +\item $E = \{3, 10\}$ +\item $F = \{ \}$ +\end{itemize} + +In the following list of formulas, write the letter of the set that +the formula encodes into the adjacent box. Note that some sets might +be encoded by more than one formula. Also note that some formulas +might not encode any of the above sets; write a ``--'' in the box of +such formulas. + +\begin{itemize} +\item[\Huge{$\square$}] $\bot$ +\item[\Huge{$\square$}] $\top$ +\item[\Huge{$\square$}] $(\neg x_3 \wedge \neg x_2 \wedge x_1 + \wedge x_0) \vee (x_3 \wedge \neg x_2 \wedge x_1 \wedge \neg + x_0)$ +\item[\Huge{$\square$}] $x_0$ +\item[\Huge{$\square$}] $\neg x_0$ +\item[\Huge{$\square$}] $x_3$ +\item[\Huge{$\square$}] $\neg x_3$ +\item[\Huge{$\square$}] $\neg x_3 \vee \neg x_2$ +\item[\Huge{$\square$}] $\neg x_3 \wedge \neg x_2$ +\end{itemize} diff --git a/symbolic_encoding/practical_questions/2_8_symbrep_self.tex b/symbolic_encoding/practical_questions/2_8_symbrep_self.tex new file mode 100644 index 0000000..2b8ff64 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_8_symbrep_self.tex @@ -0,0 +1 @@ +\item \self Given a state space of size $|S| = 2048$, find a symbolic binary encoding for this state space and compute the characteristic function for the sets of states $$B = \{s_0, s_1, s_2, ..., s_{1023}\} \enspace \text{and} \enspace C = \{s_{512}, s_{513},, s_{514}, ..., s_{1535}.\}$$ Then compute the characteristic function for the sets $D = B \cup C$ and $E = B \setminus C$. If possible, simplify the formulas. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex new file mode 100644 index 0000000..465e531 --- /dev/null +++ b/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex @@ -0,0 +1,24 @@ +\item \lect Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \emph{transition system} and +simplify your formulas. Use a binary encoding to encode the states, e.g., +encode the state $s_2$ with the formula $v1 \wedge \neg v_0$. + +\begin{center} +\vspace{-2em} +\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt, +thick,node/.style={circle,draw,minimum size=25pt}] + \node[node] (s0) {$s_0$}; + \node[node] (s1) [right of=s0] {$s_1$}; + \node[node] (s2) [below of=s1] {$s_2$}; + \node[node] (s3) [below of=s0] {$s_3$}; + %\path[<->] (s0) edge (s1); + \path[->] (s0) edge (s2); + \path[<-] (s0) edge (s3); + %\path[<->] (s1) edge (s2); + \path[<->] (s1) edge (s3); + \path[<-] (s2) edge (s3); + \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150); + %\path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); + %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60); + % \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150); +\end{tikzpicture} +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex new file mode 100644 index 0000000..d8af7cc --- /dev/null +++ b/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex @@ -0,0 +1,13 @@ +Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ +\begin{center} + $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ + $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0)$\\ +\end{center} + +We can further simplify the formula to: +\begin{center} + $\lnot v_1 \land \lnot v_0 \land \lnot v'_0 \ \lor$\\ + $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ + $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_0)$\\ +\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_self.tex b/symbolic_encoding/practical_questions/2_9_symbrep_self.tex new file mode 100644 index 0000000..84a036d --- /dev/null +++ b/symbolic_encoding/practical_questions/2_9_symbrep_self.tex @@ -0,0 +1,3 @@ +\item \self Given a state space of size $|S| = 64$. Find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets $$B = \{s_{32}, s_{33}, s_{34}, ..., s_{63}\} \enspace \text{and} \enspace C = \{s_{16}, s_{17},, s_{18}, ..., s_{40}\}.$$ + +Following, compute the formulas that represent the sets $D = B \cap C$, $E = B \cup C$, $F = B \setminus C$ and $G = C \setminus B$. \ No newline at end of file diff --git a/symbolic_encoding/symbolic_encoding.tex b/symbolic_encoding/symbolic_encoding.tex new file mode 100644 index 0000000..77faf69 --- /dev/null +++ b/symbolic_encoding/symbolic_encoding.tex @@ -0,0 +1,128 @@ +\begin{questionSection}{Transition Systems} +\question{symbolic_encoding/0001.tex} + {symbolic_encoding/0001_sol.tex} + {3cm} + +\question{symbolic_encoding/0002.tex} + {symbolic_encoding/0002_sol.tex} + {3cm} +\question{symbolic_encoding/1001.tex} + {no_solution} + {3cm} +\question{symbolic_encoding/1007.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1008.tex} + {no_solution} + {3cm} +\end{questionSection} + + +\begin{questionSection}{Symbolic Encoding} + +\question{symbolic_encoding/0003.tex} + {symbolic_encoding/0003_sol.tex} + {3cm} + +\question{symbolic_encoding/0004.tex} + {symbolic_encoding/0004_sol.tex} + {3cm} + + +\question{symbolic_encoding/0008.tex} + {symbolic_encoding/0008_sol.tex} + {3cm} +\question{symbolic_encoding/1002.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1003.tex} + {no_solution} + {3cm} + + +\question{symbolic_encoding/0005.tex} + {symbolic_encoding/0005_sol.tex} + {3cm} + +\question{symbolic_encoding/0006.tex} + {symbolic_encoding/0006_sol.tex} + {3cm} +\question{symbolic_encoding/1004.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1005.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1006.tex} + {no_solution} + {3cm} + + +\question{symbolic_encoding/1009.tex} + {no_solution} + {3cm} + + +\question{symbolic_encoding/1011.tex} + {no_solution} + {3cm} + + + +\question{symbolic_encoding/1015.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1016.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1017.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1018.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1019.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1020.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1021.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1000.tex} + {no_solution} + {3cm} +\question{symbolic_encoding/1010.tex} + {no_solution} + {3cm} +\question{symbolic_encoding/1012.tex} + {no_solution} + {3cm} + +\question{symbolic_encoding/1013.tex} + {no_solution} + {3cm} +\question{symbolic_encoding/0007.tex} + {symbolic_encoding/0007_sol.tex} + {3cm} + +\end{questionSection} + + + + +%\question{symbolic_encoding/1014.tex} +% {no_solution} +% {3cm} diff --git a/symbolic_encoding/theory_questions/0_1_symb_lect.tex b/symbolic_encoding/theory_questions/0_1_symb_lect.tex new file mode 100644 index 0000000..68acaa3 --- /dev/null +++ b/symbolic_encoding/theory_questions/0_1_symb_lect.tex @@ -0,0 +1 @@ +\item \lect Given the term \textit{state} within a reactive system, what does a \textit{state} do? \underline{rausnehmen?} \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/0_1_symb_self.tex b/symbolic_encoding/theory_questions/0_1_symb_self.tex new file mode 100644 index 0000000..40bc701 --- /dev/null +++ b/symbolic_encoding/theory_questions/0_1_symb_self.tex @@ -0,0 +1 @@ +\item \self Given the term \textit{transition} within a reactive system, what does the term \textit{transition} mean? How can a \textit{transition} be determined? \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/1_0_kripke_self.tex b/symbolic_encoding/theory_questions/1_0_kripke_self.tex new file mode 100644 index 0000000..64df842 --- /dev/null +++ b/symbolic_encoding/theory_questions/1_0_kripke_self.tex @@ -0,0 +1,2 @@ +\item \self + Give the definition of a \emph{transition system} $\mathcal{T}$ and an example. diff --git a/symbolic_encoding/theory_questions/2_01_symbrep_self.tex b/symbolic_encoding/theory_questions/2_01_symbrep_self.tex new file mode 100644 index 0000000..ce68361 --- /dev/null +++ b/symbolic_encoding/theory_questions/2_01_symbrep_self.tex @@ -0,0 +1,3 @@ +\item \self What is the main advantage of symbolic set operations over + non-symbolic operations that enumerate all set elements + explicitly? diff --git a/symbolic_encoding/theory_questions/2_1_symbrep_self.tex b/symbolic_encoding/theory_questions/2_1_symbrep_self.tex new file mode 100644 index 0000000..27de2fb --- /dev/null +++ b/symbolic_encoding/theory_questions/2_1_symbrep_self.tex @@ -0,0 +1 @@ +\item \self Considering the \textit{representation of a single state}, for a given valuation, we can write a formula that is true for exactly that evaluation. How can in contrast the \textit{representation of sets of states} be defined? Give a small example of such a representation. \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/2_2_symbrep_self.tex b/symbolic_encoding/theory_questions/2_2_symbrep_self.tex new file mode 100644 index 0000000..054efd0 --- /dev/null +++ b/symbolic_encoding/theory_questions/2_2_symbrep_self.tex @@ -0,0 +1,4 @@ +\item \self Assume you are given the formulas $a$ and + $b$, which symbolically represent the sets $A$ and $B$, + respectively. Give the formula + $c$, which symbolically represents the set $C= A \setminus B$. diff --git a/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex b/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex new file mode 100644 index 0000000..debc912 --- /dev/null +++ b/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex @@ -0,0 +1 @@ +\item \lect Given a \textit{set of ordered pairs of states}, how can a transition relation of a \textit{transition system} be symbolically represented? Explain which sets of variables you need and give an example of such a representation. \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/2_3_symbrep_self.tex b/symbolic_encoding/theory_questions/2_3_symbrep_self.tex new file mode 100644 index 0000000..115d9de --- /dev/null +++ b/symbolic_encoding/theory_questions/2_3_symbrep_self.tex @@ -0,0 +1,5 @@ +\item \self Assume you are given the formulas $a$ and + $b$, which symbolically represent the sets $A$ and $B$, + respectively. What would you have to check on $a, b$ to test + whether or not $A$ is a strict subset of $B$, i.e., $A \subset + B$?