1. Obejrzyj automaty które generuje Spin dla formuł LTL

spin -f '!<>[]p'
spin -f '[]<>!p'
spin -f '![](p -> (p U q))'


2. Sprawdź, że dla modelu opisanego w pliku ZeroSto w każdym nieskończonym sceniariuszu od pewnego miejsca między każdymi dwoma nieparzystymi wartościami x jest parzyście wiele parzystych wartości x.

3. Plik printer.pml i polecenia printer.txt