Require Export prosa.implementation.facts.maximal_arrival_sequence.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.definitions.task.

(** * Job Constructor *)

(** In this file, we define a job-generation function to use in pair with a
    concrete arrival sequence. These facts sit at the basis of POET's
    assumption-less certificates, used to prove the absence of contradicting
    hypotheses in abstract RTA. *)

(** The generated jobs to belong to the concrete task type. *)
Definition Task := concrete_task : eqType.
Definition Job := concrete_job : eqType.


(** We first define a job-generation function that produces one concrete job of
    the given task, with the given job ID, arriving at the given time ... *)
Definition generate_job_at tsk t id : Job :=
  {| task.job_id := id
  ;  task.job_arrival := t
  ;  task.job_cost := task_cost tsk
  ;  task.job_deadline := t + task_deadline tsk
  ;  task.job_task := tsk |}.

(** ... and then generalize the above function to an arbitrary number of
    jobs. *)
Definition generate_jobs_at tsk n t := map (generate_job_at tsk t) (iota 0 n).