Andrzej M. BorzyszkowskiAndrzej M.
	Borzyszkowski
System weryfikacji Spin

Zadanie 1.

Rozwiązanie umieść na portalu edukacyjnym.

Zadanie 2.

Stwórz model maszyny sprzedającej łakocie. W ofercie ma ona batoniki z mlecznej i ciemnej czekolady. Batonik mleczny kosztuje 2 zł, a gorzki – 5 zł. System powinien składać się z maszyny i „batonoholika” komunikujących się za pośrednictwem kanału – w jedną stronę płyną pieniądze, a w drugą – batony. Wiadomości modeluj za pomocą komunikatów:

        mtype = {PLN2, PLN5, MILK, DARK}

Na początek możesz użyć pliku batoniki-0.pml. Po zdefiniowaniu modelu wykonaj po kolei nastepujące ćwiczenia:

Rozwiązanie umieść na portalu edukacyjnym.

Do góry