//This file was generated from UPPAAL 3.3.35, Mar 2003

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

/*
Mutex requirement.
*/
A[] P1.cs + P2.cs + P3.cs + P4.cs <= 1

/*
The system is deadlock free.
*/
A[] not deadlock

/*
Whenever P1 requests access to the critical section it will eventually enter the wait state.
*/
P1.req --> P1.wait

/*

*/
//NO_QUERY
