Plot included in report

.gitignore

@@ -2,4 +2,305 @@ Examples
 **/pan.*
 **/pan
 *.tmp
-/ReversalModel/reversal.pml
+/ReversalModel/reversal.pml## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+
+## Build tool directories for auxiliary files
+# latexrun
+latex.out/
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# comment
+*.cut
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+*.lzo
+*.lzs
+*.slg
+*.slo
+*.sls
+
+# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+# *.ist
+
+# gnuplot
+*.gnuplot
+*.table
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.glog
+*.gtex
+
+# htlatex
+*.4ct
+*.4tc
+*.idv
+*.lg
+*.trc
+*.xref
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files
+# *.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# luatexja-ruby
+*.ltjruby
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# newpax
+*.newpax
+
+# nomencl
+*.nlg
+*.nlo
+*.nls
+
+# pax
+*.pax
+
+# pdfpcnotes
+*.pdfpc
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# svg
+svg-inkscape/
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# tcolorbox
+*.listing
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# titletoc
+*.ptc
+
+# todonotes
+*.tdo
+
+# vhistory
+*.hst
+*.ver
+
+# easy-todo
+*.lod
+
+# xcolor
+*.xcp
+
+# xmpincl
+*.xmpi
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices and outlines
+*.xyc
+*.xyd
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# LyX
+*.lyx~
+
+# Kile
+*.backup
+
+# gummi
+.*.swp
+
+# KBibTeX
+*~[0-9]*
+
+# TeXnicCenter
+*.tps
+
+# auto folder when using emacs and auctex
+./auto/*
+*.el
+
+# expex forward references with \gathertags
+*-tags.tex
+
+# standalone packages
+*.sta
+
+# Makeindex log files
+*.lpz
+
+# xwatermark package
+*.xwm
+
+# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib
+# option is specified. Footnotes are the stored in a file with suffix Notes.bib.
+# Uncomment the next line to have this generated file ignored.
+#*Notes.bib
+

ReversalModel/make_plots.py

@@ -3,17 +3,19 @@ import pandas as pd
 import seaborn as sns
 import matplotlib.pyplot as plt
 import matplotlib
+import os
 
+DIR: str = os.path.dirname(__file__) 
 
-matplotlib.use("pgf")
+matplotlib.use('pgf')
 matplotlib.rcParams.update({
-    "pgf.texsystem": "pdflatex",
+    'pgf.texsystem': 'pdflatex',
     'font.family': 'serif',
     'text.usetex': True,
     'pgf.rcfonts': False,
 })
 
-df = pd.read_csv("time.csv")
+df = pd.read_csv(DIR + '/time.csv')
 df['cpu'] = df['user'] + df['sys']
 del df['real']
 del df['user']
@@ -41,20 +43,20 @@ def timeout_by(name: str) -> pd.DataFrame:
 
 def plot_by(df_cpu: pd.DataFrame, name: str, color: any): 
     # Initialize the matplotlib figure
-    f, (ax1, ax2) = plt.subplots(1, 2, figsize=(15, 5))
+    f, (ax1, ax2) = plt.subplots(1, 2, figsize=(8, 4))
 
     sns.stripplot(ax=ax1, color=color, data=df_cpu.loc[df_cpu.variable == name],
-                  x="cpu", y="value")
+                  x='cpu', y='value')
-    sns.barplot(ax=ax2, color=color, data=timeout_by(name), y=name, x="timeout",
+    sns.barplot(ax=ax2, color=color, data=timeout_by(name), y=name, x='timeout',
                 width=0.75)
 
-    ax1.set(ylabel="Value of " + name.upper(), xlim=[0, 300],
+    ax1.set(ylabel='Value of ' + name.upper(), xlim=[0, 300],
-            xlabel="CPU time (seconds)")
+            xlabel='CPU time (seconds)')
-    ax2.set(ylabel="Value of " + name.upper(), xlim=[0, 100], 
+    ax2.set(ylabel='Value of ' + name.upper(), xlim=[0, 100], 
-            xlabel="Timeouts (%)")
+            xlabel='Timeouts (%)')
     
     sns.despine(left=True, bottom=True)
-    plt.savefig('../plots/' + name + '.pgf')
+    plt.savefig(DIR + '/../plots/' + name + '.pgf')
 
 
 def main():

report.tex

@@ -0,0 +1,95 @@
+\documentclass[11pt,a4paper]{scrartcl}
+\usepackage{algorithm}
+\usepackage{algpseudocode}
+\usepackage[utf8]{inputenc}
+\usepackage[margin=2.25cm]{geometry}
+\usepackage{hyperref}
+\usepackage{listings}
+\usepackage{xcolor}
+\usepackage{lmodern}
+\usepackage{booktabs}
+\usepackage{multirow}
+\usepackage{graphicx}
+\usepackage{float}
+\usepackage{multicol}
+\usepackage{tikz}
+\usepackage{listings}
+\usepackage{pgfplots}
+\pgfplotsset{compat=1.18}
+\usepackage{subcaption}
+\setlength{\parindent}{0cm}
+\setlength{\parskip}{0.3em}
+\hypersetup{pdfborder={0 0 0}}
+%\usepackage[nomessages]{fp} no easter eggs this time
+\usepackage{amsmath}
+\DeclareMathOperator*{\argmax}{arg\,max}
+\DeclareMathOperator*{\argmin}{arg\,min}
+\usepackage{minted}
+
+\definecolor{codegreen}{rgb}{0,0.6,0}
+\definecolor{codegray}{rgb}{0.5,0.5,0.5}
+\definecolor{codepurple}{rgb}{0.58,0,0.82}
+\definecolor{backcolour}{rgb}{0.95,0.95,0.92}
+
+\lstdefinestyle{mystyle}{
+  backgroundcolor=\color{backcolour},   
+  commentstyle=\color{codegreen},
+  keywordstyle=\color{magenta},
+  keywordstyle=[2]{\color{olive}},
+  numberstyle=\tiny\color{codegray},
+  stringstyle=\color{codepurple},
+  basicstyle=\ttfamily\footnotesize,
+  breakatwhitespace=false,         
+  breaklines=true,                 
+  captionpos=b,  
+  keepspaces=true,                 
+  numbers=left,  
+  numbersep=5pt,
+  showspaces=false,                
+  showstringspaces=false,
+  showtabs=false,
+  tabsize=2,
+  aboveskip=0.8em,
+  belowcaptionskip=0.8em
+}
+\lstset{style=mystyle}
+
+\geometry{left=2cm,right=2cm,top=2cm,bottom=3cm}
+\title{
+\vspace{-5ex} 
+Assignment 4 -- Software Analysis \\\vspace{0.5cm}
+\Large Model checking with Spin
+\vspace{-1ex} 
+}
+\author{Claudio Maggioni}
+\date{\vspace{-3ex}}
+
+\begin{document}
+\maketitle
+
+\begin{figure}
+\begin{subfigure}[t]{\linewidth}
+\centering
+\resizebox{0.85\textwidth}{!}{\input{plots/n.pgf}}
+\caption{Variable \texttt{N}}
+\end{subfigure}
+\begin{subfigure}[t]{\linewidth}
+\centering
+\resizebox{0.85\textwidth}{!}{\input{plots/length.pgf}}
+\caption{Variable \texttt{LENGTH}}
+\end{subfigure}
+\begin{subfigure}[t]{\linewidth}
+\centering
+\resizebox{0.85\textwidth}{!}{\input{plots/r.pgf}}
+\caption{Variable \texttt{R}}
+\end{subfigure}
+
+    \caption{Distribution of CPU time and percentage of timeouts (i.e.\
+    executions with a real execution time greater than 5 minutes, discarded for
+    sake of time) for different executions of the model checker for different
+    parameters of \texttt{N}, \texttt{LENGTH} and \texttt{R}.}
+\label{fig:bigplot}
+\end{figure}
+
+\end{document}
+