--Nasladujac troche modulo.smv zbuduj model skladajacy sie z 2 zmiennych  x i y ktore zainicjalizowane sa na zera i ktore rosna (albo x:=x+1 albo y:=y+1) az w sumie dadza 7 

--a) wtedy w następnym kroku obie zmieniaja wartosc na 0
--b) wtedy ta zmienna ktora mialaby wzrosnac zmienia wartosc na zero

--Uzywajac -bmc postaraj sie zapisac i udowodnic/zaprzeczyc wlasnosciom
-- x+y <=7
-- y=2 -> X y=3
-- y = 2 -> X (y=2 | y=3)
-- y<x -> X (y<=x) 
--istnieje sciezka na ktorej x zawsze = 0