ronek22
1/8/2019 - 2:51 PM

Batoniki

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)
}