---- MODULE MeolicVaja6 ----

\* Predviden cas za to vajo je 45 minut

\* Preverite pravilnost delovanja naslednjega algoritma
\* za medsebojno izkljucevanje:
\* sem = 1;
\* (-) for (;;) {
\* (a)   while (sem == 0) do; //cakaj
\* (b)   sem--;
\* (c)   ... kriticno obmocje ...
\* (d)   sem++;
\* (-) }

\* Naloge se lotite tako, da si pripravite dva sistema P1 in P2,
\* ki oba uporabljata navedeni algoritem. Ce je algoritem pravilen,
\* potem ob njunem socasnem izvajanju nikoli ne bosta oba hkrati
\* v kriticnem obmocju (vrstica oznacena z "c").

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

VARIABLES
  pc1,pc2,      (* programska stevca imata vrednosti "a","b","c","d" *)
  sem           (* skupna spremenljivka, na začetku je 1 *)

Init == (pc1 = "a") /\ (pc2 = "a") /\ (sem = 1) 
            
\* NALOGA 1
\* Dopolni specifikacijo prvega sistema

P1Step1 ==  /\ (pc1 = "a")
            /\ (pc1' = "b")

P1Step2 ==  /\ (pc1 = "b")
            /\ (pc1' = "c")

P1Step3 ==  /\ (pc1 = "c")
            /\ (pc1' = "d")

P1Step4 ==  /\ (pc1 = "d")
            /\ (pc1' = "a")
        
P1Next == P1Step1 \/ P1Step2 \/ P1Step3 \/ P1Step4

\* NALOGA 2
\* Dopolni specifikacijo drugega sistema

P2Step1 ==  /\ (pc2 = "a")
            /\ (pc2' = "b")
            
P2Step2 ==  /\ (pc2 = "b")
            /\ (pc2' = "c")

P2Step3 ==  /\ (pc2 = "c")
            /\ (pc2' = "d")

P2Step4 ==  /\ (pc2 = "d")
            /\ (pc2' = "a")
        
P2Next == P2Step1 \/ P2Step2 \/ P2Step3 \/ P2Step4 

Next == P1Next \/ P2Next

Algoritem == Init /\ [][Next]_<<pc1,pc2,sem>>

TypeInv == sem \in {0,1}
MutualExclusion == (pc1 # "c") \/ (pc2 # "c")
                
====

\* NALOGA 3
\* Razlozi dobljen rezultat.