Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Task Max Inter-Arrival *) (** We define a task-model parameter [task_max_inter_arrival_time] as the maximum time difference between the arrivals of consecutive jobs. *) Class TaskMaxInterArrival (Task : TaskType) := task_max_inter_arrival_time : Task -> duration. (** In the following section, we define two properties that a task must satisfy for its maximum inter-arrival time to be valid. *) Section ValidTaskMaxInterArrival. (** Consider any type of tasks, ... *) Context {Task : TaskType}. Context `{TaskMaxInterArrival Task}. (** ... any type of jobs associated with the tasks, ... *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** ... and any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** Firstly, the task maximum inter-arrival time for a task is positive. *) Definition positive_task_max_inter_arrival_time (tsk : Task) := task_max_inter_arrival_time tsk > 0. (** Secondly, for any job [j] (with a positive [job_index]) of a task [tsk], there exists a job [j'] of task [tsk] that arrives before [j] with [j] not arriving any later than the task maximum inter-arrival time of [tsk] after [j']. *) Definition arr_sep_task_max_inter_arrival (tsk : Task) := forall (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j > 0 -> exists (j' : Job), j <> j' /\ arrives_in arr_seq j' /\ job_task j' = tsk /\ job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk. (** 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. (** A task set is said to respect the task max inter-arrival model iff all tasks in the task set have valid task max inter-arrival times as defined above. *) Definition taskset_respects_task_max_inter_arrival_model (ts : TaskSet Task) := forall tsk, tsk \in ts -> valid_task_max_inter_arrival_time tsk. End ValidTaskMaxInterArrival.