Commit a622a142 authored by Lucien RAKOTOMALALA's avatar Lucien RAKOTOMALALA

Merge branch 'refrac-F-functions' into network-calculus

parents 554f0155 366e2a99
This diff is collapsed.
......@@ -234,6 +234,32 @@ Qed.
Let f_S1_out := [ffun i => tnth [tuple f1_S1; f2_S1; f3_S1] i].
Import GDioid.
Lemma Fplus_val_div (f g : Fplus) : Fplus_val (f / g) = (Fplus_val f / Fplus_val g).
Proof.
apply /led_antisym /andP; split.
{
rewrite -mul_div_equiv muldC.
rewrite -[_ * _ ]/(Fplus_val (g * (f / g))).
rewrite -[Fplus_val _ <= Fplus_val _]/(f <= g * (f / g)).
rewrite muldC mul_div_equiv.
apply led_reflexive.
}
(* rewrite -[Fplus_val _ <= Fplus_val _]/((f / g) <= (mk_Fplus H)). *)
(* rewrite -mul_div_equiv. muldC. *)
(* apply /Fup_leP => {H} t /=. *)
(* rewrite F_plus_val_min_conv. *)
(* move : t. *)
(* apply /Fplus_leP. *)
(* rewrite -Fplus_min_convE. *)
(* rewrite muldC mul_div_equiv . *)
(* apply led_reflexive. *)
(* Qed. *)
Admitted.
Lemma UIB_departure_S1 i :
is_maximal_arrival (
[ffun i => tnth [tuple F1_S1; F2_S1; F3_S1] i] i)
......@@ -244,7 +270,8 @@ case i => n; case n => {n} [|n].
{
move => j.
rewrite /f1_S1.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S1 (Ordinal j) alpha_S1) F1);
[ |by apply min_residual_service_S1 | by []].
rewrite /residual_server_constr.
......@@ -266,7 +293,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f2_S1.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S1 (Ordinal j) alpha_S1) F2);
[ | by apply min_residual_service_S1 | by [] ].
rewrite /residual_server_constr.
......@@ -286,7 +313,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f3_S1.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S1 (Ordinal j) alpha_S1) F3);
[ |by apply min_residual_service_S1 | by [] ].
rewrite /residual_server_constr.
......@@ -328,7 +355,7 @@ Qed.
Lemma UIB_departure_S2_1 :
is_maximal_arrival F1_S2 f1_S2.
Proof.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp
(residual_server_constr S2_1 ord0 [ffun => f1_S1]) F1_S1);
[ | by apply min_residual_service_S2_1 | by []].
......@@ -397,7 +424,7 @@ Qed.
Lemma UIB_departure_S2_2 :
is_maximal_arrival F2_S2 f2_S2.
Proof.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp
(residual_server_constr S2_2 ord0 [ffun => f2_S1]) F2_S1);
[ | by apply min_residual_service_S2_2 | by []].
......@@ -467,7 +494,7 @@ Qed.
Lemma UIB_departure_S2_3 :
is_maximal_arrival F3_S2 f3_S2.
Proof.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp
(residual_server_constr S2_3 ord0 [ffun => f3_S1]) F3_S1);
[ |by apply min_residual_service_S2_3 | by []].
......@@ -548,7 +575,7 @@ case i => n; case n => {n} [|n].
{
move => j.
rewrite /f1_S3.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S3 (Ordinal j) alpha_S3) F1_S2);
[ |by apply min_residual_service_S3 | by []].
rewrite /residual_server_constr.
......@@ -568,7 +595,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f4_S3.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S3 (Ordinal j) alpha_S3) F4);
[ |by apply min_residual_service_S3 | by []].
rewrite /residual_server_constr.
......@@ -637,7 +664,7 @@ case i => n; case n => {n} [|n].
{
move => j.
rewrite /f3_S4.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S4 (Ordinal j) alpha_S4) F3_S2);
[ |by apply min_residual_service_S4 | by []].
rewrite /residual_server_constr.
......@@ -657,7 +684,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f5_S4.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S4 (Ordinal j) alpha_S4) F5);
[ |by apply min_residual_service_S4 | by []].
rewrite /residual_server_constr.
......@@ -734,7 +761,7 @@ case i => n; case n => {n} [|n].
{
move => j.
rewrite /f3_S4.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S5 (Ordinal j) alpha_S5) F1_S3);
[ |by apply min_residual_service_S5 | by []].
rewrite /residual_server_constr.
......@@ -754,7 +781,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f5_S4.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S5 (Ordinal j) alpha_S5) F2_S2);
[ |by apply min_residual_service_S5 | by []].
rewrite /residual_server_constr.
......@@ -774,7 +801,7 @@ case n => {n} [|n].
{
move => j.
rewrite /f3_S5.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S5 (Ordinal j) alpha_S5) F3_S4);
[ |by apply min_residual_service_S5 | by []].
rewrite /residual_server_constr.
......@@ -842,7 +869,7 @@ rewrite !ffunE.
case i => n; case n => {n} [|n].
{
move => j.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S6 (Ordinal j) alpha_S6) F4_S3);
[ |by apply min_residual_service_S6 | by []].
rewrite /residual_server_constr.
......@@ -861,7 +888,7 @@ case i => n; case n => {n} [|n].
case n => {n} [|n].
{
move => j.
rewrite Fup_val_div.
rewrite Fup_val_div Fplus_val_div.
apply (@output_arrival_curve_mp (residual_server_constr S6 (Ordinal j) alpha_S6) F5_S4);
[ |by apply min_residual_service_S6 | by []].
rewrite /residual_server_constr.
......
......@@ -70,7 +70,7 @@ rewrite (Fplus_dflow HAA) => {H1} H1.
move : (H2 _ _ S2').
rewrite (Fplus_dflow HDD) => {H2} H2.
apply (led_trans H2).
rewrite (@muldA Fplus_dioid).
rewrite muldA.
by apply led_mul2r.
Qed.
......@@ -709,6 +709,7 @@ Lemma UIB_sum_dflow n (A : dflow^n.+1) (alpha : Fup^n.+1) :
Proof.
move=> sum_alpha t d /=; rewrite /Rbar_minus /=.
rewrite -[(_ + - _)%Re]/((\sum_i (A i (t + d)%nnR : R) - (\sum_i (A i t : R)))%Ri).
rewrite /Fplus_val /=.
rewrite -GRing.sumrB /= -sum_Rbar_R -sum_Rbar_nnRbar.
apply Rbar_leq_sum => i _.
apply sum_alpha.
......@@ -730,7 +731,6 @@ case x => [] [x''| |] Hx''.
by exfalso; move: Hx'' => /Rbar_le_bool_Rbar_le.
Qed.
Lemma sum_Rbar_R n (F : 'I_n -> R) : \sum_i F i = \big[Rplus/0%Re]_i F i.
Proof.
by elim: n F => [|n IHn] F; [rewrite !big_ord0|rewrite !big_ord_recl IHn].
......@@ -779,7 +779,9 @@ split; [|split].
{ by move => t; rewrite -HdD Hd. }
exists A, D; split; [by []|split; [by[]|split; [by []|]]].
move => j.
by rewrite -(@is_maximal_arrival_eq _ _ (alpha j) _(HaA j)).
rewrite -(@is_maximal_arrival_eq (a j) (A j) (alpha j) _ ) => // t.
rewrite /Fplus_val /= nnRbar_valE.
by f_equal; rewrite HaA.
Qed.
(* TODO : old version *)
......@@ -810,7 +812,8 @@ remember del as d' eqn:Hd'; move: Hd'; rewrite {}/del => Hd'.
move: Hd'.
apply (case_nnRbar d') => [{d'} d'|] Hd'; last first.
{
apply /Fplus_leP => t.
apply /F_min_leP => t.
(* apply /Fplus_leP => t. *)
rewrite delta_infty /id_Fplus /=.
move : Had => [a [? [Haa' ?]]].
have -> : Ai = ((a i)).
......@@ -824,11 +827,15 @@ apply (case_nnRbar d') => [{d'} d'|] Hd'; last first.
rewrite dflow_start.
apply nnRbar_pos.
}
apply /Fplus_leP => t.
rewrite Hdd.
apply /F_min_leP => t.
(* apply /Fplus_leP => t. *)
rewrite /Fplus_val (Hdd t).
set Had' := Had.
move : Had' => [a [d [Haa' [Hdd' ?]]]].
rewrite (Fplus_inj Haa) (Fplus_inj (Haa' i)) delta_prop_conv.
rewrite (Fplus_inj Haa) (Fplus_inj (Haa' i)).
have -> : ((a i : F) * (delta d' : F))%D t
= id_Fplus (((a i : Fup)* (delta d' : Fup))%D) t; [by []|].
rewrite delta_prop_conv.
rewrite -Haa'.
apply (FIFO_aggregate_server S_FIFO Had _ _ ).
rewrite -(sum_dflow_FplusE Haa').
......@@ -860,7 +867,9 @@ apply (@Service_for_a_jitter (sum_dflow a) (aggregate_server S)) => //.
apply UIB_sum_dflow => j.
move : (Halpha j).
apply is_maximal_arrival_eq => //.
by apply fsym.
apply fsym => t'.
rewrite /Fplus_val /= nnRbar_valE.
by rewrite (Haa' j t').
}
exists (sum_dflow a), (sum_dflow d).
split; [by []| split; [by []| ]].
......
......@@ -18,10 +18,10 @@ Unset Printing Implicit Defensive.
Open Scope dioid_scope.
Definition is_maximal_arrival (f phi : Fplus) :=
Definition is_maximal_arrival (f phi : F) :=
forall t d, (f (t + d)%nnR - f t <= phi d)%Rbar.
Lemma UIB_alt_def (f phi : Fplus) :
Lemma UIB_alt_def (f phi : F) :
is_maximal_arrival f phi <-> f <= f * phi.
Proof.
split => H.
......@@ -42,11 +42,13 @@ apply (Rbar_le_trans _ _ _ H).
by apply (proj2_sig (Rbar_ex_glb _)); exists t, d.
Qed.
Lemma is_maximal_arrival_eq (A A' : Fplus) (alpha alpha' : Fup) :
Lemma is_maximal_arrival_eq (A A' : F) (alpha alpha' : Fup) :
A=1 A' -> (alpha =1 alpha') ->
is_maximal_arrival A alpha <-> is_maximal_arrival A' alpha'.
Proof.
by move=> HA Halpha; split=> H t d; [rewrite -!HA -Halpha|rewrite !HA Halpha].
move=> HA Halpha; split=> H t d;
[rewrite -!HA /Fplus_val -Halpha|rewrite !HA /Fplus_val Halpha];
apply H.
Qed.
(** Propositions 31 (1)) p 122 *)
......@@ -84,21 +86,21 @@ Theorem output_arrival_curve (S : Fplus -> Fplus -> Prop) beta_m beta_M sigma (A
(H_sigma : shaper_server sigma S)
alpha (H_alpha : is_maximal_arrival A alpha) :
forall D, S A D ->
is_maximal_arrival D (((alpha * beta_M) / beta_m) ^ sigma).
is_maximal_arrival D (((alpha * beta_M) / beta_m) ^ (sigma : F)).
Proof.
move => D HAD; apply UIB_F_min.
{
rewrite UIB_alt_def muldC mul_div_equiv.
apply (@led_trans _ ((((A : Fplus) * beta_M) / (A : Fplus)) / beta_m)).
apply (@led_trans _ ((((A : F) * beta_M) / (A : F)) / beta_m)).
{ apply led_divl.
rewrite (muldC (A : Fplus)).
rewrite (muldC (A : F)).
refine (led_trans _ (mul_divA _ _ _)).
rewrite muldC.
by apply led_mul2l, UIB_deconv2.
}
rewrite -div_mul (muldC beta_m).
apply (@led_trans _ (((A : Fplus) * beta_M) / (D : Fplus))).
{ by apply led_divr, H_beta_m. }
apply (@led_trans _ (((A : F) * beta_M) / (D : F))).
{ by apply led_divr, H_beta_m. }
by apply led_divl, (H_beta_M A).
}
rewrite UIB_alt_def.
......@@ -116,11 +118,11 @@ Qed.
Lemma Fup_one_is_max_service (S : server) : is_max_service S Fup_one.
Proof.
move => A D H; rewrite Fup_oneE muld1.
apply /Fplus_leP => t.
apply /F_min_leP => t.
apply (server_leq H).
Qed.
Lemma Fup_zero_is_shaper_server S :
Lemma Fup_zero_is_shaper_server (S : Fplus -> Fplus -> Prop):
shaper_server Fup_zero S.
Proof.
move => A D H; rewrite Fup_zeroE muld0.
......@@ -129,10 +131,10 @@ Qed.
(* Corollary 4 p.138 *)
Corollary output_arrival_curve_mp (S : server) (A D : dflow)
(alpha : Fup) (beta : Fplus) :
(alpha : Fup) (beta : F) :
S A D ->
is_min_service S beta -> is_maximal_arrival A alpha ->
is_maximal_arrival D ((alpha : Fplus) / beta).
is_maximal_arrival D ((alpha : F) / beta).
Proof.
(* some preprocessing *)
rewrite !UIB_alt_def.
......@@ -141,7 +143,8 @@ move: SAD => /server_leq /Fplus_leP HAD.
(* goal is now: D <= D * (alpha / beta)
under hypotheses: Halpha : A <= A * alpha, Hbeta : A * beta <= D, HAD : D <= A *)
rewrite muldC mul_div_equiv. (* goal: D / D <= alpha / beta *)
refine (led_trans _ (led_div HAD Hbeta)). (* A / (A * beta) <= alpha / beta *)
refine (led_trans _ (@led_div _ (A : F) (D : F) _ _ _ Hbeta)); [|apply HAD].
(* A / (A * beta) <= alpha / beta *)
rewrite muldC div_mul. (* A / A / beta <= alpha / beta *)
apply led_divl. (* A / A <= alpha *)
by rewrite -mul_div_equiv muldC.
......
......@@ -146,10 +146,26 @@ Record serverTotal := {
_ : forall A, exists D, server_f server_t A D
}.
(* Definition server_Fup (S : server) (A D : Fup) : Prop := *)
(* Definition server_F (S : server) (A D : F) : Prop := *)
(* exists A' D' : dflow, *)
(* (A =1 A' :> Fup) /\ (D =1 D' :> Fup) /\ server_f S A' D'. *)
(* Coercion server_Fup : server >-> Funclass. *)
(* (A =1 A' :> F) /\ (D =1 D' :> F) /\ server_f S A' D'. *)
(* Coercion server_F : server >-> Funclass. *)
(* Lemma server_FE (S : server) (A D : dflow) : S A D <-> server_f S A D. *)
(* Proof. *)
(* split. *)
(* { move=> [A' [D' [HA' [HD' HA'D']]]]. *)
(* have-> : A = A'. *)
(* { apply dflow_inj. *)
(* apply functional_extensionality => t. *)
(* by move: (HA' t) => [] /val_inj. } *)
(* have-> : D = D'. *)
(* { apply dflow_inj, functional_extensionality => t. *)
(* by move: (HD' t) => [] /val_inj. } *)
(* by []. } *)
(* by move=> H; exists A, D; split; [|split]. *)
(* Qed. *)
Definition server_Fplus (S : server) (A D : Fplus) : Prop :=
exists A' D' : dflow,
(A =1 A' :> Fplus) /\ (D =1 D' :> Fplus) /\ server_f S A' D'.
......@@ -191,7 +207,7 @@ Lemma server_leq_dflow (S : server) (A D : dflow)
Proof.
move => t; rewrite -[Rle _ _]/(Rbar_le (D t) (A t)).
rewrite !nnRbar_valE !nnRbar_dflowE.
apply (@server_leq S);
move : t; apply (@server_leq S).
by rewrite !server_FplusE.
Qed.
......@@ -305,7 +321,7 @@ split.
split; [by rewrite nserver_FplusE| split].
{
apply Fplus_inj => t.
rewrite Ha /= HaA.
rewrite Ha /Fplus_val /= (HaA t) /=.
apply nnRbar_inj => /=.
move: A {HAD HaA HdD S D}.
elim: n => [|n IHn] A.
......@@ -322,7 +338,7 @@ split.
by apply eq_bigr => i _; rewrite !ffunE.
}
apply Fplus_inj => t.
rewrite Hd /= HdD.
rewrite Hd /Fplus_val /= (HdD t) /=.
apply nnRbar_inj => /=.
move: D {HAD HaA HdD S A}.
elim: n => [|n IHn] D.
......@@ -343,23 +359,28 @@ exists (sum_dflow A'), (sum_dflow D').
split; [|split].
{ rewrite HA.
move: A A' HAA' {HAD HA S D D' HD HDD'}.
elim: n => [|n IHn] A A' HAA'; move=> t; apply nnRbar_inj.
elim: n => [|n IHn] A A' HAA'; move=> t /=; apply nnRbar_inj.
{ by rewrite /= !big_ord_recl /= !big_ord0 GRing.addr0 /= Rbar_plus_0_r HAA'. }
rewrite big_ord_recl /= /GRing.add /=.
rewrite /Fplus_val /=.
rewrite [in RHS]big_ord_recl /=.
rewrite -[Finite (Rplus ?[a] ?[b])]/((Finite ?[a] + Finite ?[b])%Rbar).
apply f_equal2; [by rewrite HAA'|].
have -> : \big[Fplus_plus/Fplus0]_i A (lift ord0 i)
= \big[Fplus_plus/Fplus0]_i [ffun k => A (lift ord0 k)] i.
{ by apply eq_bigr => i _; rewrite ffunE. }
move : IHn; rewrite /Fplus_val => IHn.
rewrite (IHn _ [ffun k => A' (lift ord0 k)]).
{ by rewrite /=; apply /f_equal /eq_bigr => i _; rewrite ffunE. }
by move=> i; rewrite !ffunE. }
move=> i; rewrite !ffunE.
apply HAA'.
}
{ rewrite HD.
move: D D' HDD' {HAD HD S A A' HA HAA'}.
elim: n => [|n IHn] D D' HDD'; move=> t; apply nnRbar_inj.
elim: n => [|n IHn] D D' HDD'; move=> t ; apply nnRbar_inj.
{ by rewrite /= !big_ord_recl /= !big_ord0 GRing.addr0 /= Rbar_plus_0_r HDD'. }
rewrite big_ord_recl /= /GRing.add /=.
rewrite /Fplus_val /=.
rewrite [in RHS]big_ord_recl /=.
rewrite -[Finite (Rplus ?[a] ?[b])]/((Finite ?[a] + Finite ?[b])%Rbar).
apply f_equal2; [by rewrite HDD'|].
......@@ -368,7 +389,8 @@ split; [|split].
{ by apply eq_bigr => i _; rewrite ffunE. }
rewrite (IHn _ [ffun k => D' (lift ord0 k)]).
{ by rewrite /=; apply /f_equal /eq_bigr => i _; rewrite ffunE. }
by move=> i; rewrite !ffunE. }
move=> i; rewrite !ffunE.
apply HDD'. }
by exists A', D'.
Qed.
......@@ -398,27 +420,29 @@ Lemma residual_serverE n (S : n.-server) i (Ai Di : Fplus) :
Proof.
split.
{
rewrite /Fplus_val /=.
move => [A' [D' [HAA' [HDD' [A'' [D'' [HA''D'' [HA'A'' HD'D'']]]]]]]].
exists [ffun j => A'' j : Fplus].
exists [ffun j => D'' j : Fplus].
rewrite nserver_FplusE.
rewrite !ffunE.
split; [by []| split => t].
{ rewrite HAA'.
{
apply nnRbar_inj => /=.
rewrite HAA' /Fplus_val /=.
apply f_equal.
by rewrite HA'A''. }
rewrite HDD'.
apply nnRbar_inj => /=.
rewrite HDD' /Fplus_val /=.
apply f_equal.
by rewrite HD'D''.
}
move => [A [D [[A' [D' [HAA' [HDD' HAD]]]]] [HAiA HDiD]]].
exists (A' i), (D' i).
split.
{ by move=> t; rewrite HAiA HAA'. }
{ by move=> t; rewrite /Fplus_val /= HAiA HAA'. }
split.
{ by move=> t; rewrite HDiD HDD'. }
{ by move=> t; rewrite /Fplus_val HDiD HDD'. }
by exists A', D'.
Qed.
......@@ -428,30 +452,34 @@ Qed.
(* def p126 *)
(* Final : def 5.3 p106 *)
(* TODO : why don't use F instead of Fplus ? --> To be Test*)
Definition is_min_service_for (S : Fplus -> Fplus -> Prop) (beta : Fplus) A :=
forall D, S A D -> A * beta <= D.
Definition is_min_service_for (S : Fplus -> Fplus -> Prop) (beta : F) A:=
forall D, S A D -> (A : F) * beta <= (D : F).
Definition is_min_service S beta := forall A, is_min_service_for S beta A.
Definition backlogged_period (A D : F) (u v : R) :=
forall x : nnR, u < x <= u + v -> (D x < A x)%Rbar.
(** Strict service *)
(* def p128 *)
(* Final : def 5.5 p108 *)
Definition is_strict_min_service (S : server) (beta : Fplus) :=
Definition is_strict_min_service (S : Fplus -> Fplus -> Prop) (beta : F) :=
forall A D, S A D ->
forall u v : nnR, (forall x : nnR, u < x <= u + v -> (D x < A x)%Rbar) ->
Rbar_le (beta v) (D (nnR_plus u v) - D u).
forall u v : nnR, backlogged_period A D u v ->
(beta v <= D (nnR_plus u v) - D u)%Rbar.
(** Max service *)
(* def p132 *)
(* Final : def 5.6 p113 *)
Definition is_max_service (S : Fplus -> Fplus -> Prop) (beta : Fplus) :=
forall A D, S A D -> D <= A * beta.
Definition is_max_service (S : Fplus -> Fplus -> Prop) (beta : F) :=
forall A D, S A D -> (D : F) <= (A : F) * beta.
(** Shaper *)
(* def p133 *)
(* Final : def 5.7 p113 *)
(* TODO voir differance avec reelle définition! sigma F0up normalement *)
Definition shaper_server (sigma : Fup) (S : Fplus -> Fplus -> Prop) :=
forall A D, S A D -> D <= D * sigma.
forall A D, S A D -> D <= D * (sigma : Fplus).
(** *** Definition of Pur delay **)
(* Def 18 p 60 *)
......
......@@ -23,13 +23,7 @@ Local Open Scope F_scope.
Local Open Scope Rbar_scope.
Local Open Scope dioid_scope.
(* Definition FIFO_service_policy n (S : n.+1.-server ) := *)
(* forall A D, S A D -> forall i j, forall t u : nnR, *)
(* (A i) u < (D i ) t -> (A j) u <= (D j) t. *)
(* Search "biject". *)
(* Locate bijective -> ssrfun *)
(* + faire une définition de priorité *)
Section static_priority.
Definition preemptive_SP n (S : (n.+1).-server) :=
forall i, forall t s : nnR, forall A D, S A D -> (s <= t)%Re
......@@ -46,3 +40,6 @@ Theorem SP_residual_service_curve n (S : (n.+1).-server) A D alpha (beta : Fplus
is_strict_min_service (residual_server S (inord i)) (beta (inord i)).
Proof.
move => HAD HS Hbeta i Halpha a d Had u v Huv.
Admitted.
End static_priority.
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