1991 lines
53 KiB
TeX
Executable file
1991 lines
53 KiB
TeX
Executable file
\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}
|