Commit 7f7268b6 authored by jonathan julou's avatar jonathan julou

repreuve finie

parent aaf460d7
......@@ -119,6 +119,8 @@ Section CPA_temp_step.
that their model allows them to not have a job at t=0.*)
Hypothesis models_correct_on_init : all_task_models_correct_until_t 0.
Hypothesis H_WCRT_positive: forall tsk, task_WCRT tsk > 0.
(*========================================================================*)
(* --- IV --- MAIN LEMMAS --- VI --- *)
(*========================================================================*)
......@@ -161,10 +163,7 @@ Section CPA_temp_step.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive. intro Q. destruct (task_WCRT tsk == 0) eqn: E.
+ move/eqP in E. rewrite E. destruct (job_arrival j == 0) eqn: F.
* move/eqP in F. assert (job_cost j = 0).
{
} assert (job_cost j > 0). apply H_positive_cost.
* assert (P: task_WCRT tsk > 0) by (apply H_WCRT_positive).
exfalso. ssromega.
* ssromega.
+ ssromega.
......
......@@ -751,6 +751,8 @@ Section Propagatability.
/\
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
Hypothesis WCRT_positive: forall tsk, task_WCRT tsk > 0.
(*========================================================================*)
(* --- >_< --- HYPOTHESIS --- >_< --- *)
(*========================================================================*)
......@@ -775,13 +777,10 @@ Section Propagatability.
rewrite -> dependent_period with (t1 :=tsk1).
rewrite -> dependent_jitter with (t1 :=tsk1).
apply periodic_jitter_same_law_up_to_t with sched H0 H4 H5 H6.
exact W. exact B. exact correct_dependancy. exact valid_arr_seq.
exact correct_schedule. apply correct_period. exact ints1.
apply periodic_jitter_same_law_up_to_t with sched H0 H4 H5 H6; auto.
intros j pj offset P1 P2 P3 P4 P5 P6.
rewrite <- P4. apply hyp_arrival_suiv_expr with offset t. exact P1. exact P2. exact P5. exact P6.
exact positive_cost. exact jobs_must_arrive. exact dependency.
exact model_verified_by_tsk1. exact dependency. exact dependency.
rewrite <- P4. apply hyp_arrival_suiv_expr with offset t; auto.
exact dependency. exact dependency.
Qed.
(*assuming the hypothesis, all WCRTs are respected.*)
......@@ -807,6 +806,7 @@ Section Propagatability.
unfold all_task_models_correct_until_t in Q. apply Q. exact ints.
- unfold all_task_models_correct_until_t. intros tsk' J.
apply models_correct_on_init.
- exact WCRT_positive.
- exact P.
Qed.
......
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