Commit e236efb1 authored by Björn Brandenburg's avatar Björn Brandenburg

add notion of a shared identical schedule prefix

parent a77c7c71
Require Export prosa.behavior.ready.
(** 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) :=
forall t,
t < horizon ->
sched t = sched' t.
End PrefixDefinition.
......@@ -49,3 +49,4 @@ bursty
TODO
mathcomp
hyperperiod
pointwise
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment