-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBulkhead
253 lines (203 loc) · 20.8 KB
/
Bulkhead
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
dtmc
// MATHS
const double e = 2.71828182846;
// OPTIMIZATION PARAMETERS
const int THREADPOOLSIZEA;
const int THREADPOOLSIZEB;
const int TIMEOUTA;
const int TIMEOUTB;
// SIMULATION CONSTANTS
const int SIMULATION_LENGTH_IN_MICROSECONDS = 10000; // Now 100 Milliseconds
const int TOTALTHREADNUMBER = THREADPOOLSIZEA+THREADPOOLSIZEB;
// HARDWARE SPECIFICATION
const int CORES_OF_SERVER = 8;
const int MAX_AVAILABLE_DEMAND_PERCENT = 100 * CORES_OF_SERVER;
const double MANY_THREADS_PENALTY = 0.99;
// REQUEST SPECIFICATION
const double MEAN_ARRIVAL_INTERVALL_A = 20;
const double MEAN_ARRIVAL_INTERVALL_B = 10;
const int DEMAND_PERCENT_A = 55; // 100 is full CPU
const int DEMAND_PERCENT_B = 70; // 100 is full CPU
const int BASE_PROCESSING_TIME_MICROSECOND_A = 130;
const int BASE_PROCESSING_TIME_MICROSECOND_B = 62;
const double EASY_TASK_PROBABILITY_A = 0.2;
const double EASY_TASK_PROBABILITY_B = 0.1;
const double EASY_TASK_MODIFIER_A = 0.5;
const double EASY_TASK_MODIFIER_B = 0.5;
const double DIFFICULT_TASK_PROBABILITY_A = 0.1;
const double DIFFICULT_TASK_PROBABILITY_B = 0.3;
const double DIFFICULT_TASK_MODIFIER_A = 3.0;
const double DIFFICULT_TASK_MODIFIER_B = 2.0;
// LATENCY SPECIFICATION
const int SERVER_LATENCY_MEAN_INTERVALL = 500;
const int LATENCY_MEAN_INTERVALL_A = 200;
const int LATENCY_MEAN_INTERVALL_B = 200;
const int SERVER_LATENCY_DURATION = 100;
const int LATENCY_DURATION_A = 50;
const int LATENCY_DURATION_B = 50;
const double SERVER_LATENCY_MODIFIER = 0.4;
const double LATENCY_MODIFIER_A = 0.7;
const double LATENCY_MODIFIER_B = 0.7;
// COST FUNCTION SPECIFICATION
const int REJECTED_WEIGHT = 1;
const int TIMEOUT_WEIGHT = 10;
const int A_WEIGHT = 1;
const int B_WEIGHT = 1;
const int MAX_QUEUE_LENGTH_A = 10;
const int MAX_QUEUE_LENGTH_B = 10;
global CURRENT_QUEUE_LENGTH_A : [0..MAX_QUEUE_LENGTH_A] init 0;
global CURRENT_QUEUE_LENGTH_B : [0..MAX_QUEUE_LENGTH_B] init 0;
global THREAD_TOOK_INPUT_A : bool init false;
global THREAD_TOOK_INPUT_B : bool init false;
global requestFinishedA : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
global requestFinishedB : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
global activeThreadsA : [0..THREADPOOLSIZEA] init 0;
global activeThreadsB : [0..THREADPOOLSIZEB] init 0;
global total_demand_percent : [0..TOTALTHREADNUMBER*100] init 0;
rewards "costs_A" // This is a sum; cost function for A
end : REJECTED_WEIGHT * metric_rejected_A * 1/(metric_rejected_A + metric_timeout_A + metric_successfull_number_A);
end : TIMEOUT_WEIGHT * metric_timeout_A * 1/(metric_rejected_A + metric_timeout_A + metric_successfull_number_A);
endrewards
rewards "costs_B" // This is a sum; cost function for B
end : REJECTED_WEIGHT * metric_rejected_B * 1/(metric_rejected_B + metric_timeout_B + metric_successfull_number_B);
end : TIMEOUT_WEIGHT * metric_timeout_B * 1/(metric_rejected_B + metric_timeout_B + metric_successfull_number_B);
endrewards
rewards "costs_total" // This is a sum; total costs, same rewards as for A and B together, but with weights
end : A_WEIGHT * REJECTED_WEIGHT * metric_rejected_A * 1/(metric_rejected_A + metric_timeout_A + metric_successfull_number_A);
end : A_WEIGHT * TIMEOUT_WEIGHT * metric_timeout_A * 1/(metric_rejected_A + metric_timeout_A + metric_successfull_number_A);
end : B_WEIGHT * REJECTED_WEIGHT * metric_rejected_B * 1/(metric_rejected_B + metric_timeout_B + metric_successfull_number_B);
end : B_WEIGHT * TIMEOUT_WEIGHT * metric_timeout_B * 1/(metric_rejected_B + metric_timeout_B + metric_successfull_number_B);
endrewards
// TIMER
// The timer limits the simulation time.
// A request uses the timestamp of its creation as id.
module SimulationTimer
time : [0..SIMULATION_LENGTH_IN_MICROSECONDS] init 0;
end : bool init false;
finished: bool init false;
[endRound] time < SIMULATION_LENGTH_IN_MICROSECONDS & !(CURRENT_QUEUE_LENGTH_A > 0 & THREADPOOLSIZEA > activeThreadsA) & !(CURRENT_QUEUE_LENGTH_B > 0 & THREADPOOLSIZEB > activeThreadsB) -> (time' = time + 1);
[endRound] !end & time = SIMULATION_LENGTH_IN_MICROSECONDS & !(CURRENT_QUEUE_LENGTH_A > 0 & THREADPOOLSIZEA > activeThreadsA) & !(CURRENT_QUEUE_LENGTH_B > 0 & THREADPOOLSIZEB > activeThreadsB) -> (end' = true);
[] end & !finished -> (finished' = true);
endmodule
// METRICS
module SimulationStatistics_A
metric_rejected_A : [0..SIMULATION_LENGTH_IN_MICROSECONDS] init 0;
metric_timeout_A : [0..SIMULATION_LENGTH_IN_MICROSECONDS] init 0;
metric_successfull_number_A : [0..SIMULATION_LENGTH_IN_MICROSECONDS] init 0;
//metric_successfull_time_A : [0..SIMULATION_LENGTH_IN_MICROSECONDS*SIMULATION_LENGTH_IN_MICROSECONDS] init 0;
[requestA_reject] !end & (THREADPOOLSIZEA - activeThreadsA) = 0 & CURRENT_QUEUE_LENGTH_A = MAX_QUEUE_LENGTH_A & tp_requestA != -1 -> (metric_rejected_A' = metric_rejected_A +1);
//[] requestFinishedA != -1 & (time - requestFinishedA) < TIMEOUTA -> (metric_successfull_number_A' = metric_successfull_number_A + 1)&(metric_successfull_time_A' = metric_successfull_time_A + time - requestFinishedA) & (requestFinishedA'=-1);
[] !end & requestFinishedA != -1 & (time - requestFinishedA) < TIMEOUTA -> (metric_successfull_number_A' = metric_successfull_number_A + 1) & (requestFinishedA'=-1);
[] !end & requestFinishedA != -1 & (time - requestFinishedA) >= TIMEOUTA -> (metric_timeout_A' = metric_timeout_A + 1)&(requestFinishedA'=-1);
[endRound] !end & requestFinishedA = -1 -> true;
endmodule
//module SimulationStatistics_B = SimulationStatistics_A [metric_rejected_A = metric_rejected_B, metric_timeout_A = metric_timeout_B, metric_successfull_number_A = metric_successfull_number_B, metric_successfull_time_A = metric_successfull_time_B,
//requestA_reject = requestB_reject, activeThreadsA = activeThreadsB, tp_requestA = tp_requestB, requestFinishedA = requestFinishedB, THREADPOOLSIZEA = THREADPOOLSIZEB, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B, MAX_QUEUE_LENGTH_A = MAX_QUEUE_LENGTH_B, TIMEOUTA = TIMEOUTB] endmodule
module SimulationStatistics_B = SimulationStatistics_A [metric_rejected_A = metric_rejected_B, metric_timeout_A = metric_timeout_B, metric_successfull_number_A = metric_successfull_number_B,
requestA_reject = requestB_reject, activeThreadsA = activeThreadsB, tp_requestA = tp_requestB, requestFinishedA = requestFinishedB, THREADPOOLSIZEA = THREADPOOLSIZEB, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B, MAX_QUEUE_LENGTH_A = MAX_QUEUE_LENGTH_B, TIMEOUTA = TIMEOUTB] endmodule
// ARRIVAL RATES
module SimulationDriverA
sd_finished_A : bool init false;
sd_requestA : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
// Generate or not, Poisson Process
[] !end & !sd_finished_A -> (1-pow(e,-1/MEAN_ARRIVAL_INTERVALL_A)) : (sd_requestA' = time)&(sd_finished_A' = true) + (pow(e,-1/MEAN_ARRIVAL_INTERVALL_A)) : (sd_finished_A' = true);
[overtakeThreadPoolA] !end & true -> (sd_requestA' = -1);
[endRound] !end & sd_finished_A & sd_requestA = -1 = true -> (sd_finished_A' = false);
endmodule
module SimulationDriverB = SimulationDriverA [sd_finished_A = sd_finished_B, sd_requestA = sd_requestB, overtakeThreadPoolA = overtakeThreadPoolB, MEAN_ARRIVAL_INTERVALL_A = MEAN_ARRIVAL_INTERVALL_B] endmodule
// LATENCY
module LatencyController
lc_latent_server : [0..SERVER_LATENCY_DURATION] init 0;
lc_latent_A : [0..LATENCY_DURATION_A] init 0;
lc_latent_B : [0..LATENCY_DURATION_B] init 0;
steps : [0..3] init 0;
[] !end & steps = 0 -> (1-pow(e,-1/SERVER_LATENCY_MEAN_INTERVALL)) : (lc_latent_server' = SERVER_LATENCY_DURATION)&(steps' = 1) + (pow(e,-1/SERVER_LATENCY_MEAN_INTERVALL)) : (steps' = 1);
[] !end & steps = 1 -> (1-pow(e,-1/LATENCY_MEAN_INTERVALL_A)) : (lc_latent_A' = LATENCY_DURATION_A)&(steps' = 2) + (pow(e,-1/LATENCY_MEAN_INTERVALL_A)) : (steps' = 2);
[] !end & steps = 2 -> (1-pow(e,-1/LATENCY_MEAN_INTERVALL_B)) : (lc_latent_B' = LATENCY_DURATION_B)&(steps' = 3) + (pow(e,-1/LATENCY_MEAN_INTERVALL_B)) : (steps' = 3);
[endRound] !end & steps = 3 -> (lc_latent_server' = max(lc_latent_server-1,0)) & (lc_latent_A' = max(lc_latent_A-1,0)) & (lc_latent_B' = max(lc_latent_B-1,0)) & (steps' = 0) ;
endmodule
// THREAD POOL
module ThreadPoolA
tp_requestA : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
[overtakeThreadPoolA] !end & sd_requestA = time -> (tp_requestA' = sd_requestA);
[overtakeQueueA] !end & true -> (tp_requestA' = -1);
[requestA_reject] !end & true -> (tp_requestA' = -1);
[endRound] !end & tp_requestA = -1 -> true;
endmodule
module ThreadPoolB = ThreadPoolA [tp_requestA = tp_requestB, sd_requestA = sd_requestB, overtakeThreadPoolA = overtakeThreadPoolB, overtakeQueueA = overtakeQueueB, requestA_reject = requestB_reject] endmodule
// QUEUE FOR COMP A
module Queue_A_IN
qain_request : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
qain_handleNewRequest : bool init false;
[overtakeQueueA] !end & qain_request = -1 & tp_requestA != -1 -> (qain_request'=tp_requestA) & (qain_handleNewRequest' = true);
[] !end & qain_handleNewRequest = true -> (CURRENT_QUEUE_LENGTH_A' = CURRENT_QUEUE_LENGTH_A + 1) & (qain_handleNewRequest' = false);
[overtakeQueuePreviousA_2] !end & !qain_handleNewRequest -> (qain_request' = -1);
[endRound] !end & !qain_handleNewRequest -> true;
endmodule
module Queue_A_2
qa2_request : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
[overtakeQueuePreviousA_2] !end & qa2_request = -1 & qain_request != -1 & CURRENT_QUEUE_LENGTH_A > 0 -> (qa2_request' = qain_request); // I pull the next value
[overtakeQueuePreviousA_3] !end & qa2_request != -1 -> (qa2_request' = -1); // Previous one pulled the next value
[endRound] !end & CURRENT_QUEUE_LENGTH_A = 0 | qa2_request != -1 | (qa2_request = -1 & qain_request = -1) -> true;
endmodule
module Queue_A_3 = Queue_A_2 [qa2_request = qa3_request, qain_request = qa2_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_3, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_4] endmodule
module Queue_A_4 = Queue_A_2 [qa2_request = qa4_request, qain_request = qa3_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_4, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_5] endmodule
module Queue_A_5 = Queue_A_2 [qa2_request = qa5_request, qain_request = qa4_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_5, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_6] endmodule
module Queue_A_6 = Queue_A_2 [qa2_request = qa6_request, qain_request = qa5_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_6, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_7] endmodule
module Queue_A_7 = Queue_A_2 [qa2_request = qa7_request, qain_request = qa6_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_7, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_8] endmodule
module Queue_A_8 = Queue_A_2 [qa2_request = qa8_request, qain_request = qa7_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_8, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_9] endmodule
module Queue_A_9 = Queue_A_2 [qa2_request = qa9_request, qain_request = qa8_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousA_9, overtakeQueuePreviousA_3 = overtakeQueuePreviousA_out] endmodule
module Queue_A_out
qaout_request : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
[overtakeQueuePreviousA_out] !end & qaout_request = -1 & qa9_request != -1 & CURRENT_QUEUE_LENGTH_A > 0 -> (qaout_request' = qa9_request); // I pull the next value
[] !end & THREAD_TOOK_INPUT_A -> (qaout_request' = -1) & (THREAD_TOOK_INPUT_A' = false) & (CURRENT_QUEUE_LENGTH_A' = CURRENT_QUEUE_LENGTH_A -1);
[endRound] !end & !THREAD_TOOK_INPUT_A & !(CURRENT_QUEUE_LENGTH_A > 0 & qaout_request = -1) -> true;
endmodule
// QUEUE FOR COMP B
module Queue_B_IN = Queue_A_IN [qain_request = qbin_request, qain_handleNewRequest = qbin_handleNewRequest, overtakeQueueA = overtakeQueueB, tp_requestA = tp_requestB, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_2] endmodule
module Queue_B_2 = Queue_A_2 [qa2_request = qb2_request, qain_request = qbin_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_2, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_3, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_3 = Queue_A_2 [qa2_request = qb3_request, qain_request = qb2_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_3, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_4, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_4 = Queue_A_2 [qa2_request = qb4_request, qain_request = qb3_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_4, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_5, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_5 = Queue_A_2 [qa2_request = qb5_request, qain_request = qb4_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_5, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_6, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_6 = Queue_A_2 [qa2_request = qb6_request, qain_request = qb5_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_6, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_7, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_7 = Queue_A_2 [qa2_request = qb7_request, qain_request = qb6_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_7, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_8, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_8 = Queue_A_2 [qa2_request = qb8_request, qain_request = qb7_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_8, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_9, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_9 = Queue_A_2 [qa2_request = qb9_request, qain_request = qb8_request, overtakeQueuePreviousA_2 = overtakeQueuePreviousB_9, overtakeQueuePreviousA_3 = overtakeQueuePreviousB_out, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B] endmodule
module Queue_B_out = Queue_A_out [qaout_request = qbout_request, overtakeQueuePreviousA_out = overtakeQueuePreviousB_out, qa9_request = qb9_request, CURRENT_QUEUE_LENGTH_A = CURRENT_QUEUE_LENGTH_B, THREAD_TOOK_INPUT_A = THREAD_TOOK_INPUT_B] endmodule
// ONE THREADS FOR BOTH COMPONENTS! THERE MUST BE AT LEAST AS MANY THREADS AS SUM OF BOTH THREAD POOLS!
module Thread1
t1_component : [0..2] init 0; // 0 is unassigned, 1 is component A, 2 is component B
t1_init_A : [0..2] init 0; // 1 set basic values, 2 apply modifiers
t1_init_B : [0..2] init 0;
t1_request : [-1..SIMULATION_LENGTH_IN_MICROSECONDS] init -1;
t1_demandPerMicrosecond : [0..100] init 0;
t1_demandTotalRemaining : [0..max(DEMAND_PERCENT_A*BASE_PROCESSING_TIME_MICROSECOND_A, DEMAND_PERCENT_B*BASE_PROCESSING_TIME_MICROSECOND_B)] init 0;
// INPUT A
[] !end & t1_component = 0 & qaout_request != -1 & !THREAD_TOOK_INPUT_A & activeThreadsA < THREADPOOLSIZEA -> (t1_component' = 1) & (t1_request' = qaout_request) & (THREAD_TOOK_INPUT_A' = true) & (t1_init_A' = 1) & (activeThreadsA' = activeThreadsA +1);
[] !end & t1_init_A = 1 -> (t1_demandPerMicrosecond' = DEMAND_PERCENT_A) & (t1_demandTotalRemaining' = DEMAND_PERCENT_A * BASE_PROCESSING_TIME_MICROSECOND_A) & (t1_init_A' = 2) & (total_demand_percent' = total_demand_percent + DEMAND_PERCENT_A);
[] !end & t1_init_A = 2 -> EASY_TASK_PROBABILITY_A : (t1_demandTotalRemaining' = ceil(t1_demandTotalRemaining * EASY_TASK_MODIFIER_A)) & (t1_init_A' = 0) + DIFFICULT_TASK_PROBABILITY_A : (t1_demandTotalRemaining' = ceil(t1_demandTotalRemaining * DIFFICULT_TASK_MODIFIER_A)) & (t1_init_A' = 0) + (1-DIFFICULT_TASK_PROBABILITY_A-EASY_TASK_PROBABILITY_A) : (t1_init_A' = 0);
// INPUT B TODO!
[] !end & t1_component = 0 & qbout_request != -1 & !THREAD_TOOK_INPUT_B & activeThreadsB < THREADPOOLSIZEB -> (t1_component' = 2) & (t1_request' = qbout_request) & (THREAD_TOOK_INPUT_B' = true) & (t1_init_B' = 1) & (activeThreadsB' = activeThreadsB +1);
[] !end & t1_init_B = 1 -> (t1_demandPerMicrosecond' = DEMAND_PERCENT_B) & (t1_demandTotalRemaining' = DEMAND_PERCENT_B * BASE_PROCESSING_TIME_MICROSECOND_B) & (t1_init_B' = 2) & (total_demand_percent' = total_demand_percent + DEMAND_PERCENT_B);
[] !end & t1_init_B = 2 -> EASY_TASK_PROBABILITY_B : (t1_demandTotalRemaining' = ceil(t1_demandTotalRemaining * EASY_TASK_MODIFIER_B)) & (t1_init_B' = 0) + DIFFICULT_TASK_PROBABILITY_B : (t1_demandTotalRemaining' = ceil(t1_demandTotalRemaining * DIFFICULT_TASK_MODIFIER_B)) & (t1_init_B' = 0) + (1-DIFFICULT_TASK_PROBABILITY_B-EASY_TASK_PROBABILITY_B) : (t1_init_B' = 0);
// FINISHED HANDLING
[] !end & t1_component = 1 & t1_init_A = 0 & t1_demandTotalRemaining = 0 & (requestFinishedA=-1) -> (requestFinishedA'=t1_request) & (t1_request'=-1) & (t1_component'=0) & (t1_demandPerMicrosecond'=0) & (t1_demandTotalRemaining'=0) & (activeThreadsA'=activeThreadsA-1) & (total_demand_percent'=total_demand_percent-t1_demandPerMicrosecond);
[] !end & t1_component = 2 & t1_init_B = 0 & t1_demandTotalRemaining = 0 & (requestFinishedB=-1) -> (requestFinishedB'=t1_request) & (t1_request'=-1) & (t1_component'=0) & (t1_demandPerMicrosecond'=0) & (t1_demandTotalRemaining'=0) & (activeThreadsB'=activeThreadsB-1) & (total_demand_percent'=total_demand_percent-t1_demandPerMicrosecond);
// COMPUTE
[endRound] !end & t1_init_A = 0 & t1_init_B = 0 & !(t1_component != 0 & t1_demandTotalRemaining = 0) -> (t1_demandTotalRemaining' = max(t1_demandTotalRemaining - max(floor(((t1_component = 1 & lc_latent_A > 0) ? LATENCY_MODIFIER_A : 1.0)*((t1_component = 2 & lc_latent_B > 0) ? LATENCY_MODIFIER_B : 1.0)*((lc_latent_server > 0) ? SERVER_LATENCY_MODIFIER : 1.0)*pow(MANY_THREADS_PENALTY, activeThreadsA+activeThreadsB-1) * min(MAX_AVAILABLE_DEMAND_PERCENT/total_demand_percent,1) * t1_demandPerMicrosecond),1),0));
endmodule
module Thread2 = Thread1 [t1_component = t2_component, t1_init_A = t2_init_A, t1_init_B = t2_init_B, t1_request = t2_request, t1_demandPerMicrosecond = t2_demandPerMicrosecond, t1_demandTotalRemaining = t2_demandTotalRemaining] endmodule
module Thread3 = Thread1 [t1_component = t3_component, t1_init_A = t3_init_A, t1_init_B = t3_init_B, t1_request = t3_request, t1_demandPerMicrosecond = t3_demandPerMicrosecond, t1_demandTotalRemaining = t3_demandTotalRemaining] endmodule
module Thread4 = Thread1 [t1_component = t4_component, t1_init_A = t4_init_A, t1_init_B = t4_init_B, t1_request = t4_request, t1_demandPerMicrosecond = t4_demandPerMicrosecond, t1_demandTotalRemaining = t4_demandTotalRemaining] endmodule
module Thread5 = Thread1 [t1_component = t5_component, t1_init_A = t5_init_A, t1_init_B = t5_init_B, t1_request = t5_request, t1_demandPerMicrosecond = t5_demandPerMicrosecond, t1_demandTotalRemaining = t5_demandTotalRemaining] endmodule
module Thread6 = Thread1 [t1_component = t6_component, t1_init_A = t6_init_A, t1_init_B = t6_init_B, t1_request = t6_request, t1_demandPerMicrosecond = t6_demandPerMicrosecond, t1_demandTotalRemaining = t6_demandTotalRemaining] endmodule
module Thread7 = Thread1 [t1_component = t7_component, t1_init_A = t7_init_A, t1_init_B = t7_init_B, t1_request = t7_request, t1_demandPerMicrosecond = t7_demandPerMicrosecond, t1_demandTotalRemaining = t7_demandTotalRemaining] endmodule
module Thread8 = Thread1 [t1_component = t8_component, t1_init_A = t8_init_A, t1_init_B = t8_init_B, t1_request = t8_request, t1_demandPerMicrosecond = t8_demandPerMicrosecond, t1_demandTotalRemaining = t8_demandTotalRemaining] endmodule
module Thread9 = Thread1 [t1_component = t9_component, t1_init_A = t9_init_A, t1_init_B = t9_init_B, t1_request = t9_request, t1_demandPerMicrosecond = t9_demandPerMicrosecond, t1_demandTotalRemaining = t9_demandTotalRemaining] endmodule
module Thread10 = Thread1 [t1_component = t10_component, t1_init_A = t10_init_A, t1_init_B = t10_init_B, t1_request = t10_request, t1_demandPerMicrosecond = t10_demandPerMicrosecond, t1_demandTotalRemaining = t10_demandTotalRemaining] endmodule
module Thread11 = Thread1 [t1_component = t11_component, t1_init_A = t11_init_A, t1_init_B = t11_init_B, t1_request = t11_request, t1_demandPerMicrosecond = t11_demandPerMicrosecond, t1_demandTotalRemaining = t11_demandTotalRemaining] endmodule
module Thread12 = Thread1 [t1_component = t12_component, t1_init_A = t12_init_A, t1_init_B = t12_init_B, t1_request = t12_request, t1_demandPerMicrosecond = t12_demandPerMicrosecond, t1_demandTotalRemaining = t12_demandTotalRemaining] endmodule
module Thread13 = Thread1 [t1_component = t13_component, t1_init_A = t13_init_A, t1_init_B = t13_init_B, t1_request = t13_request, t1_demandPerMicrosecond = t13_demandPerMicrosecond, t1_demandTotalRemaining = t13_demandTotalRemaining] endmodule
module Thread14 = Thread1 [t1_component = t14_component, t1_init_A = t14_init_A, t1_init_B = t14_init_B, t1_request = t14_request, t1_demandPerMicrosecond = t14_demandPerMicrosecond, t1_demandTotalRemaining = t14_demandTotalRemaining] endmodule
module Thread15 = Thread1 [t1_component = t15_component, t1_init_A = t15_init_A, t1_init_B = t15_init_B, t1_request = t15_request, t1_demandPerMicrosecond = t15_demandPerMicrosecond, t1_demandTotalRemaining = t15_demandTotalRemaining] endmodule
module Thread16 = Thread1 [t1_component = t16_component, t1_init_A = t16_init_A, t1_init_B = t16_init_B, t1_request = t16_request, t1_demandPerMicrosecond = t16_demandPerMicrosecond, t1_demandTotalRemaining = t16_demandTotalRemaining] endmodule