---- MODULE MeolicVaja4 ----

\* Potrebujemo konfiguracijsko datoteko MeolicVaja4.cfg
\* z naslednjo vsebino:
\*
\* SPECIFICATION URA
\* INVARIANT INV1
\* PROPERTY PRAVILNAURA
\* PROPERTY INVURA

\* Predviden cas za to vajo je 45 minut

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

VARIABLES
  ura             (* deklaracija spremenljivke *)

Init  ==  ura \in (1 .. 12)
Next1  ==  ura' = IF ura # 12 THEN ura + 1 ELSE 1
Next2  ==  ura' = (ura % 12) + 1

URA  ==  Init /\ [][Next1]_ura
PRAVILNAURA  ==  Init /\ [][Next2]_ura

\* Invarianta v SPECIFIKACIJI

INV1  ==  ura \in (1 .. 12)

\* Invarianto lahko zapisemo kot lastnost

INVURA  ==  [](ura \in (1 .. 12))

====