eth-janishutz/eth-summaries
1
0
Fork 0
mirror of https://github.com/janishutz/eth-summaries.git synced 2026-07-27 21:29:09 +02:00
Code Issues Packages Projects Releases Wiki Activity

[FMFP] Add small remark on modelling

Browse Source
This commit is contained in:
janishutz
2026-07-20 17:19:30 +02:00
parent e7da5ab70e
commit 51da8be172
2 changed files with 2 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
semester4/fmfp/formal-methods-functional-programming-summary.pdf
BIN
View File
Binary file not shown.
semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex
+2 -1
View File
@@ -2,7 +2,8 @@
Many of the tasks here are pretty straight forward, converting IMP into Promela, Many of the tasks here are pretty straight forward, converting IMP into Promela,
and putting an \texttt{assert} (or more) into the \texttt{init} block, to check if the required state is reached. and putting an \texttt{assert} (or more) into the \texttt{init} block, to check if the required state is reached.
Note that for non-determinism, we use Promela conditionals without conditions. \bi{Note} that for non-determinism, we use Promela conditionals without conditions.
This can also be used to simulate all possible combinations / actions that can be taken.
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), 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. then we wait for the processes to terminate using \texttt{\_nr\_pr == 1} and do our assertion.