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: ProcessorState Job}.

... 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.
  Proof.
    movesched sched' h IDENT j t LT_h.
    now rewrite /scheduled_at (IDENT t LT_h).
  Qed.

Trivially, any prefix of an identical prefix is also an identical prefix.
  Fact identical_prefix_inclusion :
     sched sched' h h',
      h' h
      identical_prefix sched sched' h identical_prefix sched sched' h'.
  Proof. by movesched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.

End PrefixDefinition.