(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer's mutual exclusion protocol
 *
 * Description     : Fischer's mutual exclusion protocol. Version with 2 processes.
 * 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         : 2020/08/14
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)

(************************************************************)
(* Property specification *)
(************************************************************)
property := #synth AGnot(loc[process_1] = cs_1 & loc[process_2] = cs_2 & loc[process_3] = cs_3);