Commit 2438d8d4 authored by Marco Maida's avatar Marco Maida 🌱
Browse files

Better comment

parent 0f810f31
Pipeline #63829 failed with stages
in 53 seconds
......@@ -123,7 +123,8 @@ Section NPUniprocessorScheduler.
(** Finally, we assume the readiness model to be non-clairvoyant. *)
Hypothesis H_nonclairvoyant_readiness: nonclairvoyant_readiness RM.
(** For brevity, we define the notion of the prefix of the schedule. *)
(** For notational convenience, recall the definition of a prefix of the
schedule based on which the next decision is made. *)
Let sched_prefix t :=
if t is t'.+1 then schedule_up_to policy None t' else empty_schedule None.
Supports Markdown
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