Commit a0354880 authored by Xiaojie Guo's avatar Xiaojie Guo Committed by Felipe Cerqueira

Removed tactics_gr.v to clear Axiom

parent 82267806
Require Import rt.util.all rt.util.tactics_gr
Require Import Arith.
Require Import rt.util.all
rt.model.arrival.basic.job
rt.model.arrival.basic.task_arrival
rt.model.schedule.uni.schedulability
......
Require Import Arith Omega Nat.
Require Import rt.util.all rt.util.tactics_gr.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job
rt.model.arrival.basic.task_arrival
rt.model.schedule.uni.schedulability
......@@ -385,7 +385,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite /to_next_slot /from_start_of_slot. repeat (rewrite -addnBA //).
rewrite case2 Hcases. repeat rewrite addSn case1 -subn1 subKn //.
repeat rewrite subn0.
cases (c < time_slot) as Hc_slot; rewrite /duration_to_finish_from_start_of_slot_with.
case Hc_slot:(c < time_slot); rewrite /duration_to_finish_from_start_of_slot_with.
* by rewrite ceil_eq1.
* rewrite ceil_suba //; try ssromega.
rewrite subn1 mulnBl mul1n addnA -addSn addn1.
......@@ -677,7 +677,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
intro c.
induction c as [| c IHc];intros ARR PEN SC.
- rewrite /formula_rt /= addn0; apply (C0_ sched j).
- cases (is_scheduled_at ARR) as l.
- case l:(is_scheduled_at ARR).
+ destruct c as [|c];apply (S_C_sched sched j);rewrite // formula_sched_St //.
* rewrite /formula_rt /= addn0;apply C0_.
* apply IHc.
......@@ -738,8 +738,8 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
unfold Task_in_time_slot in in_time_slot_at.
fold tdma_cycle in in_time_slot_at. fold time_slot in in_time_slot_at. fold slot_offset in in_time_slot_at.
have cost_pos: job_cost j > 0 by apply H_valid_job.
cases (in_time_slot_at (job_arrival j)) as test_in_slot.
- cases (job_cost j <= time_slot - from_start_of_slot (job_arrival j)) as test_cost.
case test_in_slot:(in_time_slot_at (job_arrival j)).
- case test_cost:(job_cost j <= time_slot - from_start_of_slot (job_arrival j)).
+ set other := div_ceil (job_cost j) time_slot * (tdma_cycle - time_slot).
apply leq_trans with (n:=div_ceil WCET time_slot * (tdma_cycle - time_slot) + job_cost j).
* rewrite gtn_eqF //. apply leq_addl.
......@@ -803,14 +803,12 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
fold slot_offset in in_time_slot_at. fold from_start_of_slot in in_time_slot_at.
assert (gt_ref: reflect (time_slot> from_start_of_slot (job_arrival j))%coq_nat
(time_slot >from_start_of_slot (job_arrival j))) by apply ltP.
cases (time_slot > from_start_of_slot (job_arrival j)) as hgt.
- apply decPcases in gt_ref. rewrite EXISTS ltnn in hgt.
false.
case hgt:(time_slot > from_start_of_slot (job_arrival j)).
- apply decPcases in gt_ref. rewrite EXISTS ltnn in hgt. done.
- apply decPcases in gt_ref.
destruct (TDMA_policy_case_RT_le_Period (job_arrival j)) as [hj |hj]. apply pendingArrival.
unfold in_time_slot_at in hj.
+ unfold from_start_of_slot in gt_ref.
move /ltP/negP in gt_ref. contradiction.
+ rewrite /from_start_of_slot in gt_ref. rewrite /from_start_of_slot in EXISTS. case (_ < _) in gt_ref;try ssromega.
+ have F:in_time_slot_at (job_arrival j) = false by auto. rewrite F.
rewrite /to_next_slot EXISTS /duration_to_finish_from_start_of_slot_with.
rewrite mulnBl mul1n addnA {1}gtn_eqF // -COST_WCET.
......
Require Import Arith Nat.
Require Import rt.util.all rt.util.tactics_gr.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task
rt.model.arrival.basic.job
rt.model.schedule.uni.schedule
......@@ -124,14 +124,14 @@ Module end_time.
job_end_time_p t c e.
Proof.
induction wf as [| wf' IHwf']; intros t c; simpl.
- destruct c; intros H; inverts H.
- destruct c; intros H; inversion H .
apply C0_.
- intros IHSwf. cases (scheduled_at sched job t) as Hcases; destruct c.
- intros IHSwf. case Hcases:(scheduled_at sched job t); destruct c.
+ inversion IHSwf. apply C0_.
+ apply IHwf' in IHSwf. apply S_C_sched with (c:=c)(e:=e).
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_sched with (c:=c)(e:=e).
apply Hcases. apply IHSwf.
+ inversion IHSwf. apply C0_.
+ apply IHwf' in IHSwf. apply S_C_not_sched with (c:=c)(e:=e).
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_not_sched with (c:=c)(e:=e).
* rewrite Hcases. done.
* apply IHSwf.
Qed.
......@@ -148,8 +148,8 @@ Module end_time.
induction H as [t|t c e Hcase1 Hpre [wf Hwf] |t c e Hcase2 Hpre [wf Hwf]].
- exists 1. done.
- exists (1+wf).
cases (scheduled_at sched job t) as Csa.
+ false.
case Csa:(scheduled_at sched job t).
+ done.
+ simpl. rewrite Csa. apply Hwf.
- exists (1+wf). simpl.
rewrite Hcase2. apply Hwf.
......@@ -165,7 +165,7 @@ Module end_time.
Proof.
intros* Hcase1 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; false.
inversion Hpre; try apply H2; done.
Qed.
(* If we consider a time t where the job is scheduled, then the end_time_predicate
......@@ -178,7 +178,7 @@ Module end_time.
Proof.
intros* Hcase2 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; false.
inversion Hpre; try apply H2; done.
Qed.
(* Assume that the job end time is job_end *)
......@@ -225,7 +225,7 @@ Module end_time.
- by rewrite big_geq.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
cases (scheduled_at sched job t) as cases; try easy; false.
case cases:(scheduled_at sched job t); try easy; done.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
rewrite Hcase2 //.
......@@ -271,7 +271,7 @@ Module end_time.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
rewrite big_ltn // IHHpre /service_at /service_during.
cases (scheduled_at sched job t). false. done.
case C:(scheduled_at sched job t);done.
- destruct c.
+ inversion Hpre. apply big_geq. ssromega.
+ apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
......
This diff is collapsed.
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