(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : jobshop_2_4
 * Description      : Jobshop case study
 * Correctness      : All tasks performed on time
 * Scalable         : yes
 * 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/12/02
 * Last modified    : 2021/10/07
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)


(*--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(*, s*)
		: clock;

	m1,m2,m3,m4
		: bool;

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

(************************************************************)
  automaton job1
(************************************************************)
actions: b1,FIN1;

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

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

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

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

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

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

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

loc Q1: invariant x1 <= d14
	when  x1=d14 sync FIN1 do {m4 := False} goto End1;

loc End1: invariant True

end (*job1*)

(************************************************************)
  automaton job2
(************************************************************)
actions: b2,FIN2;

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

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

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

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

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

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

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

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

loc End2: invariant True

end (*job1*)

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

init := {
  discrete =
  	(*------------------------------------------------------------*)
  	(* Initial location *)
  	(*------------------------------------------------------------*)
	  loc[job1] := I1,
  	loc[job2] := I2,

  	m1 := False,
    m2 := False,
    m3 := False,
    m4 := False,
  ;

  continuous =
  	(*------------------------------------------------------------*)
  	(* Initial clock constraints *)
  	(*------------------------------------------------------------*)
  	& x1=0
  	& x2=0
(*   	& s=0 *)

  	(*------------------------------------------------------------*)
  	(* Parameter constraints *)
  	(*------------------------------------------------------------*)
  	& d11 >= 0
  	& d12 >= 0
  	& d13 >= 0
  	& d14 >= 0
  	& d21 >= 0
  	& d22 >= 0
  	& d23 >= 0
  	& d24 >= 0
  ;
}

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

end