[FMFP] Notes on LTL

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

@@ -34,6 +34,13 @@ vector v; // using the custom vector type
 mtype msg = ack; // Using the symbolic constant
 
 
+// --- Functions -----------------------------------------------
+// Note that these are not full functions and recursion is not supported!
+inline fun() {
+    // function body goes here
+}
+
+
 // --- Processes -----------------------------------------------
 // Process declarations
 proctype myProc(int p) {

semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex

@@ -1,4 +1,5 @@
 \subsubsection{Linear Temporal Logic}
+\label{sec:ltl-details}
 This is used to formalize LT-properties of traces.
 
 \paragraph{Operators}

semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex

@@ -4,9 +4,19 @@ and putting an \texttt{assert} (or more) into the \texttt{init} block, to check
 
 Note that for non-determinism, we use Promela conditionals without conditions.
 
-For parallelism, we can use the \texttt{run} keyword for a \texttt{proctype}, then we wait for the processes to terminate using
-\texttt{\_nr\_pr == 1} and do our assertion.
+For parallelism, we can use the \texttt{run} keyword for a \texttt{proctype} (rest of syntax is just as with a function in most C-like programming languages),
+then we wait for the processes to terminate using \texttt{\_nr\_pr == 1} and do our assertion.
+
+We can use an \texttt{atomic} block to ensure atomicity.
+
+Promela \bi{does not} support functions, instead, the \texttt{inline} keyword works similarly to macros in \texttt{C},
+they are simply substituted into the code at compile time.
+In some solutions, they use double-dash arrows (\verb|-->|). From testing, it seems that it is also fine to use normal arrows (\verb|->|) and it will still work.
+For completeness, the double-dash arrows are used in if statements with conjuncts or disjuncts.
 
 
 If we are given a text description only however, things get more challenging, as we need to model the properties given there.
 A possible simplification of the process may be to model things one property at a time, then combine them as needed.
+
+To check if something is achievable (i.e. there is a solution to the task), we can use an \texttt{assert false} on the case where we have success
+If there is a way, then the assertion will fail (because it will always fail and is only called if \texttt{success} is true)

semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex

@@ -1,2 +1,27 @@
 \subsubsection{Linear Time Properties (LTL)}
 We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises.
+
+For doing verification of liveness / safety properties using \texttt{spin} and Promela,
+the operators are translated to Promela as follows:
+\verb+[] <> ! && || -> U+ for $\square \Diamond \neg \land \lor \Rightarrow U$, respectively.
+In addition, we have the equality operator as a primitive propositional formula. We have \texttt{p == true} for $p$ in the operators.
+
+Execute \texttt{spin -a file.pml}, followed by \texttt{gcc pan.c} and \texttt{./a.out}.
+
+As a reminder, these are the operators (details in Section~\ref{sec:ltl-details}):
+\begin{itemize}
+    \item Now: $p$ states that the proposition is true ``\textit{now}''
+    \item Holds until: $\Phi U \Psi$ states that $\Phi$ holds (with no other valid proposition holding between) until $\Psi$ holds.
+    \item Next: $\bigcirc \Phi$ states that $\Phi$ holds for the ``next''
+    \item Eventually: $\Diamond \Phi$ states that $\Phi$ holds \textit{eventually}, $\Diamond \Phi \equiv (\texttt{true} U \Phi)$
+    \item Always (from now on): $\square \Phi$ states that from now on, $\Phi$ will always hold, $\square \Phi \equiv \neg \Diamond \neg \Phi$
+\end{itemize}
+For the implication (where the left hand side is called the \textit{antecedent}, right hand side is called the \textit{consequent}),
+remember to show the case where the antecedent is true and state that for antecedent false, it is trivially true
+
+Another important remark is that you can't just write $\Diamond \neg s_1$, where $s_1$ is a state, you need to specify the propositions.
+
+
+\subparagraph{Liveness and Safety Properties}
+Proofs here run using the definitions directly, either by showing a counter example (for disproving) or showing that, in fact, the definition holds.
+Indirect proofs may also come in handy, because it is typically easier to show that something is not a safety property (or liveness property) that to show that it is.