```// ************************************************************************** //
//                                                                            //
//    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;
}
||
// ------------------------------------------
// 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
}
```