Zweryfikuj prawdziwość następujących stwierdzeń. Postaraj się
uzasadnić uzyskaną odpowiedź.

Plik "zeroSto":
 
  1) wartość x jest zawsze większa od 0 i mniejsza równa 100
  2) kiedyś x będzie równy 1
  3) zawsze wartość x po jakimś czasie dojdzie do 1


Plik "demonStepper":
  1) kiedyś będzie (x != 19)
  2a) jeśli kiedyś zajdzie (x == 1), to kiedyś w przyszłości musi zajść (x == 9)
   b) co się zmieni, jeśli usuniemy jeden z dozorów (x > 9)
  3a) zmień wartość początkową x na 10; czy zachodzi (x < 19) U (x == 19)
   b) co się zmieni, gdy
          :: x > 9 -> x = 0
      zamienimy na
          :: x > 19 -> x = 0
  4) zweryfikuj własność z punktu 1) z ustawioną opcją "With Weak Fairness"


Plik "peterson" (z laboratorium 1):
  1) w sekcji krytycznej zawsze jest co najwyĹźej jeden proces
  2) któryś proces wejdzie do s.k.
  3) każdy proces wejdzie do s.k. (spróbuj też z opcją "Weak Weak Fairness")
  4) jeśli proces zachce (flag[_pid] == 1), to w końcu wejdzie do s.k.
  5) jeśli proces czeka na wejście do s.k., to drugi proces nie wejdzie do niej dwukrotnie

Plik "elevator" (z laboratorium 1):

Dodaj przycisk do windy, który może przyjmować jedną z 4 wartości
0..3. Winda powinna jechać w kierunku wezwania i dopóki go nie obsłuży
to nie zapamiętuje innych wezwań. Wartość wezwania może być globalna.

Czy prawdziwa jest własność, że jeśli przycisk ma wartość 1 to winda
kiedyś obsłuży to wezwanie ?