Library prosa.analysis.definitions.schedule_prefix

Require Export prosa.behavior.ready.
Require Export prosa.util.nat.

We define the notion of prefix-equivalence of schedules.

Section PrefixDefinition.

For any type of jobs...
  Context {Job : JobType}.

... and any kind of processor model, ...
  Context {PState: Type} `{ProcessorState Job PState}.

... two schedules share an identical prefix if they are pointwise identical (at least) up to a fixed horizon.
  Definition identical_prefix (sched sched' : schedule PState) (horizon : instant) :=
     t,
      t < horizon
      sched t = sched' t.

In other words, two schedules with a shared prefix are completely interchangeable w.r.t. whether a job is scheduled (in the prefix).
  Fact identical_prefix_scheduled_at:
     sched sched' h,
      identical_prefix sched sched' h
       j t,
        t < h
        scheduled_at sched j t = scheduled_at sched' j t.

Trivially, any prefix of an identical prefix is also an identical prefix.
  Fact identical_prefix_inclusion:
     sched sched' h,
      identical_prefix sched sched' h
       h',
        h' h
        identical_prefix sched sched' h'.

End PrefixDefinition.