(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : LA02_deadline-2_1param
 * 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
	time
		: clock;
	deadline
		: parameter;

	c_1:clock;
			wcet_m_0_job_1 = 20,
			wcet_m_1_job_1 = 31,
			wcet_m_2_job_1 = 17,
			wcet_m_3_job_1 = 87,
			wcet_m_4_job_1 = 76,
		: 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;


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


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

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



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