//This was generated from Uppaal2k

/*
Fischer's mutual exclusion protocol.
*/
//NO_QUERY


/*
Mutex requirement.
*/
A[] not ( ( P1.cs and ( P2.cs or P3.cs or P4.cs ) ) or \
          ( P2.cs and ( P3.cs or P4.cs ) ) or \
          ( P3.cs and P4.cs ) \
        )