Library prosa.classic.implementation.uni.susp.dynamic.task

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

Module ConcreteTask.

  Import SporadicTaskset.

  Section Defs.

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

    (* 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_suspension_bound t1 == task_suspension_bound 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.

    Definition concrete_taskset :=
      taskset_of concrete_task_eqType.

  End ConcreteTaskset.

End ConcreteTask.