Batoniki
mtype = {PLN2, PLN5, MILK, DARK}
chan k = [0] of {mtype};
proctype Lasuch(){
do
:: k!PLN2
printf("Wyprodukowalem %e\n", PLN2);
:: k!PLN5
printf("Wyprodukowalem %e\n", PLN5);
od
}
proctype Maszyna(byte ileM; byte ileC) {
mtype moneta;
do
:: k?moneta;
printf("Stan kasy: %d zl\nDostałem %e\n", kasa, moneta);
if
:: moneta == PLN2 -> kasa = kasa + 2; k!MILK;
:: moneta == PLN5 -> kasa = kasa + 5; k!DARK;
fi
od
}
init {
run Lasuch()
run Maszyna(10,10)
}