Commit fb7f6470 authored by jonathan julou's avatar jonathan julou

AH

parent 1abfae4c
Pipeline #18871 passed with stages
in 3 minutes and 37 seconds
......@@ -857,7 +857,7 @@ Local Ltac init_pipeline_lemma offset:=
theoretical_arrival j =
offset + BCRT + n * task_period tsk1.
Proof.
Pro of.
intros offset n.
init_pipeline_lemma offset. intro hyp.
......@@ -987,7 +987,6 @@ Local Ltac init_pipeline_lemma offset:=
Proof.
intros dependency Q.
unfold respects_periodic_jitter_task_model in Q.
destruct Q as [offset Q].
assert (RPJTM: is_indeed_the_offset tsk1 offset t) by (exact Q).
......@@ -997,18 +996,14 @@ Local Ltac init_pipeline_lemma offset:=
*)
destruct Q as [correction injection].
destruct correct_dependancy as [right_complete left_complete].
unfold respects_periodic_jitter_task_model.
exists (offset + BCRT).
split. (* 2: split.*)
- (* FIRST PART: CORRECTION *)
intros j arr_bound in_arr_seq_two in_task_two.
apply (correction_lemma_UTT offset j dependency RPJTM
in_task_two in_arr_seq_two arr_bound).
- (* SECOND PART: INJECTIVITY *)
intros ja jb.
intros arr_bound_ja arr_bound_jb.
......
echo ""
echo "CPA_MAIN"
./.proofloc.py --check frame_by_frame/cpa_temporal_step_formula.v
./.proofloc.py --check frame_by_frame/periodic_jitter_propagation_up_to_t.v
echo ""
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