MODULE main
VAR
    cyfra : 0..9;
    zamek: {pierwsza, bledna, pierwsza_ok, druga_ok, odblokowany};

INIT cyfra in 0..9 &
    zamek = pierwsza; -- ignorujemy pierwszą cyfrę

TRANS next(cyfra) in 0..9;
TRANS next(zamek) in case
    -- zachowaj odblokowany stan
    zamek = odblokowany : odblokowany;
    -- jeśli trzecia cyfra ok to odblokowany
    zamek = druga_ok & next(cyfra) = 9 : odblokowany;
    -- jeśli druga cyfra ok
    zamek = pierwsza_ok & next(cyfra) = 5 : druga_ok;
    -- jeśli pierwsza cyfra ok
    next(cyfra) = 1 : pierwsza_ok;
    -- w każdym pozostałym przypadku błędna cyfra
    TRUE : bledna;
    esac

-- Osiągalność: zamek jest odblokowywalny [should pass]
CTLSPEC EF(zamek = odblokowany)

-- Trwałość: raz odblokowany zamek pozostanie już odblokowany [should pass]
CTLSPEC AG(zamek = odblokowany -> AX(zamek = odblokowany))

-- Bezpieczeństwo: nie reagujemy na pierwszą cyfrę (nawet jak jest 1 to stan nie jest zmieniany na pierwsza_ok) [shoud pass]
CTLSPEC AG(zamek = pierwsza & cyfra = 1 -> zamek = pierwsza)

-- Jeśli zamek nie jest jeszcze odblokowany, nie sprawdzamy aktualnie pierwszej cyfry oraz wylosowana cyfra to 1, to
-- automat powinien znaleźć się w stanie pierwsza_ok [should pass]
CTLSPEC AG(zamek != odblokowany & zamek != pierwsza & cyfra = 1 -> zamek = pierwsza_ok)