From 90f217ce0b8bcd981b2f0be2b92adcc3cc6085e8 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 13 Oct 2015 17:20:30 +0200
Subject: [PATCH] Before making changes
---
BertognaResponseTimeDefs.v | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/BertognaResponseTimeDefs.v b/BertognaResponseTimeDefs.v
index 7b2b26fa1..a7f1e3949 100644
--- a/BertognaResponseTimeDefs.v
+++ b/BertognaResponseTimeDefs.v
@@ -826,6 +826,16 @@ Module ResponseTimeAnalysis.
else None
end) ts.
+ Definition R_list' : option (seq task_with_response_time) :=
+ foldr (fun tsk hp_pairs =>
+ if hp_pairs is Some rt_bounds then
+ let R := per_task_rta tsk rt_bounds (max_steps tsk) in
+ if R <= task_deadline tsk then
+ Some (rcons rt_bounds (tsk, R))
+ else None
+ else None)
+ (Some [::]) ts.
+
Definition fp_schedulability_test := R_list != None.
(*Section AuxiliaryLemmas.
@@ -1100,6 +1110,7 @@ Module ResponseTimeAnalysis.
Hypothesis H_test_passes: fp_schedulability_test.
(*..., then no task misses its deadline. *)
+
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by tsk.
Proof.
--
GitLab