Commit c6a57412 authored by jonathan julou's avatar jonathan julou

changes merged

parents 7f7268b6 eb00229b
Pipeline #19152 passed with stages
in 6 minutes and 15 seconds
From rt.restructuring Require Export behavior.schedule model.task model.arrival.periodic_jitter analysis.schedulability.
Section ArrivalsDefs.
Context {Jobs : JobType} {Tasks : TaskType}.
Context `{JobArrival Jobs}.
Variable arr_seq : arrival_sequence Jobs.
Definition valid_arrival_sequence_up_to_t (t : instant) := True.
Lemma valid_arrival_sequence_eq : valid_arrival_sequence arr_seq <-> forall t, valid_arrival_sequence_up_to_t t.
Admitted.
End ArrivalsDefs.
Section ScheduleDefs.
Context {Jobs : JobType} {Tasks : TaskType}.
Context `{JobArrival Jobs} `{JobCost Jobs}.
Context (State : Type) `{ProcessorState Jobs State}.
Variable arr_seq : arrival_sequence Jobs.
Variable sched : schedule State.
Definition valid_schedule_up_to_t (t : instant) := True.
Lemma valid_schedule_eq : valid_schedule sched arr_seq <-> forall t, valid_schedule_up_to_t t.
Admitted.
Variable ts : seq Tasks.
(* TODO : all_jobs_from_taskset in model.task? + up_to_t + equiv *)
Definition all_jobs_from_taskset := valid_arrival_sequence arr_seq /\ ts = nil.
Definition all_jobs_from_taskset_up_to_t (t : instant) := True.
(* TODO : respects_preemptive_priorities_up_to_t + equiv *)
(* TODO : work_conserving_up_to_t + equiv *)
End ScheduleDefs.
Section Transformation.
Context {Jobs : JobType} {Tasks : TaskType}.
Context `{JobArrival Jobs} `{JobCost Jobs} `{JobTask Jobs Tasks}.
Context (State : Type) `{ProcessorState Jobs State}.
Variable ts : seq Tasks.
Variable tsk : Tasks.
Variable R : duration.
Hypothesis Hanalysis_correct :
forall arr_seq : arrival_sequence Jobs,
valid_arrival_sequence arr_seq ->
all_jobs_from_taskset arr_seq ts ->
forall sched : schedule State,
valid_schedule sched arr_seq (* etc *) ->
task_response_time_upper_bound arr_seq sched tsk R.
End Transformation.
\ No newline at end of file
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