(******************************************************************************* * IMITATOR MODEL * * Title : jobshop_4_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/10/25 * 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, x4, s : clock; m1,m2,m3,m4 : discrete; d11,d12,d13,d14,d21,d22,d23,d24,d31,d32,d33,d34, d41,d42,d43,d44 : 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*) (************************************************************) automaton job4 (************************************************************) synclabs: b4; loc I4: invariant True when m2=0 sync b4 do {x4 := 0,m2 := 1} goto J4; loc J4: invariant x3<= d42 when x4 = d42 sync b4 do {m2 := 0} goto K4; loc K4: invariant True when m1=0 sync b4 do {x4 := 0,m1 := 1} goto L4; loc L4: invariant x3 <= d43 when x4=d43 sync b4 do {m1 := 0} goto M4; loc M4: invariant True when m3=0 sync b4 do {x4 := 0,m3 := 1} goto N4; loc N4: invariant x3 <= d41 when x4=d41 sync b4 do {m3 := 0} goto P4; loc P4: invariant True when m4=0 sync b4 do {x4 := 0,m4 := 1} goto Q4; loc Q4: invariant x3 <= d44 when x4=d44 sync b4 do {m4 := 0} goto End4; loc End4: invariant True end (*job4*) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) loc[job1] = I1 & loc[job2] = I2 & loc[job3] = I3 & loc[job4] = I4 & m1=0 & m2=0 & m3=0 & m4=0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x1=0 & x2=0 & x3=0 & x4=0 & s=0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) (* & d11=1 & d12=3 & d13=6 & d14=7 & d21=8 & d22=5 & d23=10 & d24=4 & d31=5 & d32=4 & d33=9 & d34=1 & d41=9 & d42=3 & d43=3 & d44=1*) & d11 >= 0 & d12 >= 0 & d13 >= 0 & d14 >= 0 & d21 >= 0 & d22 >= 0 & d23 >= 0 & d24 >= 0 & d31 >= 0 & d32 >= 0 & d33 >= 0 & d34 >= 0 & d41 >= 0 & d42 >= 0 & d43 >= 0 & d44 >= 0 ; (************************************************************) (* The end *) (************************************************************) end