Library prosa.analysis.definitions.carry_in

Require Export prosa.model.priority.classes.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Throughout this file, we assume ideal uniprocessor schedules.
Require Import prosa.model.processor.ideal.

No Carry-In

In this module we define the notion of no carry-in time for uni-processor schedulers.
Section NoCarryIn.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence with consistent arrivals.
Next, consider any ideal uni-processor schedule of this arrival sequence.
The processor has no carry-in at time t iff every job (regardless of priority) from the arrival sequence released before t has completed by that time.
  Definition no_carry_in (t : instant) :=
      arrives_in arr_seq j_o
      arrived_before j_o t
      completed_by sched j_o t.

End NoCarryIn.