module main {
  type State = enum { pay, select, soda, beer };
  var current_state : State;
  var coin_inserted : boolean;

  init {
    current_state = pay;
    coin_inserted = false;
  }

  input insert_coin : boolean;
  input select_soda : boolean;
  input select_beer : boolean;

  next {
    if (current_state == pay && insert_coin) {
      current_state' = select;
      coin_inserted' = true;
    } else if (current_state == select && select_soda && coin_inserted) {
      current_state' = soda;
    } else if (current_state == select && select_beer && coin_inserted) {
      current_state' = beer;
    } else {
      current_state' = current_state;
      coin_inserted' = coin_inserted;
    }
  }

  // LTL Property: A drink is only delivered after coin insertion
  // G (soda or beer -> previous coin_inserted)
  // This property states that globally (always), if the state is soda or beer, then in the previous state, a coin must have been inserted.
  ltl deliver_after_coin { G ((current_state == soda || current_state == beer) -> (coin_inserted)) }

  control {
    init;
    check;
    print_results;
  }
}
