#+TITLE:   Esercizio Timed Automata
#+AUTHOR:   Francesco Mecca
#+EMAIL:    me@francescomecca.eu
#+LANGUAGE: en
#+LaTeX_CLASS: article
#+LaTeX_HEADER: \linespread{1.25}
#+LaTeX_HEADER: \usepackage{pdfpages}
#+LaTeX_HEADER: \usepackage{comment} 

#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t
#+STARTUP: showall
* Modello A
Sono stati usati tre template per rappresentare un sender, un link wd
un receiver
| sender = Sender();
| receiver = Receiver();
| link = Link();
| system sender, receiver, link;
** Sender
Lo stato iniziale dell'automata e` /wait/ che simula l'attesa
dell'arrivo di un pacchetto che viene processato nell'intervallo [1;2]
del clock /sc/.
Lo stato successivo e` /send\under{}pkg/ che invia il pacchetto sul canale di
sincronizzazione urgente /ML/. Il sender passa allo stato /wait\under{}ack/
che simula l'attesa di un pacchetto sul canale di sincronizzazione
urgente /LM/ e resetta il clock /sc/.
Viene simulata la verifica dell'ack in un intervallo di tempo [2;4] e
successivamente l'automa torna allo stato iniziale resettando il clock
/sc/.
#+CAPTION: Sender protocollo A
[[./sender_A.jpg]]
** Receiver
Il receiver e` simmetrico al sender. Dallo stato iniziale di /wait/
viene simulato l'arrivo di un pacchetto sul canale di sincronizzazione
urgente /LR/ che permette al receiver di resettare il clock /rc/ e
avanzare nello stato /recv\under{}pkg/, simulando la preparazione del
pacchetto in un intervallo di tempo [2;4].
La transizione dallo stato /done\under{}pkg/ a /send\under{}ack/ simula la generazione
di un pacchetto di ack in un intervallo di tempo [2;4] ed tornare allo
stato iniziale dopo aver inviato il pacchetto nel canale di
sincronizzazione urgente /RL/.
#+CAPTION: Receiver protocollo A
[[./receiver_A.jpg]]
** Link
Il link e` modellato come un canale perfetto senza perdite. Lo stato
interno /idle/ simula l'attesa di un pacchetto da parte del receiver o
del sender. Lo stato /received\under{}pkg/ simula l'arrivo di un pacchetto da
parte del sender sul canale /ML/ che viene processato e spedito al
receiver sul canale /LR/. Simmetricamente le stesse operazioni di
attesa, processing e invio avvengono con i pacchetti di ack di cui si
simula l'arrivo nello stato /received\under{}ack/ dal canale di trasmissione
/RL/ e l'invio verso il sender dallo stato /resend\under{}ack/ attraverso il
canale di trasmissione /LM/. Per il processing dei pacchetti
l'intervallo di tempo e` sempre [2;4].
#+CAPTION: Link protocollo A
[[./link_A.jpg]]
** Proprieta`
Sono state verificate tre proprieta` TCTL sul modello:
- Assenza di deadlock
  | A[] (not deadlock)
  che viene rispettata e indica che la traccia del sistema e` infinita
- Il sender ricevera` sempre un ack
  | AF sender.received\under{}ack
  | A<> sender.received\under{}ack
  la proprieta` risulta vera in quanto il link non ha perdite.
- Il receiver ricevera` sempre un pacchetto
  | AF receiver.recv\under{}pkg
  | A<> receiver.recv\under{}pkg
  e` una proprieta` rispettata in quando non ci sono constraint sul
  tempo di attesa del pacchetto.
** Tempo attesa
Il tempo di attesa viene calcolato attraverso il simulatore di Uppaal.
E` stato inserito un clock che viene resettato ogni qualvolta viene
inviato un pacchetto e una volta processato l'ack.
L'intervallo di tempo che intercorre dall'invio del messaggio alla
recezione del suo ack e` [11, 22).
* Modello B 
E` stato riutilizzato il sistema A e modificato il link per simulare
la possibilita` di perdita o corruzione di un pacchetto.
** Link
Come si denota dall'immagine il link e` simile a quello del modello A
eccezion fatta per la possibilita` di procedere non
deterministicamente dagli spazi /received\under{}pkg/ e /received\under{}ack/ verso
/loss/
#+CAPTION: Link protocollo B
[[./link_B.jpg]]
Mostriamo un trace in cui il link perde un pacchetto di ack inviato
dal sender e il sistema va in deadlock.
Dalla figura possiamo notare la transizione che simula la perdita,
ovvero l'arco /received\under{}ack/ → /loss/.
#+CAPTION: Trace con deadlock
[[./trace_B.jpg]]
\includepdf{trace_B2.jpg}
** Proprieta`
Sono state verificate quattro proprieta` TCTL sul modello:
- Assenza di deadlock
  | A[] (not deadlock)
  che non e` rispettata
- Il sender compiera` sempre del progresso
  | sender.wait_ack --> (sender.received_ack)
  la proprieta` non risulta vera in quanto il link ha perdite
- Il receiver ricevera` sempre un pacchetto
  | AF receiver.recv\under{}pkg
  | A<> receiver.recv\under{}pkg
  che come per la proprieta` precedente non puo` risultare vera
- Il receiver puo` ricevere un pacchetto
  | EF receiver.recv\under{}pkg
  | E<> receiver.recv\under{}pkg
  la proprieta` risulta vera perche` il link in alcuni path riesce ad
  inviare il pacchetto (non avvengono perdite sul canale)
** Tempo attesa 
Non si devono fare modifiche al modello rispetto al precedente per
stabilire il tempo che intercorre dall'invio di un messaggio
all'arrivo dell'ack. Bisogna pero` notare che in caso di deadlock
l'ack non arriva mai al mittente e quindi effettivamente possiamo
calcolare solo il tempo di ricezione minimo, ovvero 11 cicli del clock.
* Modello C
E` stato riutilizzato il sistema B e modificati sender e receiver per
simulare la possibilita` di recovery in seguito alla perdita o
corruzione di uno o piu` pacchetti.
Vengono anche mantenute due flag binarie globali, /ack/ e /frame/ per
tenere traccia dei pacchetti inviati e degli ack ricevuti.

** Receiver
Di seguito viene mostrato il receiver del modello C. Rispetto al
Modello B il receiver utilizza una flag binaria locale /r\under{}frame/ per tenere
traccia degli pacchetti gia` ricevuti e processati.
#+CAPTION: Receiver protocollo C
[[./receiver_C.jpg]]
** Sender
Il sender e` stato modellato raddopiando il numero di posti e archi,
escludendo per lo stato iniziale, in modo da poter processare nella
parte destra i frame di tipo 0 e nella parte sinistra i frame di
tipo 1.
Inoltre sono stati aggiunti due timer che, nel momento in cui
l'automa e` fermo su /wait\under{}ack/ allo scadere del timeout, permettono
di spostarsi nello spazio /lost/ e riprovare l'invio del pacchetto.
Si nota subito che i due timer sono indipendenti l'uno dall'altro e vi
e` la possibilita` di modellare i sender senza duplicare il numero di
spazi.
#+CAPTION: Sender protocollo C (due timer)
[[./sender_2t_C.jpg]]
#+CAPTION: Sender protocollo C (un timer)
[[./sender_1t_C.jpg]]
La variabile che regola il timeout e` un numero intero uguale o
maggiore del piu` grande fra i seguenti valore:
- il massimo tempo necessario all'invio di un pacchetto che il sender non ha processato
- il massimo tempo necessario all'invio di un pacchetto che il sender ha gia`
  processato
Se non si rispetta questo constraint il sistema va in deadlock.
Nel modello utilizzato lo spazio /is\under{}dup/ e /done\under{}pkg/ del receiver
hanno lo stesso invariante e il timeout /TOUT/ ha valore minimo 16.
\begin{comment}
Ho calcolato il timeout considerando i seguenti cammini
# Perdita per sender
Link: received\under{}pkg -> resend\under{}pkg = 4
Receiver: recv\under{}pkg -> done\under{}pkg = 4
Receiver: done\under{}pkg -> send\under{}ack = 4
Link: received\under{}ack -> resend\under{}ack = 4

# Perdita per receiver
Link: received\under{}pkg -> resend\under{}pkg = 4
Receiver: recv\under{}pkg -> is\under{}dup = 4
Receiver: is\under{}dup -> send\under{}ack = 4
Link: received\under{}ack -> resend\under{}ack = 4
\end{comment}
** Proprieta`
Sono state verificate cinque proprieta` TCTL sul modello:
- In caso di perdita il sender o il receiver tentano nuovamente di
  inviare il pacchetto
  | link.loss --> (sender.send\under{}pkg \vert{}\vert{} sender.send\under{}pkg1 \vert{}\vert{} receiver.send\under{}ack) 
  questa proprieta` e` rispttata.
- Assenza di deadlock
  | A[] (not deadlock)
  questa proprieta` e` rispettata.
- Nonostante una perdita nel link, il sender o il receiver riceveranno
  il pacchetto
  | link.loss --> (sender.send\under{}pkg \vert{}\vert{} receiver.send\under{}ack)
  la proprieta` e` rispettata
- Il receiver ricevera` sempre un pacchetto
  | sender.wait\under{}ack \vert{}\vert{} sender.wait\under{}ack1 --> (sender.received\under{}ack \vert{}\vert{} sender.received\under{}ack1)
  questa proprieta` non risulta vera dato che ci possono essere delle
  perdite nel canale
- C'e` almeno un caso in cui l'ack ricevuto e` quello atteso
  | E<> (ack == expected)
  questa proprieta` risulta vera e conferma la correttezza del meccanismo di
  recovery loss.
** Tempo attesa 
In questo modello se si considera l'intervallo di tempo che intercorre
dal primo tentativo di invio alla ricezione dell'ack, non e` possibile
calcolare il valore massimo dell'intervallo.
Questo perche` non e` possibile prevedere quanti tentativi saranno
necessari per un corretto invio.
Se invece si decide di resettare il clock ad ogni tentativo di invio,
ovvero di calcolare l'intervallo di tempo che intercorre fra un
pacchetto inviato in una situazione in cui il link non avra` perdite
fino all'invio del relativo ack, allora si puo` considerare il modello
equivalente al modello A, e quindi l'intervallo e` il medesimo.