// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// A vending machine controller that dispenses gum once. The 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          //
// ************************************************************************** //

module VendingMachine(event bool ?nickel,?dime,gum,int{31} credit) {
    // ------------------------------------------
    // thread for counting the credit
    // ------------------------------------------
    loop {
       event int{31} 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;
    }
} satisfies {

    // --- the credit is always positive
    credit_positive : assert A G (credit >= 0);
    // --- 25 is an upper bound for the credit
    credit_max25 : assert A G (credit <= 25);
    // --- machine provides gum when credit>=15
    serve_gum : assert A G (credit >= 15 -> gum); //lmc directive deleted for Averest 2.0
}