From e8650107f10d9a5f533e9c252b1ac32fa85ea986 Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 07:01:09 +0100 Subject: [PATCH 1/9] Add FixedDurationInterruptibleTask --- processscheduler/__init__.py | 1 + processscheduler/resource_constraint.py | 14 +++++--- processscheduler/task.py | 16 +++++++++ processscheduler/task_constraint.py | 46 +++++++++++++------------ 4 files changed, 51 insertions(+), 26 deletions(-) diff --git a/processscheduler/__init__.py b/processscheduler/__init__.py index 691699b0..5ecaaa64 100644 --- a/processscheduler/__init__.py +++ b/processscheduler/__init__.py @@ -56,6 +56,7 @@ ZeroDurationTask, FixedDurationTask, VariableDurationTask, + FixedDurationInterruptibleTask, ) from processscheduler.constraint import * from processscheduler.task_constraint import * diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 1ba1023d..78861b68 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -25,7 +25,7 @@ from processscheduler.resource import Worker, CumulativeWorker, SelectWorkers from processscheduler.constraint import ResourceConstraint from processscheduler.util import sort_no_duplicates -from processscheduler.task import VariableDurationTask +from processscheduler.task import VariableDurationTask, FixedDurationInterruptibleTask, Task class WorkLoad(ResourceConstraint): @@ -427,6 +427,7 @@ def __init__(self, **data) -> None: # check if the task allows variable duration is_interruptible = isinstance(task, VariableDurationTask) + is_fixed_interruptible = isinstance(task, FixedDurationInterruptibleTask) duration = end_task_i - start_task_i folded_start_task_i = (start_task_i - self.offset) % self.period @@ -472,17 +473,17 @@ def __init__(self, **data) -> None: ) overlaps.append(overlap) - if is_interruptible: + if is_interruptible or is_fixed_interruptible: # just make sure that the task does not start or end within one of the time intervals... # TODO: account for zero-duration? conds.extend([ z3.Xor( - folded_start_task_i <= interval_lower_bound, + folded_start_task_i < interval_lower_bound, folded_start_task_i >= interval_upper_bound ), z3.Xor( folded_end_task_i <= interval_lower_bound, - folded_end_task_i >= interval_upper_bound + folded_end_task_i > interval_upper_bound ) ]) else: @@ -504,6 +505,11 @@ def __init__(self, **data) -> None: conds.append( task._duration <= task.max_duration + total_overlap ) + elif is_fixed_interruptible: + total_overlap = z3.Sum(*overlaps) + conds.append( + task._overlap == total_overlap + ) # TODO: add AND only of mask is set? core = z3.And(*conds) diff --git a/processscheduler/task.py b/processscheduler/task.py index 6220f72a..a4e4d07e 100644 --- a/processscheduler/task.py +++ b/processscheduler/task.py @@ -268,6 +268,22 @@ def __init__(self, **data) -> None: self.set_assertions(assertions) +class FixedDurationInterruptibleTask(Task): + + duration: PositiveInt + + def __init__(self, **data) -> None: + super().__init__(**data) + self._overlap = z3.Int(f"{self.name}_overlap") + assertions = [ + self._end - self._start == self.duration + self._overlap, + self._start >= 0, + self._overlap >= 0 + ] + + self.set_assertions(assertions) + + class VariableDurationTask(Task): """The duration can take any value, computed by the solver.""" diff --git a/processscheduler/task_constraint.py b/processscheduler/task_constraint.py index f4cb97c2..199ff946 100644 --- a/processscheduler/task_constraint.py +++ b/processscheduler/task_constraint.py @@ -27,6 +27,8 @@ FixedDurationTask, ZeroDurationTask, VariableDurationTask, + FixedDurationInterruptibleTask, + Task ) from processscheduler.buffer import ConcurrentBuffer, NonConcurrentBuffer from processscheduler.util import sort_no_duplicates @@ -37,7 +39,7 @@ # class TaskGroup(TaskConstraint): list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] ] time_interval: Tuple[int, int] = Field(default=None) time_interval_length: int = Field(default=0) @@ -107,10 +109,10 @@ class TaskPrecedence(TaskConstraint): """Task precedence relation""" task_before: Union[ - FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup + FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup, FixedDurationInterruptibleTask, Task ] task_after: Union[ - FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup + FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup, FixedDurationInterruptibleTask, Task ] offset: int = Field(default=0, ge=0) kind: Literal["lax", "strict", "tight"] = Field(default="lax") @@ -154,8 +156,8 @@ def __init__(self, **data) -> None: class TasksStartSynced(TaskConstraint): """Two tasks that must start at the same time""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] def __init__(self, **data) -> None: super().__init__(**data) @@ -177,8 +179,8 @@ def __init__(self, **data) -> None: class TasksEndSynced(TaskConstraint): """Two tasks that must complete at the same time""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] def __init__(self, **data) -> None: super().__init__(**data) @@ -201,8 +203,8 @@ class TasksDontOverlap(TaskConstraint): """Two tasks must not overlap, i.e. one needs to be completed before the other can be processed""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] def __init__(self, **data) -> None: super().__init__(**data) @@ -228,7 +230,7 @@ class TasksContiguous(TaskConstraint): """A list of tasks are scheduled contiguously.""" list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] ] def __init__(self, **data) -> None: @@ -261,7 +263,7 @@ def __init__(self, **data) -> None: class TaskStartAt(TaskConstraint): """One task must start at the desired time""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] value: Union[int, z3.ArithRef] def __init__(self, **data) -> None: @@ -278,7 +280,7 @@ def __init__(self, **data) -> None: class TaskStartAfter(TaskConstraint): - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] value: Union[int, z3.ArithRef] kind: Literal["lax", "strict"] = Field(default="lax") @@ -301,7 +303,7 @@ def __init__(self, **data) -> None: class TaskEndAt(TaskConstraint): """On task must complete at the desired time""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] value: Union[int, z3.ArithRef] def __init__(self, **data) -> None: @@ -320,7 +322,7 @@ def __init__(self, **data) -> None: class TaskEndBefore(TaskConstraint): """task.end < value""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] value: Union[int, z3.ArithRef] kind: Literal["lax", "strict"] = Field(default="lax") @@ -346,7 +348,7 @@ def __init__(self, **data) -> None: class OptionalTaskForceSchedule(TaskConstraint): """task_2 is scheduled if and only if task_1 is scheduled""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] to_be_scheduled: bool def __init__(self, **data) -> None: @@ -361,7 +363,7 @@ def __init__(self, **data) -> None: class OptionalTaskConditionSchedule(TaskConstraint): """An optional task that is scheduled only if a condition is fulfilled.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] condition: z3.BoolRef def __init__(self, **data) -> None: @@ -382,8 +384,8 @@ def __init__(self, **data) -> None: class OptionalTasksDependency(TaskConstraint): """task_2 is scheduled if and only if task_1 is scheduled""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] def __init__(self, **data) -> None: super().__init__(**data) @@ -399,7 +401,7 @@ class ForceScheduleNOptionalTasks(TaskConstraint): at at least/at most/exactly n tasks, with 0 < n <= m.""" list_of_optional_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] ] nb_tasks_to_schedule: PositiveInt = Field(default=1) kind: Literal["min", "max", "exact"] = Field(default="exact") @@ -429,7 +431,7 @@ class ScheduleNTasksInTimeIntervals(TaskConstraint): in this time interval""" list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] ] nb_tasks_to_schedule: int list_of_time_intervals: List[Tuple[int, int]] @@ -487,7 +489,7 @@ class TaskUnloadBuffer(TaskConstraint): """A tasks that unloads a buffer, i.e. that takes one or more quantity units to the buffer.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] buffer: Union[NonConcurrentBuffer, ConcurrentBuffer] quantity: int @@ -501,7 +503,7 @@ class TaskLoadBuffer(TaskConstraint): """A task that loads a buffer, i.e. a that adds one or more quantity unis to the buffer.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask] + task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] buffer: Union[NonConcurrentBuffer, ConcurrentBuffer] quantity: int From 285d33f01c427d3cb0722e9670ed7f472afe343e Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 07:03:37 +0100 Subject: [PATCH 2/9] Fix typo in reference to _cumulative_workers resource attribute --- processscheduler/resource_constraint.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 78861b68..13a3f18f 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -176,7 +176,7 @@ def __init__(self, **data) -> None: if isinstance(self.resource, Worker): workers = [self.resource] elif isinstance(self.resource, CumulativeWorker): - workers = self.resource.cumulative_workers + workers = self.resource._cumulative_workers resource_assigned = False @@ -243,7 +243,7 @@ def __init__(self, **data): if isinstance(self.resource, Worker): workers = [self.resource] elif isinstance(self.resource, CumulativeWorker): - workers = self.resource.cumulative_workers + workers = self.resource._cumulative_workers resource_assigned = False @@ -303,7 +303,7 @@ def __init__(self, **data) -> None: if isinstance(self.resource, Worker): workers = [self.resource] elif isinstance(self.resource, CumulativeWorker): - workers = self.resource.cumulative_workers + workers = self.resource._cumulative_workers resource_assigned = False @@ -415,7 +415,7 @@ def __init__(self, **data) -> None: if isinstance(self.resource, Worker): workers = [self.resource] elif isinstance(self.resource, CumulativeWorker): - workers = self.resource.cumulative_workers + workers = self.resource._cumulative_workers resource_assigned = False From f718e76aa62cf5a0955b0dc5da05e75edacccbbd Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 07:15:54 +0100 Subject: [PATCH 3/9] Add check for FixedDurationInterruptibleTask to ResourceInterrupted --- processscheduler/resource_constraint.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 13a3f18f..3d63cde9 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -359,6 +359,11 @@ def __init__(self, **data) -> None: conds.append( task._duration <= task.max_duration + total_overlap ) + elif is_fixed_interruptible: + total_overlap = z3.Sum(*overlaps) + conds.append( + task._overlap == total_overlap + ) # TODO: remove AND, as the solver does that anyways? self.set_z3_assertions(z3.And(*conds)) From 73fc422d3a5a68a409055bad2d2e21b4fa99ec9d Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 07:16:46 +0100 Subject: [PATCH 4/9] Adjust start and end assertions and remove TODO about zero-duration tasks --- processscheduler/resource_constraint.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 3d63cde9..a611bd5c 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -329,15 +329,14 @@ def __init__(self, **data) -> None: if is_interruptible: # just make sure that the task does not start or end within the time interval... - # TODO: account for zero-duration? conds.extend([ z3.Xor( - start_task_i <= interval_lower_bound, + start_task_i < interval_lower_bound, start_task_i >= interval_upper_bound ), z3.Xor( end_task_i <= interval_lower_bound, - end_task_i >= interval_upper_bound + end_task_i > interval_upper_bound ) ]) else: @@ -480,7 +479,6 @@ def __init__(self, **data) -> None: if is_interruptible or is_fixed_interruptible: # just make sure that the task does not start or end within one of the time intervals... - # TODO: account for zero-duration? conds.extend([ z3.Xor( folded_start_task_i < interval_lower_bound, From 4c93c87a9a1c47ca29b0e4f39d723cfacc2ea3ad Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 07:20:12 +0100 Subject: [PATCH 5/9] Fix missing boolean for FixedDurationInterruptibleTask in ResourceInterruptible --- processscheduler/resource_constraint.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index a611bd5c..50e94989 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -314,6 +314,7 @@ def __init__(self, **data) -> None: overlaps = [] is_interruptible = isinstance(task, VariableDurationTask) + is_fixed_interruptible = isinstance(task, FixedDurationInterruptibleTask) for interval_lower_bound, interval_upper_bound in self.list_of_time_intervals: overlap_condition = z3.Not(z3.Xor( @@ -433,6 +434,7 @@ def __init__(self, **data) -> None: is_interruptible = isinstance(task, VariableDurationTask) is_fixed_interruptible = isinstance(task, FixedDurationInterruptibleTask) + duration = end_task_i - start_task_i folded_start_task_i = (start_task_i - self.offset) % self.period folded_end_task_i = (end_task_i - self.offset) % self.period From 749a810cdcfb623899aca41c1f24d2a8171f0735 Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 20:19:09 +0100 Subject: [PATCH 6/9] Apply black formatting --- processscheduler/resource_constraint.py | 145 ++++++++++++---------- processscheduler/task.py | 11 +- processscheduler/task_constraint.py | 156 ++++++++++++++++++++---- 3 files changed, 222 insertions(+), 90 deletions(-) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 50e94989..c978a866 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -25,7 +25,11 @@ from processscheduler.resource import Worker, CumulativeWorker, SelectWorkers from processscheduler.constraint import ResourceConstraint from processscheduler.util import sort_no_duplicates -from processscheduler.task import VariableDurationTask, FixedDurationInterruptibleTask, Task +from processscheduler.task import ( + VariableDurationTask, + FixedDurationInterruptibleTask, + Task, +) class WorkLoad(ResourceConstraint): @@ -222,7 +226,6 @@ class ResourcePeriodicallyUnavailable(ResourceConstraint): offset: int = 0 end: Union[int, None] = None - def __init__(self, **data): """ Initialize a ResourceUnavailable constraint. @@ -254,8 +257,10 @@ def __init__(self, **data): duration = end_task_i - start_task_i conds = [ z3.Xor( - (start_task_i - self.offset) % self.period >= interval_upper_bound, - (start_task_i - self.offset) % self.period + duration <= interval_lower_bound + (start_task_i - self.offset) % self.period + >= interval_upper_bound, + (start_task_i - self.offset) % self.period + duration + <= interval_lower_bound, ) ] @@ -314,56 +319,61 @@ def __init__(self, **data) -> None: overlaps = [] is_interruptible = isinstance(task, VariableDurationTask) - is_fixed_interruptible = isinstance(task, FixedDurationInterruptibleTask) + is_fixed_interruptible = isinstance( + task, FixedDurationInterruptibleTask + ) - for interval_lower_bound, interval_upper_bound in self.list_of_time_intervals: - overlap_condition = z3.Not(z3.Xor( - start_task_i >= interval_upper_bound, - end_task_i <= interval_lower_bound - )) + for ( + interval_lower_bound, + interval_upper_bound, + ) in self.list_of_time_intervals: + overlap_condition = z3.Not( + z3.Xor( + start_task_i >= interval_upper_bound, + end_task_i <= interval_lower_bound, + ) + ) overlap = z3.If( overlap_condition, interval_upper_bound - interval_lower_bound, - 0 + 0, ) overlaps.append(overlap) if is_interruptible: # just make sure that the task does not start or end within the time interval... - conds.extend([ - z3.Xor( - start_task_i < interval_lower_bound, - start_task_i >= interval_upper_bound - ), - z3.Xor( - end_task_i <= interval_lower_bound, - end_task_i > interval_upper_bound - ) - ]) + conds.extend( + [ + z3.Xor( + start_task_i < interval_lower_bound, + start_task_i >= interval_upper_bound, + ), + z3.Xor( + end_task_i <= interval_lower_bound, + end_task_i > interval_upper_bound, + ), + ] + ) else: # ...otherwise make sure the task does not overlap with the time interval conds.append( z3.Xor( start_task_i >= interval_upper_bound, - end_task_i <= interval_lower_bound + end_task_i <= interval_lower_bound, ) ) if is_interruptible: # add assertions for task duration based on the total count of overlapped periods total_overlap = z3.Sum(*overlaps) - conds.append( - task._duration >= task.min_duration + total_overlap - ) + conds.append(task._duration >= task.min_duration + total_overlap) if task.max_duration is not None: conds.append( task._duration <= task.max_duration + total_overlap ) elif is_fixed_interruptible: total_overlap = z3.Sum(*overlaps) - conds.append( - task._overlap == total_overlap - ) + conds.append(task._overlap == total_overlap) # TODO: remove AND, as the solver does that anyways? self.set_z3_assertions(z3.And(*conds)) @@ -432,89 +442,98 @@ def __init__(self, **data) -> None: # check if the task allows variable duration is_interruptible = isinstance(task, VariableDurationTask) - is_fixed_interruptible = isinstance(task, FixedDurationInterruptibleTask) - + is_fixed_interruptible = isinstance( + task, FixedDurationInterruptibleTask + ) duration = end_task_i - start_task_i folded_start_task_i = (start_task_i - self.offset) % self.period folded_end_task_i = (end_task_i - self.offset) % self.period - for interval_lower_bound, interval_upper_bound in self.list_of_time_intervals: + for ( + interval_lower_bound, + interval_upper_bound, + ) in self.list_of_time_intervals: # intervals need to be defined in one period if interval_upper_bound > self.period: - raise AssertionError(f"interval ({interval_lower_bound}, {interval_upper_bound}) exceeds period {self.period}") + raise AssertionError( + f"interval ({interval_lower_bound}, {interval_upper_bound}) exceeds period {self.period}" + ) # if true, the folded task overlaps with the time interval in the first period - crossing_condition = z3.Not(z3.Xor( - # folded task is completely before the first time interval - z3.And( - folded_start_task_i <= interval_lower_bound, - folded_start_task_i + duration % self.period <= interval_lower_bound, - ), - # folded task is completely between the first and second time interval - z3.And( - folded_start_task_i >= interval_upper_bound, - folded_start_task_i + duration % self.period <= interval_lower_bound + self.period, + crossing_condition = z3.Not( + z3.Xor( + # folded task is completely before the first time interval + z3.And( + folded_start_task_i <= interval_lower_bound, + folded_start_task_i + duration % self.period + <= interval_lower_bound, + ), + # folded task is completely between the first and second time interval + z3.And( + folded_start_task_i >= interval_upper_bound, + folded_start_task_i + duration % self.period + <= interval_lower_bound + self.period, + ), ) - )) + ) # if true, the task overlaps with at least one time interval overlap_condition = z3.Or( crossing_condition, # task does not fit between two intervals - duration > interval_lower_bound + self.period - interval_upper_bound + duration + > interval_lower_bound + self.period - interval_upper_bound, ) # adjust the number of crossed time intervals crossings = z3.If( crossing_condition, duration / self.period + 1, - duration / self.period + duration / self.period, ) # calculate the total overlap for this particular time interval overlap = z3.If( overlap_condition, (interval_upper_bound - interval_lower_bound) * crossings, - 0 + 0, ) overlaps.append(overlap) if is_interruptible or is_fixed_interruptible: # just make sure that the task does not start or end within one of the time intervals... - conds.extend([ - z3.Xor( - folded_start_task_i < interval_lower_bound, - folded_start_task_i >= interval_upper_bound - ), - z3.Xor( - folded_end_task_i <= interval_lower_bound, - folded_end_task_i > interval_upper_bound - ) - ]) + conds.extend( + [ + z3.Xor( + folded_start_task_i < interval_lower_bound, + folded_start_task_i >= interval_upper_bound, + ), + z3.Xor( + folded_end_task_i <= interval_lower_bound, + folded_end_task_i > interval_upper_bound, + ), + ] + ) else: # ...otherwise make sure the task does not overlap with any of time intervals conds.append( z3.Xor( folded_start_task_i >= interval_upper_bound, - folded_start_task_i + duration <= interval_lower_bound + folded_start_task_i + duration <= interval_lower_bound, ) ) if is_interruptible: # add assertions for task duration based on the total count of overlapped periods total_overlap = z3.Sum(*overlaps) - conds.append( - task._duration >= task.min_duration + total_overlap - ) + conds.append(task._duration >= task.min_duration + total_overlap) if task.max_duration is not None: conds.append( task._duration <= task.max_duration + total_overlap ) elif is_fixed_interruptible: total_overlap = z3.Sum(*overlaps) - conds.append( - task._overlap == total_overlap - ) + conds.append(task._overlap == total_overlap) # TODO: add AND only of mask is set? core = z3.And(*conds) diff --git a/processscheduler/task.py b/processscheduler/task.py index a4e4d07e..f1edf448 100644 --- a/processscheduler/task.py +++ b/processscheduler/task.py @@ -74,7 +74,9 @@ def __init__(self, **data) -> None: super().__init__(**data) # workers required to process the task - self._required_resources = [] # type: List[Union[Worker, CumulativeWorker, SelectWorkers]] + self._required_resources = ( + [] + ) # type: List[Union[Worker, CumulativeWorker, SelectWorkers]] # z3 Int variables self._start = z3.Int(f"{self.name}_start") # type: z3.ArithRef @@ -88,7 +90,9 @@ def __init__(self, **data) -> None: raise AssertionError("No active problem. First create a SchedulingProblem") # the task_number is an integer that is incremented each time # a task is created. The first task has number 1, the second number 2 etc. - self._task_number = processscheduler.base.active_problem.add_task(self) # type: int + self._task_number = processscheduler.base.active_problem.add_task( + self + ) # type: int # the release date if self.release_date is not None: @@ -269,7 +273,6 @@ def __init__(self, **data) -> None: class FixedDurationInterruptibleTask(Task): - duration: PositiveInt def __init__(self, **data) -> None: @@ -278,7 +281,7 @@ def __init__(self, **data) -> None: assertions = [ self._end - self._start == self.duration + self._overlap, self._start >= 0, - self._overlap >= 0 + self._overlap >= 0, ] self.set_assertions(assertions) diff --git a/processscheduler/task_constraint.py b/processscheduler/task_constraint.py index 199ff946..2d0d4c9e 100644 --- a/processscheduler/task_constraint.py +++ b/processscheduler/task_constraint.py @@ -28,7 +28,7 @@ ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask, - Task + Task, ) from processscheduler.buffer import ConcurrentBuffer, NonConcurrentBuffer from processscheduler.util import sort_no_duplicates @@ -39,7 +39,12 @@ # class TaskGroup(TaskConstraint): list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] ] time_interval: Tuple[int, int] = Field(default=None) time_interval_length: int = Field(default=0) @@ -109,10 +114,20 @@ class TaskPrecedence(TaskConstraint): """Task precedence relation""" task_before: Union[ - FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup, FixedDurationInterruptibleTask, Task + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + TaskGroup, + FixedDurationInterruptibleTask, + Task, ] task_after: Union[ - FixedDurationTask, ZeroDurationTask, VariableDurationTask, TaskGroup, FixedDurationInterruptibleTask, Task + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + TaskGroup, + FixedDurationInterruptibleTask, + Task, ] offset: int = Field(default=0, ge=0) kind: Literal["lax", "strict", "tight"] = Field(default="lax") @@ -156,8 +171,18 @@ def __init__(self, **data) -> None: class TasksStartSynced(TaskConstraint): """Two tasks that must start at the same time""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_1: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] + task_2: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] def __init__(self, **data) -> None: super().__init__(**data) @@ -179,8 +204,18 @@ def __init__(self, **data) -> None: class TasksEndSynced(TaskConstraint): """Two tasks that must complete at the same time""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_1: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] + task_2: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] def __init__(self, **data) -> None: super().__init__(**data) @@ -203,8 +238,18 @@ class TasksDontOverlap(TaskConstraint): """Two tasks must not overlap, i.e. one needs to be completed before the other can be processed""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_1: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] + task_2: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] def __init__(self, **data) -> None: super().__init__(**data) @@ -230,7 +275,12 @@ class TasksContiguous(TaskConstraint): """A list of tasks are scheduled contiguously.""" list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] ] def __init__(self, **data) -> None: @@ -263,7 +313,12 @@ def __init__(self, **data) -> None: class TaskStartAt(TaskConstraint): """One task must start at the desired time""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] value: Union[int, z3.ArithRef] def __init__(self, **data) -> None: @@ -280,7 +335,12 @@ def __init__(self, **data) -> None: class TaskStartAfter(TaskConstraint): - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] value: Union[int, z3.ArithRef] kind: Literal["lax", "strict"] = Field(default="lax") @@ -303,7 +363,12 @@ def __init__(self, **data) -> None: class TaskEndAt(TaskConstraint): """On task must complete at the desired time""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] value: Union[int, z3.ArithRef] def __init__(self, **data) -> None: @@ -322,7 +387,12 @@ def __init__(self, **data) -> None: class TaskEndBefore(TaskConstraint): """task.end < value""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] value: Union[int, z3.ArithRef] kind: Literal["lax", "strict"] = Field(default="lax") @@ -348,7 +418,12 @@ def __init__(self, **data) -> None: class OptionalTaskForceSchedule(TaskConstraint): """task_2 is scheduled if and only if task_1 is scheduled""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] to_be_scheduled: bool def __init__(self, **data) -> None: @@ -363,7 +438,12 @@ def __init__(self, **data) -> None: class OptionalTaskConditionSchedule(TaskConstraint): """An optional task that is scheduled only if a condition is fulfilled.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] condition: z3.BoolRef def __init__(self, **data) -> None: @@ -384,8 +464,18 @@ def __init__(self, **data) -> None: class OptionalTasksDependency(TaskConstraint): """task_2 is scheduled if and only if task_1 is scheduled""" - task_1: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] - task_2: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task_1: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] + task_2: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] def __init__(self, **data) -> None: super().__init__(**data) @@ -401,7 +491,12 @@ class ForceScheduleNOptionalTasks(TaskConstraint): at at least/at most/exactly n tasks, with 0 < n <= m.""" list_of_optional_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] ] nb_tasks_to_schedule: PositiveInt = Field(default=1) kind: Literal["min", "max", "exact"] = Field(default="exact") @@ -431,7 +526,12 @@ class ScheduleNTasksInTimeIntervals(TaskConstraint): in this time interval""" list_of_tasks: List[ - Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] ] nb_tasks_to_schedule: int list_of_time_intervals: List[Tuple[int, int]] @@ -489,7 +589,12 @@ class TaskUnloadBuffer(TaskConstraint): """A tasks that unloads a buffer, i.e. that takes one or more quantity units to the buffer.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] buffer: Union[NonConcurrentBuffer, ConcurrentBuffer] quantity: int @@ -503,7 +608,12 @@ class TaskLoadBuffer(TaskConstraint): """A task that loads a buffer, i.e. a that adds one or more quantity unis to the buffer.""" - task: Union[FixedDurationTask, ZeroDurationTask, VariableDurationTask, FixedDurationInterruptibleTask] + task: Union[ + FixedDurationTask, + ZeroDurationTask, + VariableDurationTask, + FixedDurationInterruptibleTask, + ] buffer: Union[NonConcurrentBuffer, ConcurrentBuffer] quantity: int From 720293dbc954fb54b846601260178b167fed0989 Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 21:26:25 +0100 Subject: [PATCH 7/9] Remove unused import of Task --- processscheduler/resource_constraint.py | 1 - 1 file changed, 1 deletion(-) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index dce274c1..8648f0af 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -28,7 +28,6 @@ from processscheduler.task import ( VariableDurationTask, FixedDurationInterruptibleTask, - Task, ) From 4864ccaeebe17e12eeb51b6a08f2d653cac911c7 Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Fri, 16 Feb 2024 21:29:08 +0100 Subject: [PATCH 8/9] Fix test assertion for variable task end --- test/test_resource_interrupted.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/test_resource_interrupted.py b/test/test_resource_interrupted.py index c6ab9eb6..bc284219 100644 --- a/test/test_resource_interrupted.py +++ b/test/test_resource_interrupted.py @@ -52,8 +52,8 @@ def test_resource_interrupted_variable_duration() -> None: solution = solver.solve() assert solution assert solution.tasks[task_1.name].start == 0 - assert solution.tasks[task_1.name].end == 8 - assert solution.tasks[task_2.name].start == 8 + assert solution.tasks[task_1.name].end <= 8 # does not matter when it exactly ends + assert solution.tasks[task_2.name].start == 8 # does matter assert solution.tasks[task_2.name].end == 12 From b44c718b23fb071a9411c5f2aa12412be71558f7 Mon Sep 17 00:00:00 2001 From: Jakob Zahn Date: Thu, 22 Feb 2024 09:47:36 +0100 Subject: [PATCH 9/9] Revert start and end placement conditions --- processscheduler/resource_constraint.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/processscheduler/resource_constraint.py b/processscheduler/resource_constraint.py index 8648f0af..3d6b6d22 100644 --- a/processscheduler/resource_constraint.py +++ b/processscheduler/resource_constraint.py @@ -344,12 +344,12 @@ def __init__(self, **data) -> None: conds.extend( [ z3.Xor( - start_task_i < interval_lower_bound, + start_task_i <= interval_lower_bound, start_task_i >= interval_upper_bound, ), z3.Xor( end_task_i <= interval_lower_bound, - end_task_i > interval_upper_bound, + end_task_i >= interval_upper_bound, ), ] ) @@ -504,12 +504,12 @@ def __init__(self, **data) -> None: conds.extend( [ z3.Xor( - folded_start_task_i < interval_lower_bound, + folded_start_task_i <= interval_lower_bound, folded_start_task_i >= interval_upper_bound, ), z3.Xor( folded_end_task_i <= interval_lower_bound, - folded_end_task_i > interval_upper_bound, + folded_end_task_i >= interval_upper_bound, ), ] )