//This file was generated from (Academic) UPPAAL 4.0.8 (rev. 4276), March 2009

/*

*/
E<> tea_enabled

/*

*/
A[] tea_enabled imply CoinValidator.have_c150

/*

*/
E<> Scenario.end_of_scenario

/*

*/
A[] (CoinValidator.have_c50 || CoinValidator.have_c100 || CoinValidator.have_c150) && w > 0\
  imply water_enabled

/*

*/
E<> w == 0