---- MODULE MeolicVaja3 ----

\* Predviden cas za to vajo je 90 minut

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

\* urejeni pari, trojice ipd. so v TLA-ju zaporedja

ASSUME
  ~ <<1,2>> = <<2,1>>

ASSUME
  <<8,13>> = SubSeq(<<1,1,2,3,5,8,13,21,34,55>>,6,7)

ASSUME
  {1,2,3} \X {FALSE, TRUE} = {
    <<1,FALSE>>, <<1,TRUE>>,
    <<2,FALSE>>, <<2,TRUE>>,
    <<3,FALSE>>, <<3,TRUE>>
  }

S == <<7,11,13>>

ASSUME
  /\ S[1] = 7
  /\ S[2] = 11
  /\ S[3] = 13

ASSUME
  Head(S) = 7

ASSUME
  Tail(S) = <<11,13>>

ASSUME
  Len(S) = 3

ASSUME
  <<7,11,13,17>> = Append(S,17)

ASSUME
  S \o S = <<7,11,13,7,11,13>>

ASSUME
  S \o <<TRUE>> \o <<100,200>> = <<7,11,13,TRUE,100,200>>

\* nizi znakov (stringi) so v TLA-ju zaporedja crk
\* orodje TLC stringe obravnava drugace, zato ne moremo
\* napisati npr. "TLA"[2], ceprav je to pravilno v TLA+
\* niti ne moremo uporabljati operatorja \o za sestavljanje

\* Orodje TLC ne zna obravnavati neskoncnih mnozic, zato
\* ne moremo poljubno uporabljati mnozice STRING, ki je
\* mnozica vse nizov, niti npr. mnozice
\* Seq({"A","B","C"}), ki je mnozica vseh nizov
\* sestavljenih iz črk A, B in C .

ASSUME
  "ABECEDA" \in STRING

\* relacije

STUDENTI == {"ANDREJ","BORUT","CENE","DAMJAN","EDI"}

VECJI == {<<"ANDREJ","BORUT">>,
          <<"ANDREJ","DAMJAN">>,
          <<"ANDREJ","EDI">>,
          <<"CENE","ANDREJ">>,
          <<"CENE","DAMJAN">>,
          <<"CENE","EDI">>,
          <<"CENE","BORUT">>,
          <<"DAMJAN","BORUT">>,
          <<"DAMJAN","EDI">>,
          <<"EDI","BORUT">>
         }

ASSUME (* domena za VECJI *)
  LET DOMENA == {x \in STUDENTI : (\E y \in STUDENTI : <<x,y>> \in VECJI)}
  IN Print(<<"Domena za VECJI",DOMENA>>,TRUE)

ASSUME (* zaloga vrednosti za VECJI *)
  LET ZALOGA == {y \in STUDENTI : (\E x \in STUDENTI : <<x,y>> \in VECJI)}
  IN Print(<<"Zaloga vrednosti ZA VECJI",ZALOGA>>,TRUE)

SOKRAJAN == {<<"ANDREJ","ANDREJ">>,
             <<"ANDREJ","CENE">>,
             <<"ANDREJ","EDI">>,
             <<"BORUT","BORUT">>,
             <<"BORUT","DAMJAN">>,
             <<"CENE","ANDREJ">>,
             <<"CENE","CENE">>,
             <<"CENE","EDI">>,
             <<"DAMJAN","BORUT">>,
             <<"DAMJAN","DAMJAN">>,
             <<"EDI","ANDREJ">>,
             <<"EDI","CENE">>,
             <<"EDI","EDI">>
            }

ASSUME (* refleksivnost za VECJI *)
  ~(\A x \in STUDENTI : <<x,x>> \in VECJI)

ASSUME (* refleksivnost za SOKRAJAN *)
  \A x \in STUDENTI : <<x,x>> \in SOKRAJAN

ASSUME (* simetricnost za VECJI *)
  ~(\A x,y \in STUDENTI : (<<x,y>> \in VECJI) => (<<y,x>> \in VECJI))

ASSUME (* simetricnost za SOKRAJAN *)
  \A x,y \in STUDENTI : (<<x,y>> \in SOKRAJAN) => (<<y,x>> \in SOKRAJAN)

ASSUME (* tranzitivnost za VECJI *)
  \A x,y,z \in STUDENTI :
    (<<x,y>> \in VECJI) /\ (<<y,z>> \in VECJI) => (<<x,z>> \in VECJI)

ASSUME (* tranzitivnost za SOKRAJAN *)
  \A x,y,z \in STUDENTI :
    (<<x,y>> \in SOKRAJAN) /\ (<<y,z>> \in SOKRAJAN) => (<<x,z>> \in SOKRAJAN)

ASSUME (* irefleksivnost za VECJI *)
  \A x \in STUDENTI : ~(<<x,x>> \in VECJI)

ASSUME (* irefleksivnost za SOKRAJAN *)
  ~(\A x \in STUDENTI : ~(<<x,x>> \in SOKRAJAN))

ASSUME (* intranzitivnost za VECJI *)
  ~(\A x,y,z \in STUDENTI :
      (<<x,y>> \in VECJI) /\ (<<y,z>> \in VECJI) => ~(<<x,z>> \in VECJI))

ASSUME (* intranzitivnost za SOKRAJAN *)
  ~(\A x,y,z \in STUDENTI :
      (<<x,y>> \in SOKRAJAN) /\ (<<y,z>> \in SOKRAJAN) => ~(<<x,z>> \in SOKRAJAN))

\* NALOGE 1-5
\* Za relacijo VECJI in SOKRAJAN preverite nastete lastnosti.
\* totalnost
\* asimetricnost
\* antisimetricnost
\* sovisnost
\* strogo sovisnost
\* enolicnost

\* NALOGA 6
\* Definiraj relacijo IDENTITETA v mnozici STUDENTI in ugotovi,
\* ali je to ekvivalenčna relacija.

\* Funkcije

URA == 0..23
DELDNEVA == {"DOPOLDNE","POPOLDNE"}

TERMIN(x) == IF (x \in 0..11) THEN "DOPOLDNE" ELSE "POPOLDNE"
MALICA(x) == IF (x \in 0..11) THEN 9 ELSE 17
VECJIZA2(x) == (x+2)%24

ASSUME
  /\ Print(<<"Funkcija TERMIN element",7,"preslika v element",TERMIN(7)>>,TRUE)
  /\ Print(<<"Funkcija VECJIZA2 element",7,"preslika v element",VECJIZA2(7)>>,TRUE)
  /\ Print(<<"Funkcija MALICA element",7,"preslika v element",MALICA(7)>>,TRUE)
  /\ Print(<<"Funkcija TERMIN element",22,"preslika v element",TERMIN(22)>>,TRUE)
  /\ Print(<<"Funkcija VECJIZA2 element",22,"preslika v element",VECJIZA2(22)>>,TRUE)
  /\ Print(<<"Funkcija MALICA element",22,"preslika v element",MALICA(22)>>,TRUE)

\* NALOGE 7-8
\* Za funkcije TERMIN, MALICA in VECJIZA2 preveri nasteti lastnosti:
\* injektivnost
\* surjektivnost

====