(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer's mutual exclusion protocol
 *
 * Description     : Fischer's mutual exclusion protocol with 2 processes
 * Correctness     : The mutual exclusion is ensured
 * Source          : ?
 * Author          : ?
 * Modeling        : Romain Soulat
 * Input by        : Romain Soulat, Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : < 2012/02/14
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)

property := #synth IM(
	& a=1
	& b=4
);