(************************************************************
 *                      IMITATOR MODEL                      
 *
 * References: ''Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems'' (2013) by Youcheng Sun, Romain Soulat, Giuseppe Lipari, Etienne Andre and Laurent Fribourg; Test Case 2
              
 * Note: might not be the final model of the paper (?)
 
 * Created         : 2020/08/18
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3.0
 ************************************************************)

property := #synth AGnot(
	(loc[proc_1] = DEADLINE_MISS)
	or
	(loc[proc_2] = DEADLINE_MISS)
	or
	(loc[proc_3] = DEADLINE_MISS)
);