\documentclass{article}
%\usepackage{times}
\usepackage[utf8]{inputenc}

%\usepackage{amsthm}
\usepackage{algorithm} % for pseudo-codes
%\usepackage{enumerate}
\usepackage{algpseudocode}
%\usepackage{DotArrow}
%\usepackage{subfig}
%\usepackage{amsmath, environ}
%\usepackage{amssymb}
%\usepackage{amsthm}
%%\usepackage{bm}
%%\usepackage{mathtools}
\usepackage{graphicx} 
%\usepackage{wrapfig}
%\usepackage{minibox}
%\usepackage{multirow}
%\usepackage{pifont} % \ding{}
%\usepackage[percent]{overpic}
%\usepackage{scrextend} % labeling environment
%
%\newtheorem{theorem}{Theorem}
%\newtheorem{definition}{Definition}
%\newtheorem{example}{Example}
%
%\renewcommand{\textfraction}{0.05}
%\renewcommand{\floatpagefraction}{0.75}
\usepackage{listings}
\usepackage{color}

\definecolor{dkgreen}{rgb}{0,0.6,0}
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{mauve}{rgb}{0.58,0,0.82}

\lstset{frame=tb,
  %language=NuSmv,
  aboveskip=3mm,
  belowskip=3mm,
  showstringspaces=false,
  columns=flexible,
  basicstyle={\small\ttfamily},
  numbers=none,
  numberstyle=\tiny\color{gray},
  keywordstyle=\color{blue},
  commentstyle=\color{dkgreen},
  stringstyle=\color{mauve},
  breaklines=true,
  breakatwhitespace=true,
  tabsize=3
}

\newcommand{\centerimage}[5][-7pt]{ % [vskip] | graphics-opt | imgname | label | caption
\begin{figure}[!htb]%
\centering%
\vspace{#1}%
\includegraphics[#2]{#3}%
\caption{#5}\label{#4}\vspace{2mm}%
%\vspace{-3pt}\caption{#5}\label{#4}\vspace{-2pt}%
\end{figure}}
\date{}

%\includegraphics[trim=1cm 2cm 3cm 4cm, clip=true]{example.pdf}



\begin{document}



\title{Relazione Esercizio Model Checking}


\author{Francesco Gallà, francesco.galla@edu.unito.it}

\maketitle


%========================================================================= 
%%%%%%%                       INTRODUCTION                         %%%%%%%
%========================================================================= 

\section{Descrizione}  \label{sec:Descrizione}

Di seguito viene effettuata la valutazione di correttezza per alcuni algoritmi di mutua
esclusione, mostrati in ordine di complessit\`a. Per ognuno si mostrano il modello in NuSMV,
GreatSPN e algebra dei processi. In ogni modello sono state controllate le tre propriet\`a
essenziali, qui riportate:

\begin{description}
    \item{1.} Mutua esclusione
    \item{2.} Assenza di Deadlock
    \item{3.} Assenza di Starvation Individuale
\end{description}

%=========================================================================================================
\section{Esercizio 3.2}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{32-testo.jpg}{img:32-testo}
    {Descrizione dell'algoritmo}
\break
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
    \item{2.} AG (p.state = enter $->$ AF (p.state = critical $|$ q.state = critical))
        \textbf{False}
    \item{3.} AG (p.state = enter $->$ AF p.state = critical) \textbf{False}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
in linguaggio LTL sono riportate di seguito.}

\subsection{NuSMV}

Il modello NuSMV implementa l'algoritmo pi\`u triviale per la mutua esclusione, ossia
l'alternanza di due processi sull'accesso a una sezione critica in base a una variabile
booleana $turn$.
Sono stati utilizzati 4 stati, di cui:

\begin{description}
    \item{$local$: } Rappresenta l'esecuzione non critica e non forza il progresso
    \item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $turn$
    \item{$critical$: } Rappresenta la sezione critica
    \item{$exit$: } Cambia il valore di $turn$ per garantire l'accesso all'altro processo ed
        esce dalla SC.
\end{description}
\newpage
\begin{lstlisting}
MODULE main
VAR
  turn : 1..2;
  p : process user(turn, 1, 2);
  q : process user(turn, 2, 1);
ASSIGN
  init(turn) := 1;
SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = enter -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = enter -> AF p.state = critical)

MODULE user(turnloc, myproc, otherproc)
VAR
  state : {local,enter,critical,exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, enter};
      state = enter & turnloc = myproc : critical;
      state = critical : exit;
      state = exit : local;
      TRUE : state;
    esac;
  next(turnloc) :=
    case
      state = exit : otherproc;
      TRUE : turnloc;
    esac;
FAIRNESS
  running
\end{lstlisting}
Il modello NuSmv model per l'algoritmo $3.2$.

\newpage

\subsection{Rete di Petri}

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete32.jpg}{img:rete32}
    {Modello P/T della rete 3.2}


% ---- PROPRIETA`
\subsection{Mutua Esclusione}

\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P3 == 1 && #Q3 == 1)
\end{lstlisting}
\break

La mutua esclusione \`e rispettata sia in NuSMV che in GreatSPN, in quanto non esiste un
caso in cui entrambi i processi siano contemporaneamente nella sezione critica.
\`E anche vero per\`o che i processi si aspettano a vicenda nella fase di $enter$,
pertanto il loro accesso sar\`a per forza alternato.

\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P2 == 1 -> AF ( #P3 == 1 || #Q3 == 1))
\end{lstlisting}

La propriet\`a di assenza di deadlock non pu\`o essere rispettata in quanto i processi si
aspettano a vicenda nella fase di $enter$. Essendo inoltre che i processi nella fase $local$
non sono obbligati al progresso, se un processo resta in local indefinitamente non permette
il proseguimento dell'altro.
\break
Infatti, solo nel caso in cui entrambi i processi richiedono la sezione critica, e quindi
sono entrambi nella fase $enter$, si evita il deadlock.
\break
\break
Di seguito si riporta il controesempio alla propriet\`a.
\begin{lstlisting}
-- specification AG (p.state = enter -> AF (p.state = critical | q.state = critical))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    turn = 1
    p.state = local
    q.state = local
  -> Input: 1.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 1.2 <-
    p.state = enter
  -> Input: 1.3 <-
  -> State: 1.3 <-
    p.state = critical
  -> Input: 1.4 <-
  -> State: 1.4 <-
    p.state = exit
  -> Input: 1.5 <-
  -> State: 1.5 <-
    turn = 2
    p.state = local
  -> Input: 1.6 <-
  -- Loop starts here
  -> State: 1.6 <-
    p.state = enter
  -> Input: 1.7 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 1.7 <-
  -> Input: 1.8 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 1.8 <-
  -> Input: 1.9 <-
    _process_selector_ = main
    running = TRUE
    p.running = FALSE
  -> State: 1.9 <-
\end{lstlisting}
Il controesempio fornito da NuSmv per la propriet\`a $2$.
\break
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete32-2.jpg}{img:rete32-2}
    {Controesempio fornito da GreatSPN per la propriet\`a $2$.}

\newpage

\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
  AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
  G (p.state = enter -> F (p.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P2 == 1 -> AF ( #P3 == 1 ))
\end{lstlisting}
\break
L'assenza di starvation individuale non \`e rispettata in quanto la propriet\`a di assenza di deadlock non lo \`e.
Di seguito si riporta il controesempio alla propriet\`a.
\break
\begin{lstlisting}
-- specification AG (p.state = enter -> AF p.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 2.1 <-
    turn = 1
    p.state = local
    q.state = local
  -> Input: 2.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 2.2 <-
    p.state = enter
  -> Input: 2.3 <-
  -> State: 2.3 <-
    p.state = critical
  -> Input: 2.4 <-
  -> State: 2.4 <-
    p.state = exit
  -> Input: 2.5 <-
  -> State: 2.5 <-
    turn = 2
    p.state = local
  -> Input: 2.6 <-
  -- Loop starts here
  -> State: 2.6 <-
    p.state = enter
  -> Input: 2.7 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 2.7 <-
  -> Input: 2.8 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 2.8 <-
  -> Input: 2.9 <-
    _process_selector_ = main
    running = TRUE
    p.running = FALSE
  -> State: 2.9 <-
\end{lstlisting}
Il controesempio fornito da NuSmv per la propriet\`a $3$.
\break
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete32-3.jpg}{img:rete32-3}
    {Controesempio fornito da GreatSPN per la propriet\`a $3$.}

\newpage
\subsection{Algebra dei Processi}

Si presenta un modello in algebra dei processi per l'algoritmo $3.2$. La nomenclatura vuole
richiamare i posti e le transizioni definiti nella rete P/T, per agevolare il confronto tra
il Derivation Graph in CCS e il Reachability Graph in GreatSPN.
\break
\break
Come si nota, il DG e il RG hanno lo stesso numero di nodi e archi corrispondenti.
Per questo possiamo affermare l'equivalenza del modello CCS con il modello P/T.

\begin{lstlisting}
Actions = {isTurnP, isTurnQ, setP, setQ, locP, locQ, criticalP, criticalQ}

TurnP = setP.TurnP + setQ.TurnQ + isTurnP.TurnP
TurnQ = setQ.TurnQ + setP.TurnP + isTurnQ.TurnQ

P1 = locP.P1 + locP.P2
P2 = [isTurnP].P3
P3 = criticalP.P4
P4 = [setQ].P1

Q1 = locQ.Q1 + locQ.Q2
Q2 = [isTurnQ].Q3
Q3 = criticalP.Q4
Q4 = [setP].Q1

Sync = {isTurnP, isTurnQ, setP, setQ}
Sys = {(P1 || Q1) || TurnP} / Sync

\end{lstlisting}
Modello CCS per l'algoritmo 3.2.
\textit{Nota: un'azione contornata da '[]' \`e considerata un'azione in output, tutte le altre
sono considerate in input.}

\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{dg.pdf}{img:32dg}
    {Derivation Graph per la rete 3.2}

\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{32rg.pdf}{img:32rg}
    {Reachability Graph di GreatSPN per la rete 3.2}

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.5}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{35-testo.jpg}{img:35-testo}
    {Descrizione dell'algoritmo}

I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = exit \& q.state = exit) \textbf{True}
    \item{2.} AG (p.state = enter $->$ AF (p.state = exit $|$ q.state = exit))
        \textbf{False}
    \item{3.} AG (p.state = enter $->$ AF p.state = exit) \textbf{False}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}

\subsection{NuSMV}

Il modello NuSMV implementa l'algoritmo semplificato per la mutua esclusione, ossia
l'alternanza di due processi sull'accesso a una sezione critica in base a una variabile
booleana $turn$.
Sono stati utilizzati 2 stati, di cui:

\begin{description}
    \item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $turn$. In
        questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
        tempo indefinito.
    \item{$exit$: } Cambia il valore di $turn$ per garantire l'accesso all'altro processo e
        ritorna a $enter$.
\end{description}

Questo modello si presenta come una versione semplificata dell'algoritmo $3.2$ (sono infatti
stati rimossi gli stati di sezione non critica e critica, mantenendo solo la richiesta in
$enter$ e il passaggio del turno in $exit$). Pertanto, i risultati sono gli stessi: la
mutua esclusione \`e rispettata, mentre l'assenza di deadlock e di starvation individuale
non lo sono.
Anche in questo caso i processi hanno un'alternanza all'accesso forzata dall'assegnazione in
$exit$ del turno al processo opposto dopo ogni accesso alla SC.
\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN. Le tracce di esecuzione sono simili
all'esercizio $3.2$.

\newpage
\begin{lstlisting}
MODULE main
VAR
  turn : 1..2;
  p : process user(turn, 1, 2); 
  q : process user(turn, 2, 1); 
ASSIGN
  init(turn) := 1;
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = exit & q.state = exit)
SPEC -- DEADLOCK
  AG (p.state = enter -> AF (p.state = exit | q.state = exit))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = enter -> AF p.state = exit)

MODULE user(turnloc, myproc, otherproc)
VAR
  state : {enter,exit};
ASSIGN
  init(state) := enter;
  next(state) :=
    case
      state = enter & turnloc = myproc : {enter,exit};
      state = exit : enter;
      TRUE : state;
    esac;
  next(turnloc) :=
    case
      state = exit : otherproc;
      TRUE : turnloc;
    esac;
FAIRNESS
  running
\end{lstlisting}
Il modello NuSmv model per l'algoritmo $3.5$.

\newpage

\subsection{Rete di Petri}

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete35.jpg}{img:rete35}
    {Modello P/T della rete 3.5}


% ---- PROPRIETA`

\newpage
\subsection{Algebra dei Processi}

Si presenta un modello in algebra dei processi per l'algoritmo $3.5$. La nomenclatura vuole
richiamare i posti e le transizioni definiti nella rete P/T, per agevolare il confronto tra
il Derivation Graph in CCS e il Reachability Graph in GreatSPN.
\break
\break
Come si nota, il DG e il RG hanno lo stesso numero di nodi e archi corrispondenti.
Per questo possiamo affermare l'equivalenza del modello CCS con il modello P/T.

\begin{lstlisting}
Actions = {isTurnP, isTurnQ, setP, setQ, waitP, waitQ}

TurnP = setP.TurnP + setQ.TurnQ + isTurnP.TurnP
TurnQ = setQ.TurnQ + setP.TurnP + isTurnQ.TurnQ

P1 = [isTurnP].P2 + waitP.P1
P2 = [setQ].P1

Q1 = [isTurnQ].Q2 + waitQ.Q1
Q2 = [setP].Q1


Sync = {isTurnP, isTurnQ, setP, setQ}
Sys = {(P1 || Q1) || TurnP} / Sync

\end{lstlisting}
Modello CCS per l'algoritmo 3.5.
\textit{Nota: un'azione contornata da '[]' \`e considerata un'azione in output, tutte le altre
sono considerate in input.}

\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{35dg.pdf}{img:35dg}
    {Derivation Graph per la rete 3.5}

\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{35rg.pdf}{img:35rg}
    {Reachability Graph di GreatSPN per la rete 3.5}


%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.6}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{36-testo.jpg}{img:36-testo}
    {Descrizione dell'algoritmo}

I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = critical \& q.state = critical) \textbf{False}
    \item{2.} AG (p.state = enter $->$ AF (p.state = critical $|$ q.state = critical))
        \textbf{True}
    \item{3.} AG (p.state = enter $->$ AF p.state = critical) \textbf{False}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}

\subsection{NuSMV}

Il modello NuSMV implementa il primo algoritmo per la mutua esclusione basato su due
variabili anzich\`e una condivisa.
Sono stati utilizzati 5 stati, di cui:

\begin{description}
    \item{$local$: } Sezione non critica.
    \item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $want$ opposta. In
        questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
        tempo indefinito.
    \item{$set$: } Ottenuto l'accesso, assegna alla variabile il valore $TRUE$.
    \item{$critical$: } Sezione critica.
    \item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}

Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.

\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN.

\newpage
\begin{lstlisting}
MODULE main
VAR
  wp : boolean;
  wq : boolean;
  p : process user(wp,wq); 
  q : process user(wq,wp); 
ASSIGN
  init(wp) := FALSE;
  init(wq) := FALSE;

SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = enter -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = enter -> AF p.state = critical)

MODULE user(wp, wq) 
VAR
  state : {local,enter,set,critical,exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, enter};
      state = enter & wq = FALSE : set;
      state = set : critical;
      state = critical : exit;
      state = exit : local;
      TRUE : state;
    esac;
  next(wp) :=
    case
      state = set : TRUE;
      state = exit : FALSE;
      TRUE : wp; 
    esac;
FAIRNESS
  running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.6$.
\newpage

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete36.jpg}{img:rete36}
    {Modello GreatSPN per l'algoritmo $3.6$}

% ---- PROPRIETA`
\subsection{Mutua Esclusione}

\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break

La mutua esclusione non \`e rispettata dall'algoritmo $3.6$, come si vede dall'esecuzione di
controesempio di NuSmv e GreatSPN. Se i due processi si trovano entrambi in stato di $enter$:
$wantp == wantq == FALSE$, pertanto \`e possibile che riescano entrambi a passare in stato di $set$.

Si riportano di seguito i controesempi.

\begin{lstlisting}
specification AG !(p.state = critical & q.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 1.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 1.2 <-
    p.state = enter
  -> Input: 1.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.3 <-
    q.state = enter
  -> Input: 1.4 <-
  -> State: 1.4 <-
    q.state = set
  -> Input: 1.5 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.5 <-
    p.state = set
  -> Input: 1.6 <-
  -> State: 1.6 <-
    wp = TRUE
    p.state = critical
  -> Input: 1.7 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.7 <-
    wq = TRUE
    q.state = critical
\end{lstlisting}
\newpage

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete36-1.jpg}{img:rete36-1}
    {Controesempio per la mutua esclusione di GreatSPN.}
\newpage
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}

La propriet\a` di assenza di deadlock \`e vera nel caso di NuSmv, in quanto non \`e possibile
che un processo rimanga in attesa in $enter$ per un tempo indefinito: se l'altro processo
entra, dovr\`a per forza uscire e cambiare il valore di $want$, altrimenti la variabile $want$
gli permette l'accesso a $set$.
\break
\break
In GreatSPN, la propriet\`a risulta invece falsa, in quanto \`e possibile che un processo
entri in $P1$ (attesa) ma l'altro esegua continuamente la transizione di non progresso.
Possiamo forzare questa propriet\`a estendendo la definizione di assenza di deadlock,
utilizzando quindi la seguente formula CTL:
\begin{lstlisting}
AG (#P1 == 1 -> EF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
Che viene valutata \textbf{True}.

\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
  AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
  G (p.state = enter -> F (p.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}
\break

L'assenza starvation individuale non \`e rispettata n\`e in NuSmv n\`e in GreatSPN. Questo
perch\`e \`e possibile che uno dei due processi continui ad accedere alla sezione critica
senza permettere all'altro di fare lo stesso.

\begin{lstlisting}
-- specification AG (p.state = enter -> AF p.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 2.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 2.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 2.2 <-
    p.state = enter
  -> Input: 2.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.3 <-
    q.state = enter
  -> Input: 2.4 <-
  -> State: 2.4 <-
    q.state = set
  -> Input: 2.5 <-
  -> State: 2.5 <-
    wq = TRUE
    q.state = critical
  -> Input: 2.6 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 2.6 <-
  -> Input: 2.7 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.7 <-
    q.state = exit
  -> Input: 2.8 <-
  -> State: 2.8 <-
    wq = FALSE
    q.state = local
\end{lstlisting}
    \centerimage{width=\columnwidth}
{rete36-3.jpg}{img:rete36-3}
    {Controesempio per la starvation individuale di GreatSPN.}

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.8}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{38-testo.jpg}{img:38-testo}
    {Descrizione dell'algoritmo}

I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
    \item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
        \textbf{False}
    \item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{False}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}

\subsection{NuSMV}

Il secondo algoritmo di mutua esclusione basato su due variabili \`e simile al $3.6$ ma
inverte gli stati $set$ e $enter$, di modo da segnalare la sua intenzione di entrare nella
sezione critica prima di mettersi in attesa.
Sono stati utilizzati 5 stati, di cui:

\begin{description}
    \item{$local$: } Sezione non critica.
    \item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
    \item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $want$ opposta. In
        questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
        tempo indefinito.
    \item{$critical$: } Sezione critica.
    \item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}

Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.

\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN.

\begin{lstlisting}
MODULE main
VAR
  wp : boolean;
  wq : boolean;
  p : process user(wp,wq);
  q : process user(wq,wp);
ASSIGN
  init(wp) := FALSE;
  init(wq) := FALSE;

SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = set -> AF p.state = critical)

MODULE user(wp, wq) 
VAR
  state : {local,set,enter,critical,exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, set};
      state = set : enter;
      state = enter & wq = FALSE : critical;
      state = critical : exit;
      state = exit : local;
      TRUE : state;
    esac;
  next(wp) :=
    case
      state = set : TRUE;
      state = exit : FALSE;
      TRUE : wp; 
    esac;
FAIRNESS
  running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.8$.
\newpage

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete38.jpg}{img:rete38}
    {Modello GreatSPN per l'algoritmo $3.8$}

% ---- PROPRIETA`
\subsection{Mutua Esclusione}

\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
La mutua esclusione \`e rispettata in quanto la modifica della variabile $want$ viene
effettuata prima della fase di controllo. Questo permette di evitare il caso, presente
nell'esercizio $3.6$, in cui l'esecuzione interfogliata dei due processi portava all'accesso
di entrambi nella sezione critica.

\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}

L'assenza di deadlock non \`e rispettata n\`e in NuSmv ne in GreatSPN, in quanto se entrambi
i processi eseguono $set$, entrambe le variabili $want$ avranno valore $TRUE$ non permettendo
il progresso di nessuno dei due.
Si riportano i controesempi.

\begin{lstlisting}
-- specification AG (p.state = set -> AF (p.state = critical | q.state = critical))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 1.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 1.2 <-
    p.state = set
  -> Input: 1.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.3 <-
    q.state = set
  -> Input: 1.4 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.4 <-
    wp = TRUE
    p.state = enter
  -> Input: 1.5 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 1.5 <-
    wq = TRUE
    q.state = enter
  -> Input: 1.6 <-
  -- Loop starts here
  -> State: 1.6 <-
  -> Input: 1.7 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 1.7 <-
  -> Input: 1.8 <-
    _process_selector_ = main
    running = TRUE
    p.running = FALSE
  -> State: 1.8 <-
\end{lstlisting}
Controesempio di NuSmv per l'assenza di deadlock dell'esercizio $3.8$.
\newpage
    \centerimage{width=\columnwidth}
{rete38-2.jpg}{img:rete38-2}
    {Controesempio per l'assenza di deadlock di GreatSPN.}

\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
  AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
  G (p.state = enter -> F (p.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}

Essendo che la propriet\`a di assenza di deadlock \`e falsa, \`e lecito che anche quella di
starvation individuale lo sia. Si riportano i controesempi.

\begin{lstlisting}
-- specification AG (p.state = set -> AF p.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 2.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 2.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 2.2 <-
    p.state = set
  -> Input: 2.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.3 <-
    q.state = set
  -> Input: 2.4 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 2.4 <-
    wp = TRUE
    p.state = enter
  -> Input: 2.5 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 2.5 <-
    wq = TRUE
    q.state = enter
  -> Input: 2.6 <-
  -- Loop starts here
  -> State: 2.6 <-
  -> Input: 2.7 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 2.7 <-
  -> Input: 2.8 <-
    _process_selector_ = main
    running = TRUE
    p.running = FALSE
  -> State: 2.8 <-
\end{lstlisting}
Controesempio per la starvation individuale di NuSmv.

    \centerimage{width=\columnwidth}
{rete38-3.jpg}{img:rete38-3}
    {Controesempio per l'assenza di starvation individuale di GreatSPN.}


%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.9}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{39-testo.jpg}{img:39-testo}
    {Descrizione dell'algoritmo}

I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
    \item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
        \textbf{False}
    \item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{False}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}

\subsection{NuSMV}

Il modello implementa l'algoritmo $3.8$ migliorato per mitigare la situazione di deadlock
risultante dall'esecuzione interfogliata dei due processi. Entrambi eseguono un loop in
\textit{busy waiting} alternando il valore di $want$ da $FALSE$ a $TRUE$, di modo da
permettere l'accesso nel caso l'altro processo sia in attesa. Il deadlock non \`e per\`o
evitato del tutto: se i due processi entrano nel loop in maniera sincrona (un'istruzione alla
volta) non riusciranno mai a proseguire alla SC, come mostrano i controesempi seguenti.
\break
\break
Sono stati utilizzati 7 stati, di cui:

\begin{description}
    \item{$local$: } Sezione non critica.
    \item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
    \item{$enter$: } Lo stato inizia un loop che viene eseguito finch\`e la $want$ opposta
        non diventa $FALSE$. Il loop itera sugli stati $loopUnset$ e $loopSet$.
    \item{$loopUnset$: } Cambia il valore della variabile $want$ propria a $FALSE$, per
        permettere l'accesso all'altro processo nel caso questo sia gi\`a in $enter$.
    \item{$loopSet$: } Cambia il valore della variabile $want$ propria a $TRUE$, per
        segnalare l'intezione di entrare nella sezione critica.
    \item{$critical$: } Sezione critica.
    \item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}

Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.

\begin{lstlisting}
MODULE main
VAR
  wp : boolean;
  wq : boolean;
  p : process user(wp,wq);
  q : process user(wq,wp);
ASSIGN
  init(wp) := FALSE;
  init(wq) := FALSE;

SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = set -> AF p.state = critical)

MODULE user(wp, wq) 
VAR
  state : {local,set,enter,loopUnset, loopSet, critical, exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, set};
      state = set : enter;
      state = enter & wq = FALSE : critical;
      state = enter & wq = TRUE : loopUnset;
      state = loopUnset : loopSet;
      state = loopSet : enter;
      state = critical : exit;
      state = exit : local;
      TRUE : state;
    esac;
  next(wp) :=
    case
      state = set : TRUE;
      state = loopUnset : FALSE;
      state = loopSet : TRUE;
      state = exit : FALSE;
      TRUE : wp; 
    esac;
FAIRNESS
  running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.9$.
\newpage

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
    \centerimage{width=\columnwidth}
{rete39.jpg}{img:rete39}
    {Modello GreatSPN per l'algoritmo $3.9$}

% ---- PROPRIETA`
\subsection{Mutua Esclusione}

\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
La mutua esclusione \`e rispettata in quanto la modifica della variabile $want$ viene
effettuata prima della fase di controllo. Il \textit{busy waiting} non cambia l'algoritmo da
rispetto al $3.8$ da questo punto di vista.

\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}

L'assenza di deadlock non \`e rispettata n\`e in NuSmv ne in GreatSPN. Anche con il \textit{busy 
waiting} si ripresenta il problema dell'esercizio $3.8$: se i processi sono entrambi nello
stato di attesa ($enter$), entrambi entrano nel loop e ogni volta che viene eseguito il
controllo sulle variabili, entrambe saranno $TRUE$. Si riportano i controesempi.

\begin{lstlisting}
-- specification AG (p.state = set -> AF (p.state = critical | q.state = critical))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 1.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 1.2 <-
    p.state = set
  -> Input: 1.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.3 <-
  -> Input: 1.4 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.4 <-
    wp = TRUE
    p.state = enter
  -> Input: 1.5 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.5 <-
  -> Input: 1.6 <-
  -> State: 1.6 <-
  -> Input: 1.7 <-
  -> State: 1.7 <-
    q.state = set
  -> Input: 1.8 <-
  -> State: 1.8 <-
    wq = TRUE
    q.state = enter
  -> Input: 1.9 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.9 <-
    p.state = loopUnset
  -> Input: 1.10 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 1.10 <-
    q.state = loopUnset
  -> Input: 1.11 <-
  -> State: 1.11 <-
    wq = FALSE
    q.state = loopSet
  -> Input: 1.12 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.12 <-
    wp = FALSE
    p.state = loopSet
  -> Input: 1.13 <-
  -> State: 1.13 <-
    wp = TRUE
    p.state = enter
  -> Input: 1.14 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.14 <-
    wq = TRUE
    q.state = enter
  -> Input: 1.15 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 1.15 <-
    p.state = loopUnset
  -> Input: 1.16 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 1.16 <-
    q.state = loopUnset
\end{lstlisting}
Controesempio di NuSmv per l'assenza di deadlock dell'esercizio $3.9$.
\newpage
    \centerimage{width=\columnwidth}
{rete39-2.jpg}{img:rete39-2}
    {Controesempio per l'assenza di deadlock di GreatSPN.}

\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
  AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
  G (p.state = enter -> F (p.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}

Essendo che la propriet\`a di assenza di deadlock \`e falsa, \`e lecito che anche quella di
starvation individuale lo sia. Si riportano i controesempi.

\begin{lstlisting}
-- specification AG (p.state = set -> AF p.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 2.1 <-
    wp = FALSE
    wq = FALSE
    p.state = local
    q.state = local
  -> Input: 2.2 <-
    _process_selector_ = p
    running = FALSE
    q.running = FALSE
    p.running = TRUE
  -> State: 2.2 <-
    p.state = set
  -> Input: 2.3 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.3 <-
  -> Input: 2.4 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -- Loop starts here
  -> State: 2.4 <-
    wp = TRUE
    p.state = enter
  -> Input: 2.5 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -- Loop starts here
  -> State: 2.5 <-
  -> Input: 2.6 <-
  -- Loop starts here
  -> State: 2.6 <-
  -> Input: 2.7 <-
  -> State: 2.7 <-
    q.state = set
  -> Input: 2.8 <-
  -> State: 2.8 <-
    wq = TRUE
    q.state = enter
  -> Input: 2.9 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 2.9 <-
    p.state = loopUnset
  -> Input: 2.10 <-
  -> State: 2.10 <-
    wp = FALSE
    p.state = loopSet
  -> Input: 2.11 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.11 <-
    q.state = critical
  -> Input: 2.12 <-
    _process_selector_ = p
    q.running = FALSE
    p.running = TRUE
  -> State: 2.12 <-
    wp = TRUE
    p.state = enter
  -> Input: 2.13 <-
    _process_selector_ = q
    q.running = TRUE
    p.running = FALSE
  -> State: 2.13 <-
    q.state = exit
  -> Input: 2.14 <-
  -> State: 2.14 <-
    wq = FALSE
    q.state = local
\end{lstlisting}
Controesempio per la starvation individuale di NuSmv.

    \centerimage{width=\columnwidth}
{rete39-3.jpg}{img:rete39-3}
    {Controesempio per l'assenza di starvation individuale di GreatSPN.}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.10}  \label{ssec:Es32}

    \centerimage{width=\columnwidth}
{310-testo.jpg}{img:310-testo}
    {Descrizione dell'algoritmo}

I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):

\begin{description}
    \item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
    \item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
        \textbf{True}
    \item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{True}
\end{description}

\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}

\subsection{NuSMV}

Il modello implementa l'algoritmo di Dekker, che fa uso sia delle due variabili booleane che
della variabile $turn$, riuscendo a rispettare tutte e $3$ le propriet\`a.
Sono stati utilizzati 10 stati, di cui:

\begin{description}
    \item{$local$: } Sezione non critica.
    \item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
    \item{$enter$: } Lo stato inizia un loop che viene eseguito finch\`e la $want$ opposta
        non diventa $FALSE$. Il loop itera sugli stati $checkTurn$, $loopUnset$, $waitTurn$ e $loopSet$.
    \item{$checkTurn$: } Controlla che il valore della variabile $turn$ sia corrispondente al
        processo opposto. Se cos\`i \`e, allora permette la discesa nel loop. Altrimenti il
        processo ritorna a $enter$.
    \item{$loopUnset$: } Cambia il valore della variabile $want$ propria a $FALSE$, per
        permettere l'accesso all'altro processo nel caso questo sia gi\`a in $enter$.
    \item{$waitTurn$: } Obbliga l'attesa del proprio turno controllando la variabile $turn$.
    \item{$loopSet$: } Cambia il valore della variabile $want$ propria a $TRUE$, per
        segnalare l'intezione di entrare nella sezione critica.
    \item{$critical$: } Sezione critica.
    \item{$setTurn$: } Assegna il valore di $turn$ all'altro processo.
    \item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}

Ogni processo \`e a conoscenza di $wantp$, $wantq$, della variabile $turn$, del proprio
\textit{id} e di quello dell'altro processo.

\begin{lstlisting}
MODULE main
VAR
  wp : boolean;
  wq : boolean;
  turn : 1..2;
  p : process user(wp,wq, turn, 1, 2); 
  q : process user(wq,wp, turn, 2, 1); 
ASSIGN
  init(wp) := FALSE;
  init(wq) := FALSE;
  init(turn) := 1;

SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = set -> AF p.state = critical)

MODULE user(wp, wq, turn, me, other)
VAR
  state : {local, set, enter, checkTurn, loopUnset, waitTurn, loopSet, critical, setTurn, exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, set};
      state = set : enter;

      state = enter & wq = FALSE : critical;     -- Go to CS

      state = enter & wq = TRUE : checkTurn;     -- Start waiting loop
      state = checkTurn & turn = me : enter;      -- Go back to loop check
      state = checkTurn & turn = other : loopUnset;  -- Descend in loop
      state = loopUnset : waitTurn;
      state = waitTurn & turn = me : loopSet;     -- Wait until turn == 1
      state = loopSet : enter;                   -- End of loop

      state = critical : exit;
      state = setTurn : exit;
      state = exit : local;
      TRUE : state;
    esac;

  next(wp) :=
    case
      state = set : TRUE;
      state = loopUnset : FALSE;
      state = loopSet : TRUE;
      state = exit : FALSE;
      TRUE : wp;
    esac;
  next(turn) :=
    case
      state = setTurn : other;
      TRUE : turn;
    esac;
FAIRNESS
  running
\end{lstlisting}
Modello NuSmv per l'algoritmo di Dekker.
\newpage
    \centerimage{width=\columnwidth}
{rete310.jpg}{img:rete310}
    {Modello in GreatSPN dell'algoritmo di Dekker}

% ---- PROPRIETA`
\subsection{Mutua Esclusione}

\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break

\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}

In NuSmv, dove \`e possibile imporre il requisito di fairness, l'assenza di deadlock \`e rispettat\`a.
In GreatSPN invece non \`e possibile imporre la fairness e per questo motivo pu\`o
accadere che si verifichi deadlock perch\`e uno dei processi rimane fermo (non esegue
transizioni di progresso).

    \centerimage{width=\columnwidth}
{rete310-2.jpg}{img:rete310-2}
    {Controesempio per l'assenza di deadlock di GreatSPN.}

\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{True}
\begin{lstlisting}
  AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
  G (p.state = enter -> F (p.state = critical))
\end{lstlisting}

\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}

Come per l'assenza di deadlock, anche per la starvation individuale NuSmv con $FAIRNESS
running$ ci garantisce che non si verifichi starvation, mentre per GreatSPN non si pu\`o dire
lo stesso.

    \centerimage{width=\columnwidth}
{rete310-3.jpg}{img:rete310-3}
    {Controesempio per l'assenza di starvation individuale di GreatSPN.}
\newpage

\subsection{Confronto tra NuSmv e GreatSPN}

\begin{table}[h!]
  \centering
  \begin{tabular}{ |p{3cm}||p{3cm}||p{3cm}||p{3cm}|}
    \hline
    \multicolumn{4}{|c|}{Propriet\`a degli algoritmi in NuSmv} \\
    \hline
      Esercizio & Mutua Esclusione & No Deadlock & No Starvation Ind. \\
    \hline
      3.2  & True & False & False \\
      3.5  & True & False & False \\
      3.6  & False & True & False \\
      3.8  & True & False & False \\
      3.9  & True & False & False \\
      3.10 & True & True & True \\
    \hline
    \hline
  \end{tabular} \\
    \label{tab:nusmv-table}
    \end{table}

\begin{table}[h!]
  \centering
  \begin{tabular}{ |p{3cm}||p{3cm}||p{3cm}||p{3cm}|}
    \hline
    \multicolumn{4}{|c|}{Propriet\`a degli algoritmi in GreatSPN} \\
    \hline
      Esercizio & Mutua Esclusione & No Deadlock & No Starvation Ind. \\
    \hline
      3.2  & True & False & False \\
      3.5  & True & False & False \\
      3.6  & False & \textbf{False} & False \\
      3.8  & True & False & False \\
      3.9  & True & False & False \\
      3.10 & True & \textbf{False} & \textbf{False}  \\
    \hline
    \hline
  \end{tabular} \\
    \label{tab:gspn-table}
\end{table}

\subsection{Bisimulazione: equivalenza tra esercizi $3.2$ e $3.5$}

Si vuole eguagliare i due modelli in algebra dei processi per determinare l'equivalenza dei
due algoritmi. Per fare ci\`o, si utilizza la tecnica di bisimulazione estesa, ovvero
l'algoritmo che considera le azioni $\tau$, nel modello segnate come $Sync$.

Si riportano di seguito i derivation graph per i due algoritmi, sostituendo le azioni in
$Sync$ a $\tau$.
\newpage
    \centerimage{width=\columnwidth}
{dgsync.png}{img:dgsync}
    {Derivation Graph per la rete 3.2}
\newpage
    \centerimage{width=\columnwidth}
{35dgsync.pdf}{img:35dgsync}
    {Derivation Graph per la rete 3.5}

Gli stati in comune tra i due modelli sono: \textbf{isTurnP, isTurnQ, setP, setQ}. Si applica lo
\textit{split} utilizzando questi stati come Azioni. Il set iniziale \`e rappresentato
dall'insieme degli stati dei due processi.


\subsubsection{Bisimulazione: Stato iniziale}

\begin{lstlisting}
{S1,T1}{T2,T3,T4,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14,S15,S16}
\end{lstlisting}

\subsubsection{Split su setP}

Si applica lo split sull'ultimo set:
\begin{lstlisting}
{T2,T3,T4,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14,S15,S16}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T2,T3,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14}
\end{lstlisting}

\subsubsection{Split su isTurnQ}

Si applica lo split sull'ultimo set.
\begin{lstlisting}
{T2,T3,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T3,S12,S11}{T2,S2,S3,S4,S5,S6,S7,S8,S9,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su setQ}

Si applica lo split sull'ultimo set.
\begin{lstlisting}
{T2,S2,S3,S4,S5,S6,S7,S8,S9,S10,S13,S14}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T3,S12,S11}{T2,S6,S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su isTurnP}

Si applica lo split sul primo set.
\begin{lstlisting}
{S1,T1}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3,S12,S11}{T2,S6,S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su setQ}

Si applica lo split sul quarto set.
\begin{lstlisting}
{T2,S6,S9}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3,S12,S11}{T2,S9}{S6}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su isTurnQ}

Si applica lo split sul quarto set.
\begin{lstlisting}
{T3,S12,S11}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3}{S11,S12}{T2,S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su setP}

Si applica lo split sul terzo set.
\begin{lstlisting}
{T4,S15,S16}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4}{S15,S16}{T3}{S11,S12}{T2,S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Split su setQ}
Si applica lo spit sul settimo set.
\begin{lstlisting}
{T2,S6}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4}{S15,S16}{T3}{S11,S12}{T2}{S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}

\subsubsection{Bisimulazione: conclusione}

L'algoritmo termina in quanto non \`e pi\`u possibile dividere alcun set sulla base delle
transizioni comuni.
Dopo aver applicato gli \textit{splitting} di cui sopra, i set sono partizionati nella
seguente maniera:

\begin{lstlisting}
{T1}{T4}{T3}{T2}{S1}{S15,S16}{S11,S12}{S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}


Come si pu\`o notare, gli stati dell'algoritmo $3.5$ sono gli unici elementi nel proprio set.
Se ci fosse bisimulazione, essi dovrebbero essere accoppiati a uno o pi\`u stati
dell'algoritmo $3.2$.
Possiamo quindi affermare che \textbf{non c'\`e bisimulazione} tra i due algoritmi.

\subsection{Riduzione Strutturale in modelli di reti P/T}


\subsubsection{3.2 - 3.5}

Si vogliono applicare le 4 tecniche viste di riduzione strutturale per confrontare le reti
$3.2$ e $3.5$. Si riportano i due modelli in reti P/T.

    \centerimage{width=\columnwidth}
{rete32.jpg}{img:rete32}
    {Modello P/T della rete 3.2}

    \centerimage{width=\columnwidth}
{rete35.jpg}{img:rete35}
    {Modello P/T della rete 3.5}
\break

La rete $3.5$ rappresenta un modello semplificato dell'algoritmo $3.2$, pertanto si riduce la
rete $3.2$.

Si applica:

\begin{description}
    \item{\textbf{Fusion of places}: } La fusione dei posti $P0,P1$ - $Q0,Q1$ e $P2,P3$ -
        $Q2,Q3$ (quindi su entrambe le transizioni $ncs$ e $cs$)
\end{description}

Ottenendo una rete equivalente alla $3.5$.

\subsubsection{3.6 - 3.8}

Si vogliono applicare le 4 tecniche viste di riduzione strutturale per confrontare le reti
$3.6$ e $3.8$. Si riportano i due modelli in reti P/T.

    \centerimage{width=\columnwidth}
{rete36.jpg}{img:rete36}
    {Modello P/T della rete 3.6}

    \centerimage{width=\columnwidth}
{rete38.jpg}{img:rete38}
    {Modello P/T della rete 3.8}
\break

La rete $3.6$ e la rete $3.8$ si differenziano per l'inversione delle istruzioni di $set$ e
$wait$.

Si applica:
\begin{description}
    \item{\textbf{Fusion of places}: } La fusione dei posti $P0,P1$ - $Q0,Q1$ su entrambe le
        reti.
    \item{\textbf{Fusion of places}: } La fusione dei posti $P3,P4$ - $Q3,Q4$ su entrambe le
        reti.
    \item{\textbf{Self-loop elimination}: } L'eliminazione dei self-loop delle transizioni
        $T1,T11$ su entrambe le reti.
\end{description}
A questo punto si puo` notare che le transizioni $set\{P,Q\}$ e $isWant\{P,Q\}$ non
sono riducibili in quanto non presentano nessuna delle strutture che permettono la
riduzione. Le due reti non sono quindi equivalenti.

\end{document}