Commit fa0c33b2 authored by Vedant Chavda's avatar Vedant Chavda

small improvements

parent 6f2cb4d7
Pipeline #32121 passed with stages
in 11 minutes and 24 seconds
......@@ -103,8 +103,9 @@ Section TaskArrivals.
now rewrite -filter_cat -arrivals_between_cat.
Qed.
(** We observe that for any job [j], task arrivals up to [job_arrival j] can be split
into task arrivals before [job_arrival j] and task arrivals at [job_arrival j]. *)
(** We observe that for any job [j], task arrivals up to [job_arrival j] is a
concatenation of task arrivals before [job_arrival j] and task arrivals
at [job_arrival j]. *)
Lemma task_arrivals_up_to_cat:
forall j,
arrives_in arr_seq j ->
......
......@@ -208,8 +208,9 @@ Section SporadicArrivals.
now ssromega.
Qed.
(** We show that task arrivals at [job_arrival j1] can be written as
task arrivals between [job_arrival j1] and [job_arrival j1 + 1]. *)
(** We show that task arrivals at [job_arrival j1] is the
same as task arrivals that arrive between [job_arrival j1]
and [job_arrival j1 + 1]. *)
Lemma task_arrivals_at_as_task_arrivals_between :
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
Proof.
......
......@@ -43,8 +43,8 @@ Section ValidTaskMaxInterArrival.
job_task j' = tsk /\
job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk.
(** Finally, we say that the [task_max_inter_arrival_time] of a task [tsk] is valid iff
it satisfies the above two properties. *)
(** Finally, we say that the maximum inter-arrival time of a task [tsk] is
valid iff it satisfies the above two properties. *)
Definition valid_task_max_inter_arrival_time (tsk: Task) :=
positive_task_max_inter_arrival_time tsk /\
arr_sep_task_max_inter_arrival tsk.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment