---- MODULE MeolicVaja7 ----

\* Predviden cas za to vajo je 45 minut

\* Preveri pravilnost spodaj opisane izvedbe protokola ABP.

\* S protokolom ABP povezemo oddajnik Snd in sprejemnik Rcv.
\* Med seboj si izmenjujeta okvirje, ki vsebujejo vrednosti
\* iz mnozice Data. Za vsak sprejet podatek sprejemnik
\* poslje potrditev - to so okvirji brez vsebine.
\* Posiljanje podatkov in potrditev ponazorimo z dvema
\* vrstama tipa FIFO, msgQ in ackQ. Nazadnje oddana vrednost
\* je vedno shranjena v spremenljivki send, nazadnje sprejeta
\* vrednost pa v spremenljivki rcvd. Podatki in potrditve
\* se lahko pri prenosu izgubijo. Dolzino vrst moramo
\* omejiti s stavkom CONSTRAINT, podamo npr.
\* CONSTRAINT (Len(msgQ) <= 2) /\ (Len(ackQ) <= 2)

\* Da bomo lahko preverili pravilnost protokola, dodamo v sistem
\* se sbuff in rbuff. To sta polji, ki hranita zgodovino oddanih
\* ter sprejetih vrednosti. Dolzino polj moramo omejiti,
\* s stavkom CONSTRAINT, podamo npr.
\* CONSTRAINT (Len(sbuff) <= 3) /\ (Len(rbuff) <= 3)

\* ODDAJA PODATKOV:
\* Oddajnik ima pri sebi lokalni spremenljivki sBit in sAck, ki lahko
\* zavzameta le vrednosti 0 ali 1. Pred vsako oddajo novega
\* paketa oddajnik bit sBit spremeni (nic v ena oz. obratno). V oddan
\* okvir doda trenutno vrednost sBit. Nato caka na potrditev.
\* Ce potrditve v dolocenem casu ne dobi, poslje okvir
\* z enako vsebino se enkrat.

\* SPREJEM PODATKOV IN ODDAJA POTRDITVE
\* Sprejemnik ima pri sebi lokalno spremeljivko rBit, ki
\* prav tako lahko zavzame le vrednosti 0 ali 1. Pri sprejemu
\* podatkov shrani stevilko iz okvirja v rBit. Nato odda potrditev,
\* v katero doda trenutno vrednost rBit in spet caka na nov okvir.

\* SPREJEM POTRDITVE
\* Ko sprejemnik dobi potrditev, shrani stevilko potrditve v sAck.
\* Nato preveri, ali sta sBit in sAck enaki. Ce nista, potrditev zavrze
\* in caka naprej, Ce sta enaki, pa se oddajnik vrne v korak oddaje
\* podatkov.

EXTENDS
  TLC,            (* Operator Print *)
  Naturals,       (* Operatorji za aritmetiko *)
  Sequences       (* Operatorji za zaporedja *)

CONSTANTS
  Data            (* Mnozica podatkov, ki se prenasajo *)

VARIABLES
  msgQ, ackQ, sBit, sAck, rBit, sent, rcvd, sbuff, rbuff     

\* Inicializacija

Init ==
  /\ msgQ = << >>
  /\ ackQ = << >>
  /\ sBit = 0
  /\ sAck = 0
  /\ rBit = 0
  /\ sent \in Data
  /\ rcvd \in Data 
  /\ sbuff = << >>
  /\ rbuff = << >>

\* Specifikacija protokola

SndNewValue(d) ==
  /\ sAck = sBit
  /\ sent' = d
  /\ sbuff' = Append(sbuff, d)
  /\ sBit' = 1 - sBit
  /\ msgQ' = Append(msgQ, <<sBit',d>>)
  /\ UNCHANGED <<ackQ,sAck,rBit,rcvd,rbuff>>
    
ReSndMsg ==
  /\ sAck # sBit
  /\ msgQ' = Append(msgQ, <<sBit,sent>>)
  /\ UNCHANGED <<ackQ,sBit,sAck,rBit,sent,sbuff,rcvd,rbuff>>

RcvMsg ==
  /\ msgQ # << >>
  /\ msgQ' = Tail(msgQ)
  /\ rBit' = Head(msgQ)[1]
  /\ rcvd' = Head(msgQ)[2]
  /\ rbuff' = Append(rbuff, rcvd')
  /\ UNCHANGED <<ackQ,sBit,sAck,sent,sbuff>>

SndAck ==  
  /\ ackQ' = Append(ackQ, rBit)
  /\ UNCHANGED <<msgQ,sBit,sAck,rBit,sent,sbuff,rcvd,rbuff>>  

RcvAck ==  
  /\ ackQ # << >>
  /\ ackQ' = Tail(ackQ) 
  /\ sAck' = Head(ackQ)
  /\ UNCHANGED <<msgQ,sBit,rBit,sent,sbuff,rcvd,rbuff>>  

\* Specifikacija izgubnega kanala. Kadarkoli se lahko iz vrste zbrise
\* en clen, s tem specificiramo izgubljanje okvirjev.

Lose(q) ==
  /\ q # << >>
  /\ \E i \in 1..Len(q) :
     q' = [j \in 1..(Len(q) - 1) |-> IF j < i THEN q[j] ELSE q[j + 1]]
  /\ UNCHANGED <<sBit,sAck,rBit,sent,sbuff,rcvd,rbuff>>

LoseMsg == Lose(msgQ) /\ UNCHANGED ackQ

LoseAck == Lose(ackQ) /\ UNCHANGED msgQ	

\* Sistem sestavimo skupaj

Next ==
  \/ \E d \in Data : SndNewValue(d)
  \/ ReSndMsg \/ RcvMsg \/ SndAck \/ RcvAck
  \/ LoseMsg \/ LoseAck

abvars == <<msgQ,ackQ,sBit,sAck,rBit,sent,sbuff,rcvd,rbuff>>

AlternatingBit == Init /\ [][Next]_abvars

\* Invariante in lastnosti

TypeInv ==
  /\ msgQ \in Seq({0, 1} \times Data)
  /\ ackQ \in Seq ({0, 1})
  /\ sBit \in {0, 1}
  /\ sAck \in {0, 1}
  /\ rBit \in {0, 1}
  /\ sent \in Data
  /\ rcvd \in Data 
  /\ sbuff \in Seq(Data)
  /\ rbuff \in Seq(Data)    

Reliable == 
  /\ Len(rbuff) <= Len(sbuff)
  /\ rbuff = SubSeq(sbuff,1,Len(rbuff))

====

\* NALOGA:
\* Spremeni formulo za RcvMsg tako, da bo sistem pravilno
\* uposteval dvojnike. Upostevati je potrebno naslednje pravilo.

\* Pri sprejemu podatkov preverimo, ali je stevilka okvirja enaka rBit.
\* Ce je enaka, potem je to dvojnik in ga zavrzemo (ne upostevamo).

\* Dodati je potrebno naslednjo formulo:
\*  rbuff' = IF rBit = Head(msgQ)[1] 
\*           THEN rbuff 
\*           ELSE Append(rbuff, Head(msgQ)[2])