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

(************************************************************)
(* Property specification *)
(************************************************************)

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