diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 94c44060a53cbc7dd1acb1b2081034e56f99390f..b328a868bd45ca7ab913404b08a2da2ed4cdb1b6 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -252,7 +252,7 @@ Section RequestBoundFunctions.
[max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
that equals 0 for the empty interval delta = 0. *)
Context `{MaxArrivals Task}.
- Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
+ Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Let's define some local names for clarity. *)
diff --git a/model/task/arrival/arrival_curve_to_rbf.v b/model/task/arrival/arrival_curve_to_rbf.v
new file mode 100644
index 0000000000000000000000000000000000000000..c76073dfc02496ae701958a5834b76cf9208c31f
--- /dev/null
+++ b/model/task/arrival/arrival_curve_to_rbf.v
@@ -0,0 +1,174 @@
+Require Export prosa.util.all.
+Require Export prosa.model.task.arrival.request_bound_functions.
+Require Export prosa.model.task.arrival.curves.
+
+(** * Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF) *)
+
+(** Consider any type of tasks with a given cost ... *)
+Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}.
+
+(** ... and any type of jobs associated with these tasks. *)
+Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
+
+(** In the following, we show a way to convert a given arrival curve,
+ paired with a worst-case/best-case execution time, to a request-bound function.
+ Definitions and proofs will handle both lower-bounding and upper-bounding arrival
+ curves. *)
+Section ArrivalCurveToRBF.
+
+ (** Let [MaxArr] and [MinArr] represent two arrivals curves. [MaxArr] upper-bounds
+ the possible number or arrivals for a given task, whereas [MinArr] lower-bounds it. *)
+ Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}.
+
+ (** We define the conversion to a request-bound function as the product of the task cost and the
+ number of arrivals during [Δ]. In the upper-bounding case, the cost of a task will represent
+ the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will
+ represent the BCET of its jobs. *)
+ Definition task_max_rbf (arrivals : Task -> duration -> nat) task Δ := task_cost task * arrivals task Δ.
+ Definition task_min_rbf (arrivals : Task -> duration -> nat) task Δ := task_min_cost task * arrivals task Δ.
+
+ (** Finally, we show that the newly defined functions are indeed request-bound functions. *)
+ Global Program Instance MaxArrivalsRBF : MaxRequestBound Task := task_max_rbf max_arrivals.
+ Global Program Instance MinArrivalsRBF : MinRequestBound Task := task_min_rbf min_arrivals.
+
+ (** In the following section, we prove that the transformation yields a request-bound
+ function that conserves correctness properties in both the upper-bounding
+ and lower-bounding cases. *)
+ Section Facts.
+
+ (** First, we establish the validity of the transformation for a single, given task. *)
+ Section SingleTask.
+
+ (** Consider an arbitrary task [tsk] ... *)
+ Variable tsk : Task.
+
+ (** ... and any job arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** First, note that any valid upper-bounding arrival curve, after being
+ converted, is a valid request-bound function. *)
+ Theorem valid_arrival_curve_to_max_rbf:
+ forall (arrivals : Task -> duration -> nat),
+ valid_arrival_curve (arrivals tsk) ->
+ valid_request_bound_function ((task_max_rbf arrivals) tsk).
+ Proof.
+ move => ARR [ZERO MONO].
+ split.
+ - by rewrite /task_max_rbf ZERO muln0.
+ - move => x y LEQ.
+ rewrite /task_max_rbf.
+ destruct (task_cost tsk); first by rewrite mul0n.
+ by rewrite leq_pmul2l //; apply MONO.
+ Qed.
+
+ (** The same idea can be applied in the lower-bounding case. *)
+ Theorem valid_arrival_curve_to_min_rbf:
+ forall (arrivals : Task -> duration -> nat),
+ valid_arrival_curve (arrivals tsk) ->
+ valid_request_bound_function ((task_min_rbf arrivals) tsk).
+ Proof.
+ move => ARR [ZERO MONO].
+ split.
+ - by rewrite /task_min_rbf ZERO muln0.
+ - move => x y LEQ.
+ rewrite /task_min_rbf.
+ destruct (task_min_cost tsk); first by rewrite mul0n.
+ by rewrite leq_pmul2l //; apply MONO.
+ Qed.
+
+ (** Next, we prove that the task respects the request-bound function in
+ the upper-bounding case. Note that, for this to work, we assume that the
+ cost of tasks upper-bounds the cost of the jobs belonging to them (i.e.,
+ the task cost is the worst-case). *)
+ Theorem respects_arrival_curve_to_max_rbf:
+ jobs_have_valid_job_costs ->
+ respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
+ respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).
+ Proof.
+ move=> TASK_COST RESPECT t1 t2 LEQ.
+ specialize (RESPECT t1 t2 LEQ).
+ apply leq_trans with (n := task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+ - rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+ rewrite mem_filter => /andP [/eqP TSK _] _.
+ rewrite -TSK.
+ by apply TASK_COST.
+ - by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
+ Qed.
+
+ (** Finally, we prove that the task respects the request-bound function also in
+ the lower-bounding case. This time, we assume that the cost of tasks lower-bounds
+ the cost of the jobs belonging to them. (i.e., the task cost is the best-case). *)
+ Theorem respects_arrival_curve_to_min_rbf:
+ jobs_have_valid_min_job_costs ->
+ respects_min_arrivals arr_seq tsk (MinArr tsk) ->
+ respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).
+ Proof.
+ move=> TASK_COST RESPECT t1 t2 LEQ.
+ specialize (RESPECT t1 t2 LEQ).
+ apply leq_trans with (n := task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+ - by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
+ - rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+ rewrite mem_filter => /andP [/eqP TSK _] _.
+ rewrite -TSK.
+ by apply TASK_COST.
+ Qed.
+
+ End SingleTask.
+
+ (** Next, we lift the results to the previous section to an arbitrary task set. *)
+ Section TaskSet.
+
+ (** Let [ts] be an arbitrary task set... *)
+ Variable ts : TaskSet Task.
+
+ (** ... and consider any job arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** First, we generalize the validity of the transformation to a task set both in
+ the upper-bounding case ... *)
+ Corollary valid_taskset_arrival_curve_to_max_rbf:
+ valid_taskset_arrival_curve ts MaxArr ->
+ valid_taskset_request_bound_function ts MaxArrivalsRBF.
+ Proof.
+ move=> VALID tsk IN.
+ specialize (VALID tsk IN).
+ by apply valid_arrival_curve_to_max_rbf.
+ Qed.
+
+ (** ... and in the lower-bounding case. *)
+ Corollary valid_taskset_arrival_curve_to_min_rbf:
+ valid_taskset_arrival_curve ts MinArr ->
+ valid_taskset_request_bound_function ts MinArrivalsRBF.
+ Proof.
+ move=> VALID tsk IN.
+ specialize (VALID tsk IN).
+ by apply valid_arrival_curve_to_min_rbf.
+ Qed.
+
+ (** Second, we show that a task set that respects a given arrival curve also respects
+ the produced request-bound function, lifting the result obtained in the single-task
+ case. The result is valid in the upper-bounding case... *)
+ Corollary taskset_respects_arrival_curve_to_max_rbf:
+ jobs_have_valid_job_costs ->
+ taskset_respects_max_arrivals arr_seq ts ->
+ taskset_respects_max_request_bound arr_seq ts.
+ Proof.
+ move=> TASK_COST SET_RESPECTS tsk IN.
+ by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
+ Qed.
+
+ (** ...as well as in the lower-bounding case. *)
+ Corollary taskset_respects_arrival_curve_to_min_rbf:
+ jobs_have_valid_min_job_costs ->
+ taskset_respects_min_arrivals arr_seq ts ->
+ taskset_respects_min_request_bound arr_seq ts.
+ Proof.
+ move=> TASK_COST SET_RESPECTS tsk IN.
+ by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
+ Qed.
+
+ End TaskSet.
+
+ End Facts.
+
+End ArrivalCurveToRBF.
diff --git a/model/task/arrival/curves.v b/model/task/arrival/curves.v
index b8138bf2242bfbaa42f543f9291d98aaf2dfbd3f..4a49aa79e8be8f42ff6356c5310a5271e2e18051 100644
--- a/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -60,7 +60,7 @@ Section ArrivalCurves.
(** We say that a given curve [num_arrivals] is a valid arrival curve for
task [tsk] iff [num_arrivals] is a monotonic function that equals 0 for
the empty interval [delta = 0]. *)
- Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration -> nat) :=
+ Definition valid_arrival_curve (num_arrivals : duration -> nat) :=
num_arrivals 0 = 0 /\
monotone num_arrivals leq.
@@ -134,7 +134,7 @@ Section ArrivalCurvesModel.
(** We say that [arrivals] is a valid arrival curve for a task set
if it is valid for any task in the task set *)
Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
- forall (tsk : Task), tsk \in ts -> valid_arrival_curve tsk (arrivals tsk).
+ forall (tsk : Task), tsk \in ts -> valid_arrival_curve (arrivals tsk).
(** Finally, we lift the per-task semantics of the respective arrival and
separation curves to the entire task set. *)
diff --git a/model/task/arrivals.v b/model/task/arrivals.v
index 400721e5350762fb887a34ee7431b63e2c83060d..8c10fd472c2d552332cb1a96bf530abc51034328 100644
--- a/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -43,7 +43,7 @@ Section TaskArrivals.
(** ... and also count the cost of job arrivals. *)
Definition cost_of_task_arrivals (t1 t2 : instant) :=
- \sum_(j <- task_arrivals_between t1 t2 | job_task j == tsk) job_cost j.
+ \sum_(j <- task_arrivals_between t1 t2) job_cost j.
End TaskArrivals.
diff --git a/model/task/concept.v b/model/task/concept.v
index 2de3aec8290793ce107c928334a4a70d1ad3938e..c255a7bc18d1f0cc90f0648a869cb5312e03d8f7 100644
--- a/model/task/concept.v
+++ b/model/task/concept.v
@@ -26,6 +26,10 @@ Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
execution cost (WCET). *)
Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
+(** And finally, we define a task-model parameter to express each task's best-case
+ execution cost (BCET). *)
+Class TaskMinCost (Task : TaskType) := task_min_cost : Task -> duration.
+
(** * Task Model Validity *)
@@ -33,9 +37,10 @@ Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
model must satisfy. *)
Section ModelValidity.
- (** Consider any type of tasks with WCETs and relative deadlines. *)
+ (** Consider any type of tasks with WCETs/BCETs and relative deadlines. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
+ Context `{TaskMinCost Task}.
Context `{TaskDeadline Task}.
(** First, we constrain the possible WCET values of a valid task. *)
@@ -67,7 +72,11 @@ Section ModelValidity.
Definition valid_job_cost j :=
job_cost j <= task_cost (job_task j).
- (** ... and any arrival sequence. *)
+ (** Every job have a valid job cost *)
+ Definition jobs_have_valid_job_costs :=
+ forall j, valid_job_cost j.
+
+ (** Next, consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** The cost of a job from the arrival sequence cannot
@@ -78,6 +87,36 @@ Section ModelValidity.
valid_job_cost j.
End ValidJobCost.
+
+ (** Third, we relate the cost of a task's jobs to its BCET. *)
+ Section ValidMinJobCost.
+
+ (** Consider any type of jobs associated with the tasks ... *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ (** ... and consider the cost of each job. *)
+ Context `{JobCost Job}.
+
+ (** The cost of any job [j] cannot be less than the BCET of its respective
+ task. *)
+ Definition valid_min_job_cost j :=
+ task_min_cost (job_task j) <= job_cost j.
+
+ (** Every job have a valid job cost *)
+ Definition jobs_have_valid_min_job_costs :=
+ forall j, valid_min_job_cost j.
+
+ (** Next, consider any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** The cost of a job from the arrival sequence cannot
+ be less than the task cost. *)
+ Definition arrivals_have_valid_min_job_costs :=
+ forall j,
+ arrives_in arr_seq j ->
+ valid_min_job_cost j.
+
+ End ValidMinJobCost.
End ModelValidity.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 4e3df729c7a88eedbc616172f468b22cf377cea3..873a2fac99b0aa37cceb17573ba5bbd9dfb5953e 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -38,6 +38,8 @@ RBF
RBFs
WCET
WCETs
+BCET
+BCETs
Layland
Liu
sequentiality