You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
111 lines
2.3 KiB
111 lines
2.3 KiB
// kanban manufacturing example [CT96]
|
|
// dxp/gxn 3/2/00
|
|
|
|
ctmc
|
|
|
|
// number of tokens
|
|
const int t = 1;
|
|
|
|
// rates
|
|
const double in1 = 1.0;
|
|
const double out4 = 0.9;
|
|
const double synch123 = 0.4;
|
|
const double synch234 = 0.5;
|
|
const double back = 0.3;
|
|
const double redo1 = 0.36;
|
|
const double redo2 = 0.42;
|
|
const double redo3 = 0.39;
|
|
const double redo4 = 0.33;
|
|
const double ok1 = 0.84;
|
|
const double ok2 = 0.98;
|
|
const double ok3 = 0.91;
|
|
const double ok4 = 0.77;
|
|
|
|
module k1
|
|
|
|
w1 : [0..t];
|
|
x1 : [0..t];
|
|
y1 : [0..t];
|
|
z1 : [0..t];
|
|
|
|
[in] (w1<t) & (x1<t) -> in1 : (w1'=w1+1) & (x1'=x1+1);
|
|
[] (x1>0) & (y1<t) -> redo1 : (x1'=x1-1) & (y1'=y1+1);
|
|
[] (x1>0) & (z1<t) -> ok1 : (x1'=x1-1) & (z1'=z1+1);
|
|
[] (y1>0) & (x1<t) -> back : (y1'=y1-1) & (x1'=x1+1);
|
|
[s1] (z1>0) & (w1>0) -> synch123 : (z1'=z1-1) & (w1'=w1-1);
|
|
|
|
endmodule
|
|
|
|
module k2
|
|
|
|
w2 : [0..t];
|
|
x2 : [0..t];
|
|
y2 : [0..t];
|
|
z2 : [0..t];
|
|
|
|
[s1] (w2<t) & (x2<t) -> 1 : (w2'=w2+1) & (x2'=x2+1);
|
|
[] (x2>0) & (y2<t) -> redo2 : (x2'=x2-1) & (y2'=y2+1);
|
|
[] (x2>0) & (z2<t) -> ok2 : (x2'=x2-1) & (z2'=z2+1);
|
|
[] (y2>0) & (x2<t) -> back : (y2'=y2-1) & (x2'=x2+1);
|
|
[s2] (z2>0) & (w2>0) -> 1 : (z2'=z2-1) & (w2'=w2-1);
|
|
|
|
endmodule
|
|
|
|
module k3
|
|
|
|
w3 : [0..t];
|
|
x3 : [0..t];
|
|
y3 : [0..t];
|
|
z3 : [0..t];
|
|
|
|
[s1] (w3<t) & (x3<t) -> 1 : (w3'=w3+1) & (x3'=x3+1);
|
|
[] (x3>0) & (y3<t) -> redo3 : (x3'=x3-1) & (y3'=y3+1);
|
|
[] (x3>0) & (z3<t) -> ok3 : (x3'=x3-1) & (z3'=z3+1);
|
|
[] (y3>0) & (x3<t) -> back : (y3'=y3-1) & (x3'=x3+1);
|
|
[s2] (z3>0) & (w3>0) -> 1 : (z3'=z3-1) & (w3'=w3-1);
|
|
|
|
|
|
endmodule
|
|
|
|
module k4
|
|
|
|
w4 : [0..t];
|
|
x4 : [0..t];
|
|
y4 : [0..t];
|
|
z4 : [0..t];
|
|
|
|
[s2] (w4<t) & (x4<t) -> synch234 : (w4'=w4+1) & (x4'=x4+1);
|
|
[] (x4>0) & (y4<t) -> redo4 : (x4'=x4-1) & (y4'=y4+1);
|
|
[] (x4>0) & (z4<t) -> ok4 : (x4'=x4-1) & (z4'=z4+1);
|
|
[] (y4>0) & (x4<t) -> back : (y4'=y4-1) & (x4'=x4+1);
|
|
[] (z4>0) & (w4>0) -> out4 : (z4'=z4-1) & (w4'=w4-1);
|
|
|
|
endmodule
|
|
|
|
// reward structures
|
|
|
|
// tokens in cell1
|
|
rewards "tokens_cell1"
|
|
true : x1+y1+z1;
|
|
endrewards
|
|
|
|
// tokens in cell2
|
|
rewards "tokens_cell2"
|
|
true : x2+y2+z2;
|
|
endrewards
|
|
|
|
// tokens in cell3
|
|
rewards "tokens_cell3"
|
|
true : x3+y3+z3;
|
|
endrewards
|
|
|
|
// tokens in cell4
|
|
rewards "tokens_cell4"
|
|
true : x4+y4+z4;
|
|
endrewards
|
|
|
|
// throughput of the system
|
|
rewards "throughput"
|
|
[in] true : 1;
|
|
endrewards
|
|
|