[FMFP] Modelling

semester4/fmfp/code/promela/00_basics.pml

@@ -0,0 +1,53 @@
+// --- Constants -----------------------------------------------
+// As C preprocessor macros
+#define N 5
+
+// Symbolic constant
+mtype = { ack, req };
+
+
+// --- Typedef -------------------------------------------------
+// Structure declarations
+typedef vector { int x; int y };
+
+
+// --- Channels ------------------------------------------------
+// Channels are used to exchange messages between processes
+chan buf = [2] of { int }; // can store up to 2 integers
+chan buf2 = [2] of { mtype, bit, chan }; // Messages are Triples
+chan channel = [0] of { int }; // No buffer
+chan unassigned_chan; // This channel is unassigned
+
+
+// --- Variables -----------------------------------------------
+// Note that there are no floats and unbounded integers.
+// Variables are initialized to 0 (ish) values
+// If defined outside a process, they are global, if inside,
+// they are scoped to said process
+bit bit_val; // 1 bit
+bool bool_val; // Equivalent to bit, also 1 bit
+byte counter; // 1 byte (0...255)
+short short_val; // 2 bytes (-2^15 ... 2^15 - 1)
+int val; // 4 bytes
+int arr[4]; // 16 bytes, array of four integers
+vector v; // using the custom vector type
+mtype msg = ack; // Using the symbolic constant
+
+
+// --- Processes -----------------------------------------------
+// Process declarations
+proctype myProc(int p) {
+    // Like the init body, any promela statements go in here
+    // This includes any variable or channel declarations
+    printf("My process");
+}
+
+active [N] proctype myActiveProc(int p) {
+    // Body goes here
+}
+
+
+// --- Initial state -------------------------------------------
+init {
+    printf("Hello World");
+}

semester4/fmfp/formal-methods-functional-programming-summary.tex

@@ -135,6 +135,9 @@
 \section{Modelling}
 \input{parts/04_modelling/00_intro.tex}
 \input{parts/04_modelling/01_promela/00_syntax.tex}
+\input{parts/04_modelling/01_promela/01_expressions.tex}
+\input{parts/04_modelling/01_promela/02_statements.tex}
+\input{parts/04_modelling/01_promela/03_macros.tex}
 % \input{parts/04_modelling/01_promela/}
 % \input{parts/04_modelling/}
 

semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex

@@ -1,2 +1,17 @@
 \subsection{Promela}
-% p23
+Promela has \texttt{C}-like syntax, and its main objects are processes, channels, and variables.
+
+An important consideration always is the number of states there are for each model, if spin can complete executing.
+
+The number of states is given by
+\[
+    \prod_{i = 1}^N (l(p_i) \times \prod_{\texttt{var} x_i \in p_i} |\texttt{dom}(x_i)|) \times \prod_{j = 1}^{K} |\texttt{dom}(c_j)|^{\texttt{cap}(c_j)}
+\]
+where $l(p_i)$ returns the number of program locations for process $i$, $|\texttt{dom}(x_i)|$ denotes the number of values a variable can take,
+$\texttt{dom}(c_j)$ denotes the number of values each message in the channel can take and $\texttt{cap}(c_j)$ returns the capacity of the buffer fo the channel.
+
+\shade{orange}{THUS:} \hl{Keep the model as small as possible} to prevent the above, which is called \bi{state space explosion}
+
+\newpage
+
+\inputcode{promela}{code/promela/00_basics.pml}

semester4/fmfp/parts/04_modelling/01_promela/01_expressions.tex

@@ -0,0 +1,23 @@
+\subsubsection{Expressions}
+Expressions in Promela can be:
+\begin{itemize}
+    \item Variables, constants, and literals
+    \item Structure and array accesses
+    \item Unary and binary expressions with operators. The operators correspond to the \texttt{C} operators
+    \item Function applications
+    \item Ternary operators / conditional expressions \texttt{E1 -> E2 : E3}
+\end{itemize}
+Promela has a number of built in functions, which are:
+\begin{multicols}{5}
+    \begin{itemize}
+        \item \texttt{len()}
+        \item \texttt{empty()}
+        \item \texttt{nempty()}
+        \item \texttt{full()}
+        \item \texttt{nfull()}
+        \item \texttt{run <proc>}
+        \item \texttt{eval()}
+        \item \texttt{enabled()}
+        \item \texttt{pcvalue()}
+    \end{itemize}
+\end{multicols}

semester4/fmfp/parts/04_modelling/01_promela/02_statements.tex

@@ -0,0 +1,26 @@
+\subsubsection{Statements}
+The following statement types are supported by Promela:
+\begin{itemize}
+    \item \texttt{skip}: Does not change the state (except the location counter). Always executable
+    \item \texttt{assert(E)}: Aborts execution if \texttt{E} evaluates to zero, otherwise is equivalent to \texttt{skip}. Always executable
+    \item Assignment: \texttt{x = E} assigns value of \texttt{E} to variable \texttt{x}. For arrays, use \texttt{a[n] = E}. Always executable
+    \item \texttt{s1;s2} (Sequential composition): Executable if \texttt{s1} is executable
+    \item Expression statement: Evaluates expression \texttt{E}, executable if \texttt{E} evaluates $\neq 0$. \texttt{E} must be \bi{side effect free}.
+\end{itemize}
+
+In addition, selection statements (i.e. if / switch) and repetitions (loops) are supported:
+\begin{code}{promela}
+    if
+    :: s1 -> code;
+    :: s2 -> code;
+    :: code; // The else statement, executes if no other option executable
+    fi
+
+    do
+    :: s1 -> loop_body_1; // We can use this technique to combine if and loops
+    :: s2 -> loop_body_2;
+    :: else -> break;
+    od
+\end{code}
+
+Then, we have atomic statements, which has signature \texttt{atomic \{ s \}}, which executes \texttt{s} atomically.

semester4/fmfp/parts/04_modelling/01_promela/03_macros.tex

@@ -0,0 +1,5 @@
+\subsubsection{Macros}
+Promela does \textit{not} support procedures. However, many of the effects (apart from recursion) can be achieved with macros.
+
+We define them using \mint{promela}|inline name(arg1, arg2) { /* body */ }|
+As is the case in \texttt{C}, they are simply replaced in the code and thus have no new variable scope, support no recursion and have no return value.