(************************************************************ * 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);