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

  var state : state_t;
  var coin_inserted : boolean;

  init {
    state = pay;
    coin_inserted = false;
  }

  transition {
    // User actions
    rule insert_coin {
      state == pay && !coin_inserted ==> {
        coin_inserted := true;
      }
    }

    // Machine actions
    rule get_soda {
      state == select && coin_inserted && coin_inserted := false;
    }

    rule get_beer {
      state == select && coin_inserted && coin_inserted := false;
    }
  }

  ltl property drink_after_coin {
    always (state != soda && state != beer) | coin_inserted;
  }
}
