Library prosa.classic.implementation.apa.job

Require Import prosa.classic.model.time prosa.classic.util.all.
Require Import prosa.classic.implementation.apa.task.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.

Module ConcreteJob.

  Import Time.
  Import ConcreteTask.

  Section Defs.

    Context {num_cpus: nat}.

    Record concrete_job :=
    {
      job_id: nat;
      job_arrival: nat;
      job_cost: time;
      job_deadline: time;
      job_task: @concrete_task num_cpus
    }.

    Definition job_eqdef (j1 j2: concrete_job) :=
      (job_id j1 == job_id j2) &&
      (job_arrival j1 == job_arrival j2) &&
      (job_cost j1 == job_cost j2) &&
      (job_deadline j1 == job_deadline j2) &&
      (job_task j1 == job_task j2).

    Lemma eqn_job : Equality.axiom job_eqdef.

    Canonical concrete_job_eqMixin := EqMixin eqn_job.
    Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.

   End Defs.

End ConcreteJob.