//This file was generated from (Academic) UPPAAL 4.0.10 (rev. 4417), September 2009

/*

*/
A[] (P1.my_secrets <= 15)

/*

*/
E<> (P1.my_secrets==31 and P2.my_secrets==31 and P3.my_secrets==31 and P4.my_secrets==31 and P5.my_secrets==31)