Finish FP RTA with jitter

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile apa.v BertognaResponseTimeDefs.v BertognaResponseTimeFP.v divround.v eqtask_dec.v eqtaskjitter_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v 
+# coq_makefile apa.v BertognaResponseTimeDefsJitter.v BertognaResponseTimeDefs.v BertognaResponseTimeFPJitter.v BertognaResponseTimeFP.v divround.v eqtask_dec.v eqtaskjitter_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v 
 #
 
 .DEFAULT_GOAL := all
@@ -80,7 +80,9 @@ endif
 #                    #
 ######################
 
-VFILES:=BertognaResponseTimeDefs.v\
+VFILES:=BertognaResponseTimeDefsJitter.v\
+  BertognaResponseTimeDefs.v\
+  BertognaResponseTimeFPJitter.v\
   BertognaResponseTimeFP.v\
   divround.v\
   extralib.v\

ScheduleDefs.v

@@ -376,15 +376,13 @@ Module ScheduleOfTaskWithJitter.
   Section ArrivalAfterJitter.
 
     Context {sporadic_task: eqType}.
-    Context {Job: eqType}.
-    Context {arr_seq: arrival_sequence Job}.
-    
+    Context {Job: eqType}.    
     Variable job_cost: Job -> nat.
     Variable job_task: Job -> sporadic_task.
     Variable job_jitter: Job -> nat.
-    
-    Variable num_cpus: nat.
-    Variable rate: Job -> processor num_cpus -> time.
+
+    Context {arr_seq: arrival_sequence Job}.
+    Context {num_cpus: nat}.
     Variable sched: schedule num_cpus arr_seq.
 
     (* Whether a job can only be scheduled if it has arrived *)

WorkloadDefsJitter.v

@@ -146,7 +146,7 @@ Module WorkloadWithJitter.
     (* Assumption: jobs only execute if they arrived.
        This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
     Hypothesis H_jobs_must_arrive_after_jitter:
-      jobs_execute_after_jitter job_jitter num_cpus sched.
+      jobs_execute_after_jitter job_jitter sched.
 
     (* Assumption: jobs do not execute after they completed.
        This is used to eliminate jobs that complete before the start of the interval t1. *)