
module vending_machine
{
  var nsoda : int;
  var nbeer : int;
  var sget : bool;
  var bget : bool;
  var refill : bool;
  var coin : bool;

  location start;
  location select;

  init start;

  transition start, select {
    true:coin -> select;
    true:refill -> start;
  }

  transition select {
    nsoda > 0:sget -> start;
    nbeer > 0:bget -> start;
    nsoda == 0 && nbeer == 0:ret_coin -> start;
  }

  action refill {
    nsoda := max;
    nbeer := max;
  }

  action sget {
    nsoda := nsoda - 1;
  }

  action bget {
    nbeer := nbeer - 1;
  }

  action ret_coin {
    // No change in bottle count, just return the coin
  }
}
