(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : LA02_deadline-3_6param
 * Description      : ?
 * Correctness      : ?
 * Scalable         : no
 * Generated        : ?
 * Categories       : RTS
 * Source           : Naoyuki Tamura. CSP2SAT: JSS benchmark results. 2007.
 * bibkey           : [Tamura07]
 * Author           : Naoyuki Tamura
 * Modeling         : ?? (Romain Soulat?)
 * Input by         : ?? (Romain Soulat?)
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : < 2013
 * Last modified    : 2021/07/19
 * Model version    : 0.1
 * 
 * IMITATOR version : 3.0
 ******************************************************************************)
 
 var
	c_3:clock;
		wcet_m_0_job_3 = 58,
		wcet_m_1_job_3 = 72,
		wcet_m_2_job_3 = 23,
		wcet_m_3_job_3 = 99,
		wcet_m_4_job_3 = 28,
	: parameter;

	c_2:clock;
	
		wcet_m_0_job_2 = 24,
		wcet_m_1_job_2 = 18,
		wcet_m_2_job_2 = 32,
		wcet_m_3_job_2 = 81,
		wcet_m_4_job_2 = 25,
	: parameter;

	time: clock;
	deadline: parameter;

	c_1:clock;
	
		wcet_m_0_job_1,
		wcet_m_1_job_1,
		wcet_m_2_job_1,
		wcet_m_3_job_1,
		wcet_m_4_job_1,
	: parameter;



		
(************************************************************)
(* Including body *)
(************************************************************)
#include "LA02_body-3.imi";


(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
			loc[checker] = check_1 &
			loc[job_1] = m_0_waiting &
			loc[job_2] = m_4_waiting &
			loc[job_3] = m_1_waiting &
			
			c_1 = 0 &
			c_2 = 0 &
			c_3 = 0 &
			time = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
		& wcet_m_0_job_1 >= 0
		& wcet_m_1_job_1 >= 0
		& wcet_m_2_job_1 >= 0
		& wcet_m_3_job_1 >= 0
		& wcet_m_4_job_1 >= 0
		& deadline >= 0
;



(************************************************************)
(* The end *)
(************************************************************)
end