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.

    Context {num_cpus: nat}.

    Record concrete_task :=
    {
      task_id: nat;
      task_cost: time;
      task_period: time;
      task_deadline: time;
      task_affinity: affinity num_cpus
    }.

    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).

    Lemma eqn_task : Equality.axiom task_eqdef.

    Canonical concrete_task_eqMixin := EqMixin eqn_task.
    Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.

  End Defs.

  Section ConcreteTaskset.

    Variable num_cpus: nat.

    Definition concrete_taskset :=
      taskset_of (@concrete_task_eqType num_cpus).

  End ConcreteTaskset.

End ConcreteTask.