java
module main
{
  type state_t = enum { pay, select, soda, beer };

  var state : state_t;
  input insert_coin : boolean;
  output get_soda : boolean;
  output get_beer : boolean;

  init {
    state = pay;
    get_soda = false;
    get_beer = false;
  }

  next {
    if (state == pay && insert_coin) {
      state' = select;
    } else if (state == select && get_soda) {
      state' = soda;
    } else if (state == select && get_beer) {
      state' = beer;
    } else {
      state' = state;
    }

    get_soda' = (state == select && get_soda);
    get_beer' = (state == select && get_beer);
  }

  ltlspec drink_after_coin = (state == soda || state == beer) -> (state == select);
}
