Modifications to ideal uniprocessor schedule

• We modified prev_job_nonpreemptive, as currently does respect jobs_must_be_ready_to_execute
• We do not prove schedule_respects_preemption_model anymore.
• We slightly changed valid_nonpreemptive_readiness so that sched is a parameter. This way, the proposition can be assumed to hold only for a certain schedule (making weaker assumptions).
• We proved more facts for the preemption-aware scheduler

analysis/definitions/readiness.v

@@ -41,8 +41,8 @@ Section ReadinessModelProperties.
       ready. Consequently, in a valid preemption-policy-compliant schedule, a
       nonpreemptive job must remain ready until at least the end of its
       nonpreemptive section. *)
-  Definition valid_nonpreemptive_readiness :=
-     forall sched j t,
+  Definition valid_nonpreemptive_readiness sched :=
+     forall j t,
         ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
   
 End ReadinessModelProperties.