Library prosa.classic.implementation.apa.task

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.

Module ConcreteTask.

  Import Time SporadicTaskset Affinity.

  Section Defs.

    (* Let num_cpus be the number of processors. *)
    Context {num_cpus: nat}.

    (* Definition of a concrete task. *)
    Record concrete_task :=
    {
      task_id: nat; (* for uniqueness *)
      task_cost: time;
      task_period: time;
      task_deadline: time;
      task_affinity: affinity num_cpus
    }.

    (* To make it compatible with ssreflect, we define a decidable
       equality for concrete tasks. *)
    Definition task_eqdef (t1 t2: concrete_task) :=
      (task_id t1 == task_id t2) &&
      (task_cost t1 == task_cost t2) &&
      (task_period t1 == task_period t2) &&
      (task_deadline t1 == task_deadline t2) &&
      (task_affinity t1 == task_affinity t2).

    (* Next, we prove that task_eqdef is indeed an equality, ... *)
    Lemma eqn_task : Equality.axiom task_eqdef.

    (* ..., which allows instantiating the canonical structure. *)
    Canonical concrete_task_eqMixin := EqMixin eqn_task.
    Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.

  End Defs.

  Section ConcreteTaskset.

    (* Let num_cpus be the number of processors. *)
    Variable num_cpus: nat.

    Definition concrete_taskset :=
      taskset_of (@concrete_task_eqType num_cpus).

  End ConcreteTaskset.

End ConcreteTask.