\documentclass{article}
%\usepackage{times}


%\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}

\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 Timed Automata}


\author{Francesco Galla`, francesco.galla@edu.unito.it}

\maketitle


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

\section{Modello A}  \label{sec:modA}
MODELLO A. Si assume che il canale sia perfetto, e quindi n\`e il messaggio, n\`e l’ack
possono essere persi. Il tempo di trasmissione sul link \`e variabile all’interno di un 
intervallo limitato, con poca variabilit\`a (quindi upper e lower bound del tempo di
trasmissione sul link sono molto vicini, diciamo non sopra un decimo del tempo di
trasmissione).
%=========================================================================================================
\subsection{Il modello Uppaal}  \label{ssec:Uppaal}

Il modello \`e composto da 3 template, rappresentanti un sender, un receiver e un link.

\subsubsection{Sender}

Tra gli stati del processo $Sender$, si nota lo stato iniziale di \textit{wait} \textbf{waitPacket}
in cui il processo attende un evento per cominciare la preparazione di un pacchetto. Una
volta che il pacchetto \`e pronto per essere mandato (con un tempo compreso nell'intervallo
$[1,4]$ del clock $sc$) allora si passa allo stato \textbf{canSend}. Da qui, il pacchetto
viene mandato sul canale di sincronizzazione $ML$ (urgente) e il $Sender$ passa a
\textbf{waitACK}. La ricezione dell'ACK avviene sul canale di sincronizzazione $LM$
(urgente) e il clock $sc$ viene resettato.
Ricevuto l'ACK, il $Sender$ rimane nello stato di \textbf{receivedACK} in cui occupa un tempo
nell'intevallo $[2,4]$ del clock $sc$ per processarlo, per poi resettare nuovamente il clock
e ritornare allo stato iniziale.


\subsubsection{Receiver}

Il processo $Receiver$ segue una dinamica simile a quella del $Sender$: anche questo ha $4$
stati, di cui l'iniziale \textbf{waitPacket} \`e l'attesa di un pacchetto (mandato dal
$Sender$ e trasportato dal $Link$ al $Receiver$ sul canale di sincronizzazione $LR$ (urgente).
Ricevuto il pacchetto, il receiver utilizza un tempo compreso nell'intevallo $[2,4]$ per
processarlo in \textbf{receivedPacket} e passare nello \textbf{donePacket} resettando il
clock $rc$. Qui impiega tra $2$ e $3$ secondi per costruire un ACK e passare nello stato
\textbf{canACK}, da cui pu\`o mandare l'acknowledgement sul canale di sincronizzazione $RL$
(urgente).

\subsubsection{Link}

Il processo $Link$ \`e modellato senza perdite (canale perfetto) e utilizza $5$ stati, di cui
quello iniziale \`e considerato uno stato interno e modella le situazioni in cui i processi
$Sender, Receiver$ stanno eseguendo operazioni locali (per cui non c'\`e comunicazione sul
canale). Gli altri stati si comportano in maniera simile agli stati gi\`a visti negli altri
due processi, utilizzando il clock $lc$.

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modAsend.jpg}{img:sendA}
	{Sender A}

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modArecv}{img:recvA}
	{Receiver A}

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modAlink.jpg}{img:linkA}
	{Link A}


\subsection{Analisi TCTL delle propriet\`a}

Sono state controllate 4 propriet\`a sul modello A. Essendo un modello \textit{perfetto},
senza perdite n\`e rumore, si nota come rispetti tutte le propriet\`a verificate.

\begin{description}
    \item{\textbf{1.} } $AG (not deadlock)$ \`e vera, quindi la traccia del sistema di
        processi \`e infinita.
    \item{\textbf{2.} } $sender.waitACK --> (sender.receivedACK)$ \`e vera, in quanto senza
        perdite il sender sar\`a sempre in grado di ricevere l'ACK entro un tempo finito.
    \item{\textbf{3.} } $AF receiver.receivedPacket$ \`e vera, in quanto non ci sono
        constraint sul tempo di attesa di $receiver.waitPacket$, pertanto un pacchetto
        verr\`a sempre ricevuto.
    \item{\textbf{4.} } Il tempo minimo e massimo tra l'invio del messaggio e la ricezione dell'ACK
        corrispondente da parte del $Sender$ sono ottenibili grazie a un clock aggiuntivo
        $fc$ che viene resettato ogni volta che un pacchetto viene mandato sul canale $ML$.
        Per questo nello stato $sender.canSend$ contiene il tempo minimo e massimo espressi
        come \textit{bound} dell'intervallo, in questo caso $[19,31]$.
\end{description}
\newpage

\section{Modello B}  \label{sec:modB}
MODELLO B. Si modifichi il modello in modo da prevedere la possibilità che il link 
perda un messaggio o un ack (la perdita equivale sia alla perdita effettiva che al 
caso di messaggio corrotto, perchè l’algoritmo si comporta in modo analogo). Non 
cambiate il protocollo, modellate semplicemente un link con perdita o 
corruzione del messaggio.
%=======================================================================================================
\subsection{Il modello Uppaal}  \label{ssec:Uppaal}

Il modello \`e composto da 3 template, rappresentanti un sender, un receiver e un link.
Il sender e il receiver mantengono la struttura del modello A, mentre nel $Link$ vengono
introdotte due perdite possibili: una per il pacchetto e una per l'ACK.

\subsubsection{Link}

Il $Link$ in questo caso ha possibilit\`a di perdere i pacchetti (scelta non deterministica)
in due stati: $receivedPacket$ e $receivedACK$, ovvero quelli in cui \`e stato mandato un
messaggio dal sender al link o dal receiver al link. Si nota come l'invariante degli due
stati sia $lc < 8$, dove con $lc == 8$ si sa con certezza che il pacchetto \`e stato perso
oppure ricevuto correttamente.
Per implementare la perdita \`e stato utilizzato un posto aggiuntivo rispetto al modello A,
chiamato $lostPacket$, che riporta allo stato fantasma del link senza per\`o mandare il
pacchetto o l'ACK.

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modBlink.jpg}{img:linkB}
	{Link B}


\subsection{Analisi TCTL delle propriet\`a}

\begin{description}
    \item{\textbf{1.} } $AG (not deadlock)$ \`e falsa, infatti la traccia del simulatore
        mostra come un pacchetto perso causi deadlock perch\`e $Sender$ e $Receiver$ sono
        rimasti in attesa di risposta e il canale non ha pi\`u comunicazioni al suo interno.
    \item{\textbf{2.} } $sender.waitACK --> (sender.receivedACK)$ \`e falsa, per lo stesso
        motivo per cui la $1.$ lo \`e.
    \item{\textbf{3.} } $EF receiver.receivedPacket$ \`e vera, perch\`e nonostante la
        possibilit\`a di deadlock, c'\`e almeno una traccia in cui il pacchetto viene
        consegnato correttamente. Questo significa che i pacchetti non sono persi con
        sicurezza ma tramite una scelta non deterministica.
    \item{\textbf{4.} } Il tempo minimo e massimo tra l'invio del messaggio e la ricezione dell'ACK
        corrispondente da parte del $Sender$ sono ottenibili grazie a un clock aggiuntivo
        $fc$ che viene resettato ogni volta che un pacchetto viene mandato sul canale $ML$.
        Dato che abbiamo una probabilit\`a di perdita all'interno del canale, possiamo
        stabilire con sicurezza solo il tempo \textbf{minimo}, che risulta equivalente a
        quello del modello A.
\end{description}
\newpage

\section{Modello C}  \label{sec:modC}
MODELLO C. Mantenendo il comportamento del canale previsto per il modello B, si
modelli il mittente e il ricevente descritti dall’algoritmo 3.
%=========================================================================================================
\subsection{Il modello Uppaal}  \label{ssec:Uppaal}

Il modello \`e composto da 3 template, rappresentanti un sender, un receiver e un link.
Il sender \`e stato implementato in due versioni, una che utilizza un timer singolo e una che
utilizza due timer. Il link non cambia rispetto al modello B.

Si utilizzano inoltre $3$ variabili globali booleane aggiuntive: $next, ack, frame$. La
scelta di utilizzare variabili booleane \`e data dal fatto che in STOP\&WAIT i messaggi sono
mandati singolarmente, per cui basta differenziare due messaggi successivi per riconoscere i
duplicati, come effettuato nel $Receiver$.

\subsubsection{Sender (timer singolo)}

Si estende il template $Sender$ del Modello A con la possibilit\`a di inviare nuovamente i
messaggi nel caso questi venissero persi, nel caso non fosse ricevuto un ACK e nel caso l'ACK
ricevuto non corrispondesse a quello atteso. Per fare ci\`o sono state utilizzate le
variabili globali di cui sopra e uno stato $lostPacket$ il cui accesso viene controllato da
una guardia sul timer $x0$ (singolo). Se il timer "scatta", ovvero se trascorre il tempo
stabilito nello stato $waitACK$, allora \`e forzato lo stato $lostPacket$ che riportando a
$canSend$ senza cambiare i valori di $frame$ e $next$ permette la ritrasmissione.
Inoltre, per il controllo della correttezza del'ACK, si utilizza una transizione con guardia
che porta dallo stato $receivedACK$ allo stato $lostPacket$, per ritrasmettere nel caso l'ACK
ricevuto non fosse corretto.

\subsection{Sender (timer doppio)}

Per il sender a timer doppio, \`e stata duplicata la struttura del primo sender di modo da
permettere una scelta tra $next == 1$ e $next == 0$. In questo modo si pu\`o discriminare tra
i due tipi di frame possibili.

\subsubsection{Receiver}

Al receiver del Modello A viene aggiunta la capacit\`a di riconoscere pacchetti duplicati
tramite una variabile locale $correctFrame$ e uno stato $dupPacket$. La transizione a questo
stato viene controllata da una guardia che discrimina se il frame ricevuto \`e corrispondente
a quello atteso. Nel caso il frame non corrispondesse, viene aggiornata la variabile $ack$ e
viene mandato l'ACK per il pacchetto ricevuto, seppur duplicato, per permettere il
proseguimento del sender.


%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modCsend1.jpg}{img:sendC}
    {Sender C (1 timer)}

	\centerimage{width=\columnwidth}
{modCsend2.jpg}{img:sendC2}
    {Sender C (2 timer)}

%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
	\centerimage{width=\columnwidth}
{modCrecv}{img:recvC}
	{Receiver C}


\subsection{Analisi TCTL delle propriet\`a}

Il sistema rispetta le propriet\`a seguenti sia con un timer sia con due, dimostrando che non
c'\`e necessit\`a per questo modello di due timer. Inoltre, il valore dei timer (settato a
$50$ in entrambi i casi) deve essere maggiore del tempo impiegato da un ACK a tornare al
sender, ossia due volte il tempo impiegato dal canale per spedire un pacchetto pi\`u
l'eventuale tempo di elaborazione nel receiver. Altrimenti si ha $deadlock$, perch\`e il
sender non riesce a spedire nuovamente il pacchetto se canale \`e occupato dall'ACK del receiver.
Il valore minimo del timer per questo modello \`e $42$.

\begin{description}
    \item{\textbf{1.} } $AG (not deadlock)$ \`e vera, quindi la traccia del sistema di
        processi \`e infinita.
    \item{\textbf{2.} } $sender.waitACK0 || sender.waitACK1 --> (sender.receivedACK0 ||
        sender.receivedACK1)$ \`e falsa, in quanto il canale pu\`o subire perdite.
    \item{\textbf{3.} } $E<> (sender.receivedACK0 \&\& ack == next )$ \`e vera, infatti esiste
        almeno un caso in cui l'ACK ricevuto dal sender \`e corretto (e quindi il modello \`e
        in grado di passare messaggi correttamente).
    \item{\textbf{4.} } $link.lostPacket --> (sender.canSend0 || sender.canSend1 ||
        receiver.canACK)$ \`e vera, in quanto in caso di pacchetto perso il sistema non si
        blocca ma permette al sender di mandare di nuovo il messaggio o al receiver di
        trasmettere l'ACK.
    \item{\textbf{4.} } Il tempo minimo e massimo tra l'invio del messaggio e la ricezione dell'ACK
        corrispondente da parte del $Sender$ sono ottenibili grazie a un clock aggiuntivo
        $fc$ che viene resettato ogni volta che un pacchetto viene mandato sul canale $ML$.
        Per questo nello stato $sender.canSend$ contiene il tempo minimo e massimo espressi
        come \textit{bound} dell'intervallo, in questo caso $[21,32]$.
\end{description}
\end{document}