Library prosa.classic.model.schedule.uni.schedule_of_task

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ScheduleOfTask.

  Export SporadicTaskset UniprocessorSchedule.

  Section ScheduleProperties.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_cost: Job → time.
    Variable job_task: Job → Task.

    Variable sched: schedule Job.

    Section TaskProperties.

      Variable tsk: Task.

      Definition task_scheduled_at (t: time) :=
        if sched t is Some j then
          job_task j == tsk
        else false.

      Definition task_service_at (t: time) : time := task_scheduled_at t.

      Definition task_service_during (t1 t2: time) :=
        \sum_(t1 ≤ t < t2) task_service_at t.

      Definition task_service (t2: time) := task_service_during 0 t2.

    End TaskProperties.

  End ScheduleProperties.

End ScheduleOfTask.