Require Import prosa.model.task.arrival.periodic.
[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 Import prosa.model.task.arrival.periodic_as_sporadic.
Require Import prosa.model.task.arrival.sporadic_as_curve.
Require Import prosa.model.task.arrival.curve_as_rbf.

(** * Arrival Model Conversion

  This file demonstrates the automatic conversion of arrival
  models. In particular, we show how a set of periodic tasks can be
  interpreted also as (1) sporadic tasks with minimum inter-arrival
  times, (2) sporadic tasks with arrival curves, and (3) request-bound
  functions.  *)

Section AutoArrivalModelConversion.

  (** Consider periodic tasks ... *)
  Context {Task : TaskType} `{PeriodicModel Task}.

  (** ... and their corresponding jobs. *)
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.

  (** Given a set of such periodic tasks  ... *)
  Variable ts : TaskSet Task.

  (** ... and a valid arrival sequence, ...*)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** ... if the tasks are valid periodic tasks, ...*)
  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.
  Hypothesis H_valid_periods : valid_periods ts.

  (** ... then we can automatically interpret them also as satisfying
      other arrival models, as we demonstrate in the following. *)

  (** ** Periodic Tasks as Sporadic Tasks *)

  (** The tasks satisfy the sporadic validity constraint... *)
  Goal valid_taskset_inter_arrival_times ts.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
valid_taskset_inter_arrival_times ts
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
valid_taskset_inter_arrival_times ts by []. Qed.

  (** ... and arrival sequence is legal under the sporadic task
      model. *)
  Goal taskset_respects_sporadic_task_model ts arr_seq.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
taskset_respects_sporadic_task_model ts arr_seq
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
taskset_respects_sporadic_task_model ts arr_seq by []. Qed.

  (** ** Periodic Tasks as Arrival Curves *)

  (** The tasks satisfy the arrival-curve validity constraint... *)
  Goal valid_taskset_arrival_curve ts max_arrivals.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
valid_taskset_arrival_curve ts max_arrivals
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
valid_taskset_arrival_curve ts max_arrivals by []. Qed.

  (** ... and the arrival sequence is legal under the arrival-curve
      model. *)
  Goal taskset_respects_max_arrivals arr_seq ts.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
taskset_respects_max_arrivals arr_seq ts
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
taskset_respects_max_arrivals arr_seq ts by []. Qed.

  (** ** Periodic Tasks as RBFs *)

  (** Assuming that each task has a WCET... *)
  Context `{TaskCost Task}.

  (** ... and that jobs are compliant with the WCET, ... *)
  Context `{JobCost Job}.
  Hypothesis H_valid_costs : jobs_have_valid_job_costs.

  (** ... the tasks satisfy the RBF validity constraint... *)
  Goal valid_taskset_request_bound_function ts (task_max_rbf max_arrivals).
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
H2: TaskCost Task
H3: JobCost Job
H_valid_costs: jobs_have_valid_job_costs
valid_taskset_request_bound_function ts
  (task_max_rbf max_arrivals)
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
H2: TaskCost Task
H3: JobCost Job
H_valid_costs: jobs_have_valid_job_costs
valid_taskset_request_bound_function ts
  (task_max_rbf max_arrivals) by []. Qed.

  (** ... and the arrival sequence is legal under the RBF model. *)
  Goal taskset_respects_max_request_bound arr_seq ts.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
H2: TaskCost Task
H3: JobCost Job
H_valid_costs: jobs_have_valid_job_costs
taskset_respects_max_request_bound arr_seq ts
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
ts: TaskSet Task
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_respects: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods: valid_periods ts
H2: TaskCost Task
H3: JobCost Job
H_valid_costs: jobs_have_valid_job_costs
taskset_respects_max_request_bound arr_seq ts by []. Qed.

  (** Thanks to type-class resolution, all conversions from more
      restrictive to less restrictive task model happen transparently
      and the and necessary proofs are found automatically.

      Of course, it is possible to start from sporadic tasks or tasks
      with arrival curves, too. *)

End AutoArrivalModelConversion.