TLA Simple Demo (comments in PL)

scratch.tla

------------------------------ MODULE scratch ------------------------------
EXTENDS Integers, TLC

\* Zmienne 
VARIABLE x,step,increase_by,init

\* Stałe - podane przez użytkownika
CONSTANT steps,y_range

\* Tablica zmiennych - jako ułatwienie, bo każdy
\* stan musi być opisany w każdym kroku
variables_list == <<x, increase_by, step, init>> 

\* Najpierw przeczytaj Spec, później wróć tutaj


\* Stan poczatkowy - istotne - cale uniwersum musi byc opisane
Init ==
    /\ x \in -50..50
    /\ step = 1
    /\ init = x
    /\ increase_by \in y_range
    

(*
Increase - IF/ELSE bardzo wazny bo definiuje warunki brzegowe
w przeciwnym wypadku TLC by zwiekszal w nieskonczonosc.

x' to "x w nastepnej iteracji"

Jeszcze raz - cale uniwersum jest tutaj opisane.
*)

Increase ==
    /\ IF step < steps THEN
            /\ x' = x + increase_by     
            /\ step' = step + 1
       ELSE
            UNCHANGED variables_list
            
\* Next - po prostu Increase ORAZ increase_by i init sie nie zmieniaja                  
Next == Increase /\ UNCHANGED <<increase_by, init>> 

(*
Specyfikacja. To ciag logiczny (/\ to ORAZ, \/ to LUB, jak w mat.).
Praktycznie opis mozliwych sytuacji.

1) ORAZ Init - ORAZ tylko aby align był
2) ORAZ Zawsze Next LUB variables_list nie uległo zmianie
3) ORAZ Strong Fairness variable_list w czasie kroku(Next)

TLDR; Zacznij od Init a potem rob zawsze Next ORAZ badz Fair

Fairness - Co do reguły TLC moze w dowolnym momencie wlozyc krok "Stutter".
"Stutter" oznacza, ze zadna zmienna (w tym wypadku nic w variables_list, wg 2) sie nie zmieni. 

Strong Fairness oznacza, ze ZAWSZE Next zmieni variables_list
Weak Fairness oznaczaloby, ze KIEDYS Next zmieni variables_list

TLDR; Fairness oznacza, ze nie bedzie stutterow
*)

Spec ==
    /\ Init
    /\ [][Next]_variables_list
    /\ SF_variables_list(Next)

\* Niezmienniki
NextBigger  == IF step > 1 THEN x > init ELSE TRUE


=============================================================================