Commit 1875675d authored by jonathan julou's avatar jonathan julou

rololo

parent 52fcd804
Pipeline #19246 failed with stages
in 51 seconds
......@@ -105,11 +105,6 @@ Section PathResponseTime.
forall j j', arrives_in arr_seq j -> next_job j = some j'
-> arrives_in arr_seq j'.
Hypothesis respects_task_dependency : forall tsk1 tsk2 : Task,
task_dependency tsk1 tsk2 ->
forall t,
size (completed_jobs_before Task Job arr_seq sched tsk1 t) = size (task_jobs_arrived_up_to Task Job arr_seq tsk2 t).
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
Hypothesis correct_schedule: respects_job_dependency sched.
......
......@@ -102,7 +102,7 @@ Section Periojitt_same_law.
unfold respects_job_dependency in correct_schedule.
apply correct_schedule in dependency.
unfold completes_at in dependency.
unfold dependency.completes_at in dependency.
assert (UwU: job_cost pred_j <= service sched pred_j (job_arrival j)) by ssromega.
unfold task_response_time_lower_bound in BCRT_correct.
......@@ -142,7 +142,7 @@ Section Periojitt_same_law.
unfold respects_job_dependency in correct_schedule.
apply correct_schedule in dependency.
unfold completes_at in dependency.
unfold dependency.completes_at in dependency.
assert (UwU: service sched pred_j (job_arrival j).-1 < job_cost pred_j) by ssromega.
unfold task_response_time_upper_bound in WCRT_correct.
......
......@@ -105,11 +105,6 @@ Section Prefixverif.
forall j j', arrives_in arr_seq j -> next_job j = some j'
-> arrives_in arr_seq j'.
Hypothesis respects_task_dependency : forall tsk1 tsk2 : Task,
task_dependency tsk1 tsk2 ->
forall t,
size (completed_jobs_before Task Job arr_seq sched tsk1 t) = size (task_jobs_arrived_up_to Task Job arr_seq tsk2 t).
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
Hypothesis correct_schedule: respects_job_dependency sched.
......
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