Zad 1. Jaka indukcja w jest potrzebna dla w metodzie bmc, Ĺźeby
sprawdzić że w modelu opisanym w modulo.smv zachodzi inwariant:

a) y!=8
b) y!=9
c) y<8
d) y<9 
 
Zad 2. Naśladując trochę modulo.smv zbuduj model skladający się z 2
zmiennych x i y, które zainicjalizowane są na zera i które rosną (albo
x:=x+1 albo y:=y+1 na jedno tyknięcie zegara) aż osiągną w sumie wartość 7 i

I. w następnym kroku obie zmieniają wartość na zero
II. ta zmienna która miałaby wzrosnać zmienia wartość na zero

Używając metody bmc postaraj sie zapisać i udowodnić/zaprzeczyć własnościom

a)  x+y <=7
b)  y=2 -> X y=3
c)  y = 2 -> X (y=2 | y=3)
d)  y<x -> X (y<=x) 
e)  istnieje sciezka na ktorej x zawsze = 0