From 8313f7c6bc335bc1ed1f4692b5d823af5d68959d Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 30 Aug 2019 14:12:01 +0200
Subject: [PATCH] update task and job models in preparation of aRTA port
Also removes an unnecessary module in rt.util.epsilon.
---
.../uni/limited/abstract_RTA/abstract_rta.v | 4 +-
.../limited/abstract_RTA/abstract_seq_rta.v | 2 +-
.../uni/limited/abstract_RTA/definitions.v | 2 +-
.../abstract_RTA/reduction_of_search_space.v | 2 +-
...sufficient_condition_for_lock_in_service.v | 2 +-
.../concrete_models/response_time_bound.v | 2 +-
.../edf/nonpr_reg/response_time_bound.v | 2 +-
.../uni/limited/edf/response_time_bound.v | 2 +-
.../concrete_models/response_time_bound.v | 2 +-
.../nonpr_reg/response_time_bound.v | 2 +-
.../fixed_priority/response_time_bound.v | 2 +-
.../uni/limited/platform/definitions.v | 2 +-
model/schedule/uni/limited/platform/limited.v | 2 +-
.../uni/limited/platform/nonpreemptive.v | 2 +-
.../uni/limited/platform/preemptive.v | 2 +-
.../platform/priority_inversion_is_bounded.v | 2 +-
model/schedule/uni/limited/schedule.v | 2 +-
restructuring/behavior/job.v | 8 +-
restructuring/model/job.v | 17 +++
.../schedule/priority_based/preemptive.v | 1 +
restructuring/model/schedule/sequential.v | 5 +-
restructuring/model/schedule/task_schedule.v | 52 ++++++++
restructuring/model/task.v | 113 +++++++++++++++++-
restructuring/model/task_arrivals.v | 9 +-
restructuring/model/task_cost.v | 35 ------
util/epsilon.v | 2 +-
26 files changed, 207 insertions(+), 71 deletions(-)
create mode 100644 restructuring/model/job.v
create mode 100644 restructuring/model/schedule/task_schedule.v
delete mode 100644 restructuring/model/task_cost.v
diff --git a/model/schedule/uni/limited/abstract_RTA/abstract_rta.v b/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
index 621e1306b..d6bd459e1 100644
--- a/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
+++ b/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
@@ -15,8 +15,8 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTA.
- Import Job Epsilon UniprocessorSchedule Service ResponseTime
- AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction.
+ Import Job UniprocessorSchedule Service ResponseTime AbstractRTADefinitions
+ AbstractRTALockInService AbstractRTAReduction.
(* In this section we prove that the maximum among the solutions of the response-time bound
recurrence is a response time bound for tsk. Note that in this section we do not rely on
diff --git a/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index 457832444..4c6fe76a1 100644
--- a/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -23,7 +23,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
and sequential jobs. *)
Module AbstractSeqRTA.
- Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
+ Import Job ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
Service ResponseTime MaxArrivalsWorkloadBound
AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction AbstractRTA.
diff --git a/model/schedule/uni/limited/abstract_RTA/definitions.v b/model/schedule/uni/limited/abstract_RTA/definitions.v
index 2bf00e626..09e0cc709 100644
--- a/model/schedule/uni/limited/abstract_RTA/definitions.v
+++ b/model/schedule/uni/limited/abstract_RTA/definitions.v
@@ -9,7 +9,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTADefinitions.
- Import Job Epsilon UniprocessorSchedule.
+ Import Job UniprocessorSchedule.
(* In this section, we introduce all the abstract notions required by the analysis. *)
Section Definitions.
diff --git a/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v b/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
index 9ce65a850..dded10d6c 100644
--- a/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
+++ b/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
@@ -10,7 +10,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
Module AbstractRTAReduction.
- Import Epsilon UniprocessorSchedule.
+ Import UniprocessorSchedule.
(* The response-time analysis we are presenting in this series of documents is based on searching
over all possible values of A, the relative arrival time of the job respective to the beginning
diff --git a/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v b/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
index cd31ebed9..79d740d04 100644
--- a/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
+++ b/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
@@ -12,7 +12,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
receives enough service to become nonpreemptive. *)
Module AbstractRTALockInService.
- Import Job Epsilon UniprocessorSchedule Service AbstractRTADefinitions.
+ Import Job UniprocessorSchedule Service AbstractRTADefinitions.
(* Previously we defined the notion of lock-in service (see limited.schedule.v file).
Lock-in service is the amount of service after which a job cannot be preempted until
diff --git a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index ac20dd718..03412a60c 100644
--- a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(4) EDF with floating nonpreemptive regions. *)
Module RTAforConcreteModels.
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+ Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
FullyNonPreemptivePlatform FullyPreemptivePlatform AbstractRTAforEDFwithArrivalCurves.
diff --git a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index a23e31d5d..c9ee30e43 100644
--- a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this module we prove a general RTA theorem for EDF-schedulers. *)
Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+ Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
AbstractRTAforEDFwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded.
diff --git a/model/schedule/uni/limited/edf/response_time_bound.v b/model/schedule/uni/limited/edf/response_time_bound.v
index be6856919..0ff63e7b4 100644
--- a/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/response_time_bound.v
@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
EDF uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTAforEDFwithArrivalCurves.
- Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask Priority
+ Import Job ArrivalCurves TaskArrival ScheduleOfTask Priority
UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
BusyIntervalJLFP LimitedPreemptionPlatform RBF Service JLFPInstantiation.
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
index 9c75772c1..8eef99ccc 100644
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(4) FP with floating nonpreemptive regions. *)
Module RTAforConcreteModels.
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+ Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
FullyNonPreemptivePlatform FullyPreemptivePlatform.
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index 1d9178193..d5d27a160 100644
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this module we prove a general RTA theorem for FP-schedulers *)
Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+ Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
AbstractRTAforFPwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded.
diff --git a/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index 58c43350a..12a68413e 100644
--- a/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
FP uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTAforFPwithArrivalCurves.
- Import Epsilon Job ArrivalCurves TaskArrival Priority ScheduleOfTask
+ Import Job ArrivalCurves TaskArrival Priority ScheduleOfTask
UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
LimitedPreemptionPlatform RBF BusyIntervalJLFP JLFPInstantiation.
diff --git a/model/schedule/uni/limited/platform/definitions.v b/model/schedule/uni/limited/platform/definitions.v
index a355e2e44..c9ceedfe3 100644
--- a/model/schedule/uni/limited/platform/definitions.v
+++ b/model/schedule/uni/limited/platform/definitions.v
@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
predicate for various preemption models. *)
Module LimitedPreemptionPlatform.
- Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority Service.
+ Import Job SporadicTaskset UniprocessorSchedule Priority Service.
(* In this section, we define a processor platform with limited preemptions. *)
Section Properties.
diff --git a/model/schedule/uni/limited/platform/limited.v b/model/schedule/uni/limited/platform/limited.v
index 0e6dd92b7..dfd07a387 100644
--- a/model/schedule/uni/limited/platform/limited.v
+++ b/model/schedule/uni/limited/platform/limited.v
@@ -13,7 +13,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
model with floating nonpreemptive regions. *)
Module ModelWithLimitedPreemptions.
- Import Epsilon Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
+ Import Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
(* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)
diff --git a/model/schedule/uni/limited/platform/nonpreemptive.v b/model/schedule/uni/limited/platform/nonpreemptive.v
index 6296c0a8d..28db01132 100644
--- a/model/schedule/uni/limited/platform/nonpreemptive.v
+++ b/model/schedule/uni/limited/platform/nonpreemptive.v
@@ -17,7 +17,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
can_be_preempted for the fully nonpreemptive model and prove its correctness. *)
Module FullyNonPreemptivePlatform.
- Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+ Import Job SporadicTaskset UniprocessorSchedule Priority
Service LimitedPreemptionPlatform.
Section FullyNonPreemptiveModel.
diff --git a/model/schedule/uni/limited/platform/preemptive.v b/model/schedule/uni/limited/platform/preemptive.v
index 5f3d24aad..83ea02c82 100644
--- a/model/schedule/uni/limited/platform/preemptive.v
+++ b/model/schedule/uni/limited/platform/preemptive.v
@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
can_be_preempted for the fully preemptive model and prove its correctness. *)
Module FullyPreemptivePlatform.
- Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+ Import Job SporadicTaskset UniprocessorSchedule Priority
Service LimitedPreemptionPlatform.
Section FullyPreemptiveModel.
diff --git a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
index 4f84902b3..35dce5a9e 100644
--- a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
+++ b/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
@@ -15,7 +15,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
is bounded. *)
Module PriorityInversionIsBounded.
- Import Epsilon Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP.
+ Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP.
Section PriorityInversionIsBounded.
diff --git a/model/schedule/uni/limited/schedule.v b/model/schedule/uni/limited/schedule.v
index a8825aa75..f09ea867c 100644
--- a/model/schedule/uni/limited/schedule.v
+++ b/model/schedule/uni/limited/schedule.v
@@ -7,7 +7,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In this file, we provide additional definitions and
lemmas about lock-in-serivce-compliant schedules. *)
- Import Job Epsilon Service UniprocessorSchedule.
+ Import Job Service UniprocessorSchedule.
Section Definitions.
diff --git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 9f0f97320..e00cd320e 100644
--- a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ -1,21 +1,17 @@
From rt.restructuring.behavior Require Export time.
-From mathcomp Require Export eqtype.
+From mathcomp Require Export eqtype ssrnat.
(* Throughout the library we assume that jobs have decidable equality *)
-
Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
-
Class JobCost (J : JobType) := job_cost : J -> duration.
(* Definition of a generic type of parameter for job_arrival *)
-
Class JobArrival (J : JobType) := job_arrival : J -> instant.
(* Definition of a generic type of parameter relating jobs to an absolute deadline *)
Class JobDeadline (J : JobType) := job_deadline : J -> instant.
(* Definition of a generic type of release jitter parameter. *)
-Class JobJitter (J : JobType) := job_jitter : J -> duration.
-
+Class JobJitter (J : JobType) := job_jitter : J -> duration.
\ No newline at end of file
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
new file mode 100644
index 000000000..ba5d58e50
--- /dev/null
+++ b/restructuring/model/job.v
@@ -0,0 +1,17 @@
+From rt.restructuring.behavior Require Export time job.
+From mathcomp Require Export eqtype ssrnat.
+
+(* In this section, we introduce properties of a job. *)
+Section PropertesOfJob.
+
+ (* Assume that job costs are known. *)
+ Context {Job : JobType}.
+ Context `{JobCost Job}.
+
+ (* Consider an arbitrary job. *)
+ Variable j: Job.
+
+ (* The job cost must be positive. *)
+ Definition job_cost_positive := job_cost j > 0.
+
+End PropertesOfJob.
\ No newline at end of file
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index 6eece44ef..c8d265402 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -25,4 +25,5 @@ Section Priority.
backlogged sched j t ->
scheduled_at sched j_hp t ->
hep_job_at t j_hp j.
+
End Priority.
diff --git a/restructuring/model/schedule/sequential.v b/restructuring/model/schedule/sequential.v
index bbbddef03..664414f6d 100644
--- a/restructuring/model/schedule/sequential.v
+++ b/restructuring/model/schedule/sequential.v
@@ -2,9 +2,10 @@ From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.model Require Export task.
Section PropertyOfSequentiality.
+
(* Consider any type of job associated with any type of tasks... *)
- Context {Job: JobType}.
- Context {Task: TaskType}.
+ Context {Job : JobType}.
+ Context {Task : TaskType}.
Context `{JobTask Job Task}.
(* ... with arrival times and costs ... *)
diff --git a/restructuring/model/schedule/task_schedule.v b/restructuring/model/schedule/task_schedule.v
new file mode 100644
index 000000000..97c6a111e
--- /dev/null
+++ b/restructuring/model/schedule/task_schedule.v
@@ -0,0 +1,52 @@
+From rt.restructuring.model Require Import task.
+From rt.restructuring.behavior Require Import schedule ideal_schedule.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* Due to historical reasons this file defines the notion of a schedule of
+ a task for the ideal uniprocessor model. This is not a fundamental limitation
+ and the notion can be further generalized to an arbitrary model. *)
+
+(** * Schedule of task *)
+(** In this section we define properties of schedule of a task *)
+Section ScheduleOfTask.
+
+ (* Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (* ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (* Let sched be any ideal uniprocessor schedule. *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ Section TaskProperties.
+
+ (* Let tsk be any task. *)
+ Variable tsk : Task.
+
+ (* Next we define whether a task is scheduled at time t, ... *)
+ Definition task_scheduled_at (t : instant) :=
+ if sched t is Some j then
+ job_task j == tsk
+ else false.
+
+ (* ...which also corresponds to the instantaneous service it receives. *)
+ Definition task_service_at (t: instant) := task_scheduled_at t.
+
+ (* Based on the notion of instantaneous service, we define the
+ cumulative service received by tsk during any interval [t1, t2)... *)
+ Definition task_service_during (t1 t2 : instant) :=
+ \sum_(t1 <= t < t2) task_service_at t.
+
+ (* ...and the cumulative service received by tsk up to time t2,
+ i.e., in the interval [0, t2). *)
+ Definition task_service (t2 : instant) := task_service_during 0 t2.
+
+ End TaskProperties.
+
+End ScheduleOfTask.
\ No newline at end of file
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index f530b0044..e583ceb74 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,15 +1,16 @@
From mathcomp Require Export ssrbool.
From rt.restructuring.behavior Require Export job.
+From rt.restructuring.behavior Require Export arrival_sequence.
+
(* Throughout the library we assume that tasks have decidable equality *)
-
Definition TaskType := eqType.
(* Definition of a generic type of parameter relating jobs to tasks *)
-
Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
Section SameTask.
+
(* For any type of job associated with any type of tasks... *)
Context {Job: JobType}.
Context {Task: TaskType}.
@@ -21,12 +22,112 @@ Section SameTask.
End SameTask.
+
(* Definition of a generic type of parameter for task deadlines *)
Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
(* Given task deadlines and a mapping from jobs to tasks we provide a generic definition of job_deadline *)
-
Instance job_deadline_from_task_deadline
- (Job : JobType) (Task : TaskType)
- `{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} :
- JobDeadline Job := fun j => job_arrival j + task_deadline (job_task j).
+ (Job : JobType) (Task : TaskType)
+ `{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JobDeadline Job :=
+ fun j => job_arrival j + task_deadline (job_task j).
+
+
+(* Definition of a generic type of parameter for task cost *)
+Class TaskCost (T : TaskType) := task_cost : T -> duration.
+
+
+(* In this section, we introduce properties of a task. *)
+Section PropertesOfTask.
+
+ (* Consider any type of tasks. *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+
+ (* Next we intrdoduce attributes of a valid sporadic task. *)
+ Section ValidTask.
+
+ (* Consider an arbitrary task. *)
+ Variable tsk: Task.
+
+ (* The cost and deadline of the task must be positive. *)
+ Definition task_cost_positive := task_cost tsk > 0.
+ Definition task_deadline_positive := task_deadline tsk > 0.
+
+ (* The task cost cannot be larger than the deadline or the period. *)
+ Definition task_cost_le_deadline := task_cost tsk <= task_deadline tsk.
+
+ End ValidTask.
+
+ (* Job of task *)
+ Section ValidJobOfTask.
+
+ (* Consider any type of jobs associated with the tasks ... *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+ Context `{JobDeadline Job}.
+
+ (* Consider an arbitrary job. *)
+ Variable j: Job.
+
+ (* The job cost cannot be larger than the task cost. *)
+ Definition job_cost_le_task_cost :=
+ job_cost j <= task_cost (job_task j).
+
+ End ValidJobOfTask.
+
+ (* Jobs of task *)
+ Section ValidJobsTask.
+
+ (* Consider any type of jobs associated with the tasks ... *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+
+ (* ... and any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (* The cost of a job from the arrival sequence cannot
+ be larger than the task cost. *)
+ Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_cost_le_task_cost j.
+
+ End ValidJobsTask.
+
+End PropertesOfTask.
+
+(* In this section, we introduce properties of a task set. *)
+Section PropertesOfTaskSet.
+
+ (* Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (* ... and any type of jobs associated with these tasks ... *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+
+ (* ... and any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (* Consider an arbitrary task set. *)
+ Variable ts : seq Task.
+
+ (* Tasks from the task set have a positive cost. *)
+ Definition tasks_cost_positive :=
+ forall tsk,
+ tsk \in ts ->
+ task_cost_positive tsk.
+
+ (* All jobs in the arrival sequence come from the taskset. *)
+ Definition all_jobs_from_taskset :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_task j \in ts.
+
+End PropertesOfTaskSet.
\ No newline at end of file
diff --git a/restructuring/model/task_arrivals.v b/restructuring/model/task_arrivals.v
index 943bebf34..1f5905db0 100644
--- a/restructuring/model/task_arrivals.v
+++ b/restructuring/model/task_arrivals.v
@@ -3,15 +3,18 @@ From rt.restructuring.model Require Export task.
(* In this file we provide basic definitions related to tasks on arrival sequences *)
Section TaskArrivals.
- Context {Job : JobType} {Task : TaskType}.
+ (* Consider any type of job associated with any type of tasks. *)
+ Context {Job: JobType}.
+ Context {Task: TaskType}.
Context `{JobTask Job Task}.
- (* Consider any job arrival sequence, *)
+ (* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
Section Definitions.
- (* And a given task *)
+
+ (* Let tsk be any task. *)
Variable tsk : Task.
(* We define the sequence of jobs of tsk arriving at time t *)
diff --git a/restructuring/model/task_cost.v b/restructuring/model/task_cost.v
deleted file mode 100644
index 014720c3d..000000000
--- a/restructuring/model/task_cost.v
+++ /dev/null
@@ -1,35 +0,0 @@
-From rt.restructuring.behavior Require Export arrival_sequence.
-From rt.restructuring.model Require Export task.
-
-Section TaskCost.
- Context {T : TaskType}.
-
- Variable (task_cost : duration).
-
- Definition valid_task_cost := task_cost > 0.
-End TaskCost.
-
-(* Definition of a generic type of parameter for task cost *)
-
-Class TaskCost (T : TaskType) := task_cost : T -> duration.
-
-Section TasksetCosts.
- Context {T : TaskType} `{TaskCost T}.
-
- Variable ts : seq T.
-
- Definition valid_taskset_costs :=
- forall tsk : T,
- tsk \in ts ->
- task_cost tsk > 0.
-
- Context {J : JobType} `{JobTask J T} `{JobCost J}.
-
- Variable arr_seq : arrival_sequence J.
-
- Definition respects_taskset_costs :=
- forall j,
- arrives_in arr_seq j ->
- job_cost j <= task_cost (job_task j).
-
-End TasksetCosts.
diff --git a/util/epsilon.v b/util/epsilon.v
index d66c6b81f..dae64637c 100644
--- a/util/epsilon.v
+++ b/util/epsilon.v
@@ -1,4 +1,4 @@
-Module Epsilon.
+Section Epsilon.
(* ε is defined as the smallest positive number. *)
Definition ε := 1.
--
GitLab