(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : jobshop_3_4
 * Description      : Jobshop case study
 * Correctness      : All tasks performed on time
 * Scalable         : 
 * Generated        : 
 * Categories       : RTS ; Scheduling
 * Source           : Maler et al. ("Job-Shop Scheduling Using Timed Automata", by Yasmina Abdeddaïm and Oded Maler, CAV 2001 (??))
 * bibkey           : AM01
 * Author           : Romain Soulat
 * Modeling         : Romain Soulat
 * Input by         : Romain Soulat, Étienne André
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : < 2011/11/22
 * Last modified    : 2020/08/17
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)
 
(*--Job2_4: solution = 27
--
--J1: m3(1),m1(3),m2(6),m4(7)
--J2: m2(8),m3(5),m1(10),m4(4)*)

var 	x1, x2, x3, s
		: clock;

	m1,m2,m3,m4
		: discrete;

(*	d11 = 1,
	d12 = 3,
	d13 = 6,
	d14 = 7,
	d21 = 8,
	d22 = 5,
	d23 = 10,
	d24 = 4,
	d31 = 5,
	d32 = 4,
	d33 = 9,
	d34 = 1 *)
	d11,
	d12,
	d13,
	d14,
	d21,
	d22,
	d23,
	d24,
	d31,
	d32,
	d33,
	d34
		: parameter;

	
(************************************************************)
  automaton job1
(************************************************************)
synclabs: b1;

loc I1: invariant True
	when  m3=0  sync b1 do {x1 := 0, m3 := 1} goto J1;  

loc J1: invariant x1<= d13
	when  x1 = d13 sync b1 do {m3 := 0} goto K1;   

loc K1: invariant True
	when  m1=0 sync b1 do {x1 := 0,m1 := 1} goto L1;   

loc L1: invariant x1 <= d11
	when  x1=d11 sync b1 do {m1 := 0} goto M1;   

loc M1: invariant True
	when  m2=0 sync b1 do {x1 := 0,m2 := 1} goto N1;   

loc N1: invariant x1 <= d12
	when  x1=d12 sync b1 do {m3 := 0} goto P1;   

loc P1: invariant True
	when  m4=0 sync b1 do {x1 := 0,m4 := 1} goto Q1;   

loc Q1: invariant x1 <= d14
	when  x1=d14 sync b1 do {m3 := 0} goto End1;   

loc End1: invariant True 

end (*job1*)

(************************************************************)
  automaton job2
(************************************************************)
synclabs: b2;

loc I2: invariant True
	when  m2=0 sync b2 do {x2 := 0,m2 := 1} goto J2;  

loc J2: invariant x2<= d22
	when  x2 = d22 sync b2 do {m2 := 0} goto K2;   

loc K2: invariant True
	when  m3=0 sync b2 do {x2 := 0,m3 := 1} goto L2;   

loc L2: invariant x2 <= d23
	when  x2=d23 sync b2 do {m3 := 0} goto M2;   

loc M2: invariant True
	when  m1=0 sync b2 do {x2 := 0,m1 := 1} goto N2;   

loc N2: invariant x2 <= d21
	when  x2=d21 sync b2 do {m1 := 0} goto P2;   

loc P2: invariant True
	when  m4=0 sync b2 do {x2 := 0,m4 := 1} goto Q2;   

loc Q2: invariant x2 <= d24
	when  x2=d24 sync b2 do {m4 := 0} goto End2;   

loc End2: invariant True 

end (*job2*)

(************************************************************)
  automaton job3
(************************************************************)
synclabs: b3;

loc I3: invariant True
	when  m3=0 sync b3 do {x3 := 0,m3 := 1} goto J3;  

loc J3: invariant x3<= d33
	when  x3 = d33 sync b3 do {m3 := 0} goto K3;  

loc K3: invariant True
	when  m4=0 sync b3 do {x3 := 0,m4 := 1} goto L3;   

loc L3: invariant x3 <= d34
	when  x3=d34 sync b3 do {m4 := 0} goto M3;

loc M3: invariant True
	when  m1=0 sync b3 do {x3 := 0,m1 := 1} goto N3;

loc N3: invariant x3 <= d31
	when  x3=d31 sync b3 do {m1 := 0} goto P3;

loc P3: invariant True
	when  m2=0 sync b3 do {x3 := 0,m2 := 1} goto Q3;

loc Q3: invariant x3 <= d32
	when  x3=d32 sync b3 do {m2 := 0} goto End3;

loc End3: invariant True 

end (*job3*)



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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)

	  loc[job1] = I1
	& loc[job2] = I2
	& loc[job3] = I3

	& m1=0 & m2=0 	& m3=0 & m4=0 
	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x1=0 
	& x2=0
	& x3=0
	& s=0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& d11 >= 0
	& d12 >= 0
	& d13 >= 0
	& d14 >= 0
	& d21 >= 0
	& d22 >= 0
	& d23 >= 0
	& d24 >= 0
	& d31 >= 0
	& d32 >= 0
	& d33 >= 0
	& d34 >= 0
;

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

end