module BeverageVendingMachine {
  var coin_inserted: boolean;
  var insert_coin: boolean;
  var state: enum { beer, pay, select, soda, state };

  next {
    coin_inserted' = (coin_inserted || insert_coin);

  }
}
