---- MODULE MeolicVaja5 ----

\* Predviden cas za to vajo je 45 minut

\* Napisite specifikacijo sistema v TLA+, ki predstavlja program P
\* s tremi spremenljivkami, x , y in z. Vse inicializira na 0.
\* Nato najprej poveca x za 1, nato y nastavi na 2, nazadnje pa z
\* nastavi na vsoto x in y.

\* Pri resevanju naloge bomo uporabili pomozno spremenljivko pc,
\* s katero bomo zagotovili pravilni vrstni red izvajanja operacij.
\* To ni edini mozni nacin izvedbe, je pa zelo prirocen in preprost.

\* Sistem ima zagatno stanje. Ce nocemo,da nas TLC na to opozori,
\* uporabimo ukaz java tlc2.TLC -deadlock MeolicVaja5

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

VARIABLES
  pc,             (* programski stevec ima vrednosti 0,1,2,3 *)
  x,y,z           (* spremenljivke *)

\* pc in spremenljivke x, y, z nastavimo na nic
Pinit == (pc = 0) /\ (x = 0) /\ (y = 0) /\ (z = 0)

\* NALOGA 1
\* V prvem koraku povecamo x za 1
Pstep1 == TRUE

\* NALOGA 2
\* V drugem koraku nastavimo y na 2
Pstep2 == TRUE

\* NALOGA 3
\* V tretjem koraku nastavimo z na vsoto x + y
Pstep3 == TRUE

\* Vsak korak v sistemu bo vedno eden od treh nastetih
PNext == Pstep1 \/ Pstep2 \/ Pstep3

P == Pinit /\ [][PNext]_<<pc,x,y,z>>

PRAVILNO ==
  IF (pc = 3) THEN (x = 1) /\ (y = 2) /\ (z = 3) ELSE TRUE

====

\* NALOGA 4
\* Spremeni drugi korak tako, da bo y dobil vrednost 5.
\* Prepricas se lahko, da TLC najde napako.
\* Nato namesto INVARIANT v konfiguracijsko datoteko napisi
\* PROPERTY. Ali bo potem TLC odkril napako. Razlozite.