Commit 03ce6180 authored by jonathan julou's avatar jonathan julou

essai en faisant alle plus loin BCRT et WCRT. devrait etre faux

parent b222b4d0
Pipeline #18998 failed with stages
in 33 seconds
......@@ -33,7 +33,7 @@ Section Tasks.
arrives_in arr_seq j ->
job_task j = tsk ->
(
completed_by sched j t ->
completed_by sched j (t+R) ->
~ job_response_time_bound sched j R
).
......@@ -44,13 +44,13 @@ Section Tasks.
arrives_in arr_seq j ->
job_task j = tsk ->
(
completed_by sched j t->
completed_by sched j (t+R)->
job_response_time_bound sched j R
)
/\
(
pending sched j t ->
job_arrival j >= t-R
pending sched j (t+R) ->
job_arrival j > t
).
End Tasks.
......@@ -89,7 +89,7 @@ Section Proofs.
unfold task_response_time_lower_bound_until_t in P.
destruct (completed_by sched j (job_arrival j + BCRT)) eqn:Q.
+ rewrite <- Q.
apply P with (t := job_arrival j + BCRT). exact in_arr_seq.
apply P with (t := job_arrival j). exact in_arr_seq.
exact in_task. exact Q.
+ trivial.
......@@ -114,12 +114,12 @@ Section Proofs.
destruct (completed_by sched j (job_arrival j + WCRT)) eqn:Q.
+ trivial.
+ destruct (completed_by sched j (job_arrival j + WCRT).+1) eqn:E.
* apply P with (t:= (job_arrival j + WCRT).+1). exact in_arr_seq.
* apply P with (t:= (job_arrival j).+1). exact in_arr_seq.
exact in_task. exact E.
* assert (R: (job_arrival j + WCRT).+1 - WCRT <= job_arrival j).
apply P with (t := (job_arrival j + WCRT).+1).
* assert (R: (job_arrival j).+1 < job_arrival j).
apply P with (t := (job_arrival j).+1).
exact in_arr_seq. exact in_task. unfold pending.
unfold has_arrived. destruct (job_arrival j <= (job_arrival j + WCRT).+1) eqn: J.
unfold has_arrived. destruct (job_arrival j <= (job_arrival j).+1 + WCRT) eqn: J.
-- simpl. apply/eqP. move/eqP in E. exact E.
-- exfalso; ssromega.
-- exfalso; ssromega.
......@@ -134,14 +134,14 @@ Section Proofs.
destruct PS as [arrjt cpltjt].
unfold has_arrived in arrjt. unfold completed_by in cpltjt.
unfold completed_by in Q.
assert (cpltjt_rewritten: job_cost j > service sched j t). ssromega.
assert (R: service sched j t < service sched j (job_arrival j + WCRT)).
assert (cpltjt_rewritten: job_cost j > service sched j (t+WCRT)). ssromega.
assert (R: service sched j (t+WCRT) < service sched j (job_arrival j + WCRT)).
{ apply leq_trans with (job_cost j). exact cpltjt_rewritten.
apply Q. exact in_arr_seq. exact in_task. }
unfold service in R. unfold service_during in R.
assert (W: t <= job_arrival j + WCRT).
apply jonathan.sum_to_args_leq with (F := service_at sched j).
exact R. ssromega.
assert (W: t < job_arrival j).
apply jonathan.sum_to_args_lt with (F := service_at sched j) in R.
ssromega. exact W.
Qed.
End Proofs.
\ 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