(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer's mutual exclusion protocol
 *
 * Description     : Fischer's mutual exclusion protocol
 * Correctness     : No two processes in the mutual exclusion
 * Source          : From "Linear Parametric Model Checking of Timed Automata" Hune, Romijn, Stoelinga, Vaandrager, 2002
 * Author          : Hune, Romijn, Stoelinga, Vaandrager
 * Modeling        : Hune, Romijn, Stoelinga, Vaandrager
 * Input by        : Étienne André
 *
 * Created         : 2013/12/10
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)

property := #synth IM(
	(* Random pi0 satisfying max_rw <= min_delay *)
	& min_rw = 1
	& max_rw = 2
	& min_delay = 3
	& max_delay = 4
);