@@ -222,7 +222,6 @@ class ResourcePeriodicallyUnavailable(ResourceConstraint):
222
222
offset : int = 0
223
223
end : Union [int , None ] = None
224
224
225
-
226
225
def __init__ (self , ** data ):
227
226
"""
228
227
Initialize a ResourceUnavailable constraint.
@@ -254,8 +253,10 @@ def __init__(self, **data):
254
253
duration = end_task_i - start_task_i
255
254
conds = [
256
255
z3 .Xor (
257
- (start_task_i - self .offset ) % self .period >= interval_upper_bound ,
258
- (start_task_i - self .offset ) % self .period + duration <= interval_lower_bound
256
+ (start_task_i - self .offset ) % self .period
257
+ >= interval_upper_bound ,
258
+ (start_task_i - self .offset ) % self .period + duration
259
+ <= interval_lower_bound ,
259
260
)
260
261
]
261
262
@@ -315,46 +316,51 @@ def __init__(self, **data) -> None:
315
316
316
317
is_interruptible = isinstance (task , VariableDurationTask )
317
318
318
- for interval_lower_bound , interval_upper_bound in self .list_of_time_intervals :
319
- overlap_condition = z3 .Not (z3 .Xor (
320
- start_task_i >= interval_upper_bound ,
321
- end_task_i <= interval_lower_bound
322
- ))
319
+ for (
320
+ interval_lower_bound ,
321
+ interval_upper_bound ,
322
+ ) in self .list_of_time_intervals :
323
+ overlap_condition = z3 .Not (
324
+ z3 .Xor (
325
+ start_task_i >= interval_upper_bound ,
326
+ end_task_i <= interval_lower_bound ,
327
+ )
328
+ )
323
329
overlap = z3 .If (
324
330
overlap_condition ,
325
331
interval_upper_bound - interval_lower_bound ,
326
- 0
332
+ 0 ,
327
333
)
328
334
overlaps .append (overlap )
329
335
330
336
if is_interruptible :
331
337
# just make sure that the task does not start or end within the time interval...
332
338
# TODO: account for zero-duration?
333
- conds .extend ([
334
- z3 .Xor (
335
- start_task_i <= interval_lower_bound ,
336
- start_task_i >= interval_upper_bound
337
- ),
338
- z3 .Xor (
339
- end_task_i <= interval_lower_bound ,
340
- end_task_i >= interval_upper_bound
341
- )
342
- ])
339
+ conds .extend (
340
+ [
341
+ z3 .Xor (
342
+ start_task_i <= interval_lower_bound ,
343
+ start_task_i >= interval_upper_bound ,
344
+ ),
345
+ z3 .Xor (
346
+ end_task_i <= interval_lower_bound ,
347
+ end_task_i >= interval_upper_bound ,
348
+ ),
349
+ ]
350
+ )
343
351
else :
344
352
# ...otherwise make sure the task does not overlap with the time interval
345
353
conds .append (
346
354
z3 .Xor (
347
355
start_task_i >= interval_upper_bound ,
348
- end_task_i <= interval_lower_bound
356
+ end_task_i <= interval_lower_bound ,
349
357
)
350
358
)
351
359
352
360
if is_interruptible :
353
361
# add assertions for task duration based on the total count of overlapped periods
354
362
total_overlap = z3 .Sum (* overlaps )
355
- conds .append (
356
- task ._duration >= task .min_duration + total_overlap
357
- )
363
+ conds .append (task ._duration >= task .min_duration + total_overlap )
358
364
if task .max_duration is not None :
359
365
conds .append (
360
366
task ._duration <= task .max_duration + total_overlap
@@ -432,74 +438,84 @@ def __init__(self, **data) -> None:
432
438
folded_start_task_i = (start_task_i - self .offset ) % self .period
433
439
folded_end_task_i = (end_task_i - self .offset ) % self .period
434
440
435
- for interval_lower_bound , interval_upper_bound in self .list_of_time_intervals :
441
+ for (
442
+ interval_lower_bound ,
443
+ interval_upper_bound ,
444
+ ) in self .list_of_time_intervals :
436
445
# intervals need to be defined in one period
437
446
if interval_upper_bound > self .period :
438
- raise AssertionError (f"interval ({ interval_lower_bound } , { interval_upper_bound } ) exceeds period { self .period } " )
447
+ raise AssertionError (
448
+ f"interval ({ interval_lower_bound } , { interval_upper_bound } ) exceeds period { self .period } "
449
+ )
439
450
440
451
# if true, the folded task overlaps with the time interval in the first period
441
- crossing_condition = z3 .Not (z3 .Xor (
442
- # folded task is completely before the first time interval
443
- z3 .And (
444
- folded_start_task_i <= interval_lower_bound ,
445
- folded_start_task_i + duration % self .period <= interval_lower_bound ,
446
- ),
447
- # folded task is completely between the first and second time interval
448
- z3 .And (
449
- folded_start_task_i >= interval_upper_bound ,
450
- folded_start_task_i + duration % self .period <= interval_lower_bound + self .period ,
452
+ crossing_condition = z3 .Not (
453
+ z3 .Xor (
454
+ # folded task is completely before the first time interval
455
+ z3 .And (
456
+ folded_start_task_i <= interval_lower_bound ,
457
+ folded_start_task_i + duration % self .period
458
+ <= interval_lower_bound ,
459
+ ),
460
+ # folded task is completely between the first and second time interval
461
+ z3 .And (
462
+ folded_start_task_i >= interval_upper_bound ,
463
+ folded_start_task_i + duration % self .period
464
+ <= interval_lower_bound + self .period ,
465
+ ),
451
466
)
452
- ))
467
+ )
453
468
454
469
# if true, the task overlaps with at least one time interval
455
470
overlap_condition = z3 .Or (
456
471
crossing_condition ,
457
472
# task does not fit between two intervals
458
- duration > interval_lower_bound + self .period - interval_upper_bound
473
+ duration
474
+ > interval_lower_bound + self .period - interval_upper_bound ,
459
475
)
460
476
461
477
# adjust the number of crossed time intervals
462
478
crossings = z3 .If (
463
479
crossing_condition ,
464
480
duration / self .period + 1 ,
465
- duration / self .period
481
+ duration / self .period ,
466
482
)
467
483
# calculate the total overlap for this particular time interval
468
484
overlap = z3 .If (
469
485
overlap_condition ,
470
486
(interval_upper_bound - interval_lower_bound ) * crossings ,
471
- 0
487
+ 0 ,
472
488
)
473
489
overlaps .append (overlap )
474
490
475
491
if is_interruptible :
476
492
# just make sure that the task does not start or end within one of the time intervals...
477
493
# TODO: account for zero-duration?
478
- conds .extend ([
479
- z3 .Xor (
480
- folded_start_task_i <= interval_lower_bound ,
481
- folded_start_task_i >= interval_upper_bound
482
- ),
483
- z3 .Xor (
484
- folded_end_task_i <= interval_lower_bound ,
485
- folded_end_task_i >= interval_upper_bound
486
- )
487
- ])
494
+ conds .extend (
495
+ [
496
+ z3 .Xor (
497
+ folded_start_task_i <= interval_lower_bound ,
498
+ folded_start_task_i >= interval_upper_bound ,
499
+ ),
500
+ z3 .Xor (
501
+ folded_end_task_i <= interval_lower_bound ,
502
+ folded_end_task_i >= interval_upper_bound ,
503
+ ),
504
+ ]
505
+ )
488
506
else :
489
507
# ...otherwise make sure the task does not overlap with any of time intervals
490
508
conds .append (
491
509
z3 .Xor (
492
510
folded_start_task_i >= interval_upper_bound ,
493
- folded_start_task_i + duration <= interval_lower_bound
511
+ folded_start_task_i + duration <= interval_lower_bound ,
494
512
)
495
513
)
496
514
497
515
if is_interruptible :
498
516
# add assertions for task duration based on the total count of overlapped periods
499
517
total_overlap = z3 .Sum (* overlaps )
500
- conds .append (
501
- task ._duration >= task .min_duration + total_overlap
502
- )
518
+ conds .append (task ._duration >= task .min_duration + total_overlap )
503
519
if task .max_duration is not None :
504
520
conds .append (
505
521
task ._duration <= task .max_duration + total_overlap
0 commit comments