Skip to content
Snippets Groups Projects
Commit fe7f53ce authored by Sergey Bozhko's avatar Sergey Bozhko :eyes:
Browse files

remove some prints and warnings

parent f5252f57
No related branches found
No related tags found
1 merge request!1Formalize pRTA from "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited"
...@@ -145,5 +145,3 @@ Section WCETisAxiomaticPWCET. ...@@ -145,5 +145,3 @@ Section WCETisAxiomaticPWCET.
Qed. Qed.
End WCETisAxiomaticPWCET. End WCETisAxiomaticPWCET.
Print Assumptions WCET_is_axiomatic_pWCET.
...@@ -105,5 +105,3 @@ Section MainLemma. ...@@ -105,5 +105,3 @@ Section MainLemma.
Qed. Qed.
End MainLemma. End MainLemma.
Print Assumptions probabilistic_rt_monotonicity_of_iid_pWCET.
...@@ -470,5 +470,3 @@ Section WCDFPIsBounded. ...@@ -470,5 +470,3 @@ Section WCDFPIsBounded.
Qed. Qed.
End WCDFPIsBounded. End WCDFPIsBounded.
Print Assumptions probabilistic_rta_fp.
...@@ -33,9 +33,9 @@ Section PrTaskWorkloadBoundedNthCost. ...@@ -33,9 +33,9 @@ Section PrTaskWorkloadBoundedNthCost.
(** Assume that job costs are independent of the (prob.) arrival sequence. *) (** Assume that job costs are independent of the (prob.) arrival sequence. *)
Let ξpart := partition_on_ξ μ : Ω_partition. Let ξpart := partition_on_ξ μ : Ω_partition.
Hypothesis job_costs_independent_arr_seq : Hypothesis H_job_costs_independent_arr_seq :
let ξpart := partition_on_ξ μ : Ω_partition in let ξpart := partition_on_ξ μ : Ω_partition in
forall (ξ : I ξpart) `{!PosProb μ (ξpart{ξ})} (jobs : seq Job), forall (ξ : I ξpart) `(!PosProb μ (ξpart{ξ})) (jobs : seq Job),
indep2 indep2
(mkRvar μ (fun ω => [seq job_cost j ω | j <- jobs])) (mkRvar μ (fun ω => [seq job_cost j ω | j <- jobs]))
(mkRvar μ (fun ω => ξpart{ξ} ω)). (mkRvar μ (fun ω => ξpart{ξ} ω)).
...@@ -61,7 +61,7 @@ Section PrTaskWorkloadBoundedNthCost. ...@@ -61,7 +61,7 @@ Section PrTaskWorkloadBoundedNthCost.
{ by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. } { by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
} }
eapply indep2_fn_extl; first by intros; apply: EQ. eapply indep2_fn_extl; first by intros; apply: EQ.
by apply job_costs_independent_arr_seq, PosProb0. by apply H_job_costs_independent_arr_seq, PosProb0.
Qed. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment