//This file was generated from (Academic) UPPAAL 4.1.2 (rev. 4405), August 2009

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

/*
Mutex requirement.
*/
A[] (sum(i:pid_t) P(i).cs) <= 1

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

/*

*/
//NO_QUERY
