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 {
    if (state == pay && coin_inserted) {
      state := select;
    } else if (state == select) {
      if (coin_inserted) {
        if (some_condition) {
          state := soda;
        } else {
          state := beer;
        }
      }
    }
  }

  process insertCoin {
    var inserted : boolean;

    transition {
      inserted := coin_inserted;
      coin_inserted := true;
    }

    next {
      coin_inserted := inserted;
    }
  }

  process getSoda {
    transition {
      if (state == soda) {
        state := pay;
      }
    }
  }

  process getBeer {
    transition {
      if (state == beer) {
        state := pay;
      }
    }
  }

  ltl property drink_after_coin {
    always (state == soda || state == beer) -> coin_inserted;
  }
}
