(************************************************************
 *                      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         : 2020/08/14
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)
 
(************************************************************)
(* Property specification *)
(************************************************************)

property := #synth AGnot(loc[proc1] = CS & loc[proc2] = CS);