Library prosa.classic.model.arrival.basic.task

Require Import prosa.classic.model.time prosa.classic.util.all.
From mathcomp Require Import ssrnat ssrbool eqtype fintype seq.

Module SporadicTask.

  Import Time.

  Section BasicTask.
    Context {Task: eqType}.
    Variable task_cost: Task → time.
    Variable task_period: Task → time.
    Variable task_deadline: Task → time.

    Section ValidParameters.
      Variable tsk: Task.

      Definition task_cost_positive := task_cost tsk > 0.
      Definition task_period_positive := task_period tsk > 0.
      Definition task_deadline_positive := task_deadline tsk > 0.

      Definition task_cost_le_deadline := task_cost tsk ≤ task_deadline tsk.
      Definition task_cost_le_period := task_cost tsk ≤ task_period tsk.

      Definition is_valid_sporadic_task :=
        task_cost_positive ∧ task_period_positive ∧ task_deadline_positive ∧
        task_cost_le_deadline ∧ task_cost_le_period.

    End ValidParameters.

  End BasicTask.

End SporadicTask.

Module SporadicTaskset.
  Import Time.
  Export SporadicTask.

  Section TasksetDefs.

    Definition taskset_of (Task: eqType) := {set Task}.

    Section TasksetProperties.

      Context {Task: eqType}.
      Variable task_cost: Task → time.
      Variable task_period: Task → time.
      Variable task_deadline: Task → time.

      Let is_valid_task :=
        is_valid_sporadic_task task_cost task_period task_deadline.

      Variable ts: seq Task.

      Definition valid_sporadic_taskset :=
        ∀ tsk,
          tsk \in ts → is_valid_task tsk.

      Definition implicit_deadline_model :=
        ∀ tsk,
          tsk \in ts → task_deadline tsk = task_period tsk.

      Definition constrained_deadline_model :=
        ∀ tsk,
          tsk \in ts → task_deadline tsk ≤ task_period tsk.

      Definition arbitrary_deadline_model := True.

    End TasksetProperties.

  End TasksetDefs.

End SporadicTaskset.