Add new generic parameters

restructuring/behavior/job.v

 From rt.restructuring.behavior Require Export time.
 From mathcomp Require Export eqtype ssrnat.
 
-(* Throughout the library we assume that jobs have decidable equality *)
+(* 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 relating jobs to a discrete cost. *)
+Class JobCost (Job : JobType) := job_cost : Job -> 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 for job_arrival. *)
+Class JobArrival (Job : JobType) := job_arrival : Job -> 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 parameter relating jobs to an absolute deadline. *)
+Class JobDeadline (Job : JobType) := job_deadline : Job -> instant.
 
 (* Definition of a generic type of release jitter parameter. *)
-Class JobJitter (J : JobType) := job_jitter : J -> duration.
+Class JobJitter (Job : JobType) := job_jitter : Job -> duration.
\ No newline at end of file
+
+(* Definition of a generic type of parameter relating jobs to their preemption points. *)
+Class JobPreemptable (Job : JobType) := job_preemptable : Job -> duration -> bool.
\ No newline at end of file

restructuring/model/task.v

@@ -7,13 +7,29 @@ From rt.restructuring.behavior Require Export arrival_sequence.
 Definition TaskType := eqType.
 
 (* Definition of a generic type of parameter relating jobs to tasks *)
-Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
+Class JobTask (Job : JobType) (Task : TaskType) := job_task : Job -> Task.
+
+(* Definition of a generic type of parameter for task deadlines *)
+Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
+
+(* Definition of a generic type of parameter for task cost *)
+Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
+
+(* Definition of a generic type of parameter relating tasks 
+   to the length of the maximum nonpreeptive segment. *)
+Class TaskMaxNonpreemptiveSegment (Task : TaskType) :=
+  task_max_nonpreeptive_segment : Task -> duration.
+
+(* Definition of a generic type of parameter relating tasks
+   to theirs run-to-completion threshold. *)
+Class TaskRunToCompletionThreshold (Task : TaskType) :=
+  task_run_to_completion_threshold : Task -> duration.
 
 Section SameTask.
   
   (* For 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}.
 
   (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1
@@ -22,10 +38,6 @@ 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)
@@ -33,9 +45,6 @@ Instance job_deadline_from_task_deadline
   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.