(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer's mutual exclusion protocol
 *
 * Description     : Fischer's mutual exclusion protocol with 2 processes
 * Correctness     : Not 2 processes together in the critical section (location obs_violation unreachable)
 * Source          : PAT library of benchmarks
 * Author          : ?
 * Input by        : Étienne André
 *
 * Created         : 2012/10/08
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)
 
property := #synth IM(
	& delta   = 3
	& epsilon = 4
);