Commit f1d6d35d authored by Vedant Chavda's avatar Vedant Chavda

progress

parent be861aca
Pipeline #32020 failed with stages
in 10 minutes and 4 seconds
......@@ -141,6 +141,44 @@ Section todo_name.
now auto.
Qed.
Lemma equal_arrivals_implies_equal_jobs :
forall tsk j1 j2,
valid_offset arr_seq tsk ->
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
job_task j1 = tsk ->
job_task j2 = tsk ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 = job_arrival j2 ->
j1 = j2.
Proof.
intros * OFF PERIOD PERIODIC TSK1 TSK2 ARR1 ARR2 EQ_ARR.
case (boolP (j1 == j2)) => [/eqP EQ | NEQ]; first by auto.
specialize (leq_total (job_arrival j1) (job_arrival j2)) => /orP [J1_LTE | J2_LTE].
specialize (job_sep_periodic arr_seq H_consistent_arrivals H_uniq_arr_seq tsk PERIODIC PERIOD j1 j2) => ARR_SEP.
feed_n 6 ARR_SEP => //.
now apply /eqP.
move : ARR_SEP => [n [POS_N ARR_R]].
rewrite EQ_ARR TSK1 in ARR_R.
exfalso.
have POS : (n * task_period tsk > 0).
rewrite muln_gt0; apply /andP.
split => //.
now ssromega.
specialize (job_sep_periodic arr_seq H_consistent_arrivals H_uniq_arr_seq tsk PERIODIC PERIOD j2 j1) => ARR_SEP.
feed_n 6 ARR_SEP => //.
apply neq_sym in NEQ.
now apply /eqP.
move : ARR_SEP => [n [POS_N ARR_R]].
rewrite EQ_ARR TSK2 in ARR_R.
exfalso.
have POS : (n * task_period tsk > 0).
rewrite muln_gt0; apply /andP.
split => //.
now ssromega.
Qed.
Lemma jobs_exists_later :
forall n tsk,
valid_offset arr_seq tsk ->
......@@ -149,23 +187,35 @@ Section todo_name.
exists j',
arrives_in arr_seq j' /\
job_task j' = tsk /\
job_arrival j' = task_offset tsk + n * task_period tsk.
job_arrival j' = task_offset tsk + n * task_period tsk /\
job_index arr_seq j' = n.
Proof.
intros * VALID_OFF PERIOD PERIODIC.
induction n.
rewrite mul0n addn0.
rewrite /valid_offset /job_released_at_offset in VALID_OFF.
move : VALID_OFF => [A [j' [ARR_IN [TSK ARR]]]].
now exists j'.
move : IHn => [j' [ARR [TSK ARR_TIME]]].
have EXISTS_J : exists j'', arrives_in arr_seq j'' /\ job_task j'' = tsk /\ job_index arr_seq j'' = job_index arr_seq j' + 1 by apply H_infinite_jobs.
move : EXISTS_J => [j'' [TSK' [ARR' IND]]].
exists j''.
repeat split; try by auto.
apply consecutive_job_separation with (tsk0 := tsk) in IND => //.
rewrite mulSn IND TSK.
now ssromega.
Qed.
{ rewrite mul0n addn0.
move : (VALID_OFF) => [A [j' [ARR_IN [TSK ARR]]]].
exists j'; repeat split => //.
specialize (exists_jobs_before_j arr_seq H_consistent_arrivals H_uniq_arr_seq j' ARR_IN 0) => BEFORE_JB.
have Z_OR_SUCCN : job_index arr_seq j' = 0 \/ job_index arr_seq j' > 0 by admit.
move : Z_OR_SUCCN => [Z | POS]; first by auto.
feed_n 1 BEFORE_JB => //.
move : BEFORE_JB => [bj [NEQ_BJ [TSKBJ [ARRBJ INDBJ]]]].
apply first_job_arrival with (tsk0 := tsk) in INDBJ => //.
- rewrite -INDBJ in ARR.
now apply equal_arrivals_implies_equal_jobs with (tsk := tsk) in ARR => //; try by rewrite TSKBJ.
- now rewrite TSKBJ.
}
{ move : IHn => [j' [ARR [TSK [ARR_TIME IND]]]].
have EXISTS_J : exists j'', arrives_in arr_seq j'' /\ job_task j'' = tsk /\ job_index arr_seq j'' = job_index arr_seq j' + 1 by apply H_infinite_jobs.
move : EXISTS_J => [j'' [TSK' [ARR' IND'']]].
exists j''.
repeat split; try by auto.
apply consecutive_job_separation with (tsk0 := tsk) in IND'' => //.
rewrite mulSn IND'' TSK.
now ssromega.
now rewrite IND'' IND; ssromega.
Grab Existential Variables.
Admitted.
Lemma task_arrivals_at_size :
forall tsk n,
......@@ -177,8 +227,8 @@ Section todo_name.
intros * OFFSET PERIOD PERIODIC.
have EXISTS_J : exists j', arrives_in arr_seq j' /\
job_task j' = tsk /\
job_arrival j' = task_offset tsk + n * task_period tsk by apply jobs_exists_later => //.
move : EXISTS_J => [j' [ARR [TSK ARRIVAL]]].
job_arrival j' = task_offset tsk + n * task_period tsk /\ job_index arr_seq j' = n by apply jobs_exists_later => //.
move : EXISTS_J => [j' [ARR [TSK [ARRIVAL IND]]]].
apply only_j_in_task_arrivals_at_j with (tsk0 := tsk) in ARR => //; try by apply periodic_task_respects_sporadic_task_model.
rewrite /task_arrivals_at_job_arrival TSK in ARR.
rewrite -ARRIVAL.
......@@ -208,7 +258,7 @@ Section todo_name.
valid_offset arr_seq tsk ->
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
task_arrivals_at arr_seq tsk t = [::].
task_arrivals_at arr_seq tsk t = [::].
Proof.
intros * T OFFSET PERIOD H_PERIODIC.
have EMPT_OR_EXISTS : forall xs, xs = [::] \/ exists a, a \in xs.
......@@ -251,16 +301,24 @@ Section todo_name.
now apply arrivals_uniq.
Qed.
Lemma todo_name4 :
forall tsk j' n,
Lemma job_arr_index :
forall tsk n j',
valid_offset arr_seq tsk ->
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
arrives_in arr_seq j' ->
job_task j' = tsk ->
job_arrival j' = task_offset tsk + n * task_period tsk ->
job_index arr_seq j' = n.
Proof.
Admitted.
intros * OFF PERIOD PERIODIC ARR_J TSK ARR.
specialize (jobs_exists_later n tsk) => LATER_JB.
feed_n 3 LATER_JB => //.
move : LATER_JB => [j'' [ARR' [TSK' [ARRIVAL IND]]]].
rewrite -ARR in ARRIVAL.
apply equal_arrivals_implies_equal_jobs with (tsk := tsk) in ARRIVAL => //.
now rewrite -ARRIVAL.
Qed.
Lemma todo_name5 :
forall tsk n j' t,
......@@ -298,9 +356,9 @@ Section todo_name.
split => //.
specialize (jobs_exists_later n tsk) => LATER_JB.
feed_n 3 LATER_JB => //.
move : LATER_JB => [j' [ARR' [TSK' J'ARR]]].
move : LATER_JB => [j' [ARR' [TSK' [J'ARR IND']]]].
move : (J'ARR) => IND.
apply todo_name4 in IND => //.
apply job_arr_index in IND => //.
set nj := nth j (task_arrivals_up_to arr_seq tsk t) n.
have IND_JB : job_index arr_seq nj = n.
rewrite /job_index /nj.
......
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