// =======================================================================
//                        VendingMachine.qrz
//
// Vending machine controller that dispenses gum once. The two inputs,
// nickel and dime, are present when a corresponding coin has been inserted.
// The gum is present for a single cycle after the machine has been given
// fifteen cents. No change is returned.
//
// Sources: Randy H. Katz, Contemporary Logic Design, 1994, page 389
// =======================================================================

#ifdef INTEGER
#define TYPE int
#else
#ifndef BITS
#define BITS 6
#endif
#define TYPE int[BITS]
#endif

module VendingMachine(event nickel,dime,&gum,TYPE &credit)
implements VendingMachineSpec(credit)
{
    // ------------------------------------------
    // thread for counting the credit
    // ------------------------------------------
    loop {
       TYPE nickel_amount, dime_amount, gum_amount;
       if(nickel) nickel_amount = 5; else nickel_amount=0;
       if(dime) dime_amount=10; else dime_amount=0;
       if(gum) gum_amount=15; else gum_amount=0;
       next(credit) = credit + nickel_amount + dime_amount - gum_amount;
       pause;
    }
  ||
    // ------------------------------------------
    // thread for dispensing the gum: the task is
    // to return a gum if 15 cents are paid
    // ------------------------------------------
    loop {
        if(credit >= 15)
            emit gum;
        pause;
    }
}

spec VendingMachineSpec(TYPE credit) {
    // --- the credit is always positive
    credit_positive : A G (credit >= 0);
    // --- 25 is an upper bound for the credit
    credit_max25 [lmc]: A G (credit <= 25);
    // --- machine provides gum when credit>=15
    serve_gum [lmc]: A G (credit >= 15 -> gum);
}