move non-essential job parameter definitions out of behavior

restructuring/behavior/job.v

@@ -12,9 +12,3 @@ Class JobArrival (Job : JobType) := job_arrival : Job -> 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 (Job : JobType) := job_jitter : Job -> duration.
-
-(* 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/preemption/preemption_model.v

@@ -2,12 +2,15 @@ From rt.restructuring.behavior Require Import job schedule.
 From rt.restructuring.model Require Import job task.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform with limited preemptions *)
 (** Since the notion of preemption points is based on an user-provided 
     predicate (variable job_can_be_preempted), it does not guarantee that 
     the scheduler will enforce correct behavior. For that, we must 
     define additional predicates. *)
+
+(* Definition of a generic type of parameter relating jobs to their preemption points. *)
+Class JobPreemptable (Job : JobType) := job_preemptable : Job -> duration -> bool.
+
 Section ValidPreemptionModel.
 
   (* Consider any type of tasks ... *)

restructuring/model/readiness/jitter.v

@@ -6,6 +6,9 @@ From rt.util Require Import nat.
 (* We define the readiness indicator function for models with release jitter
    (and no self-suspensions). *)
 
+(* Definition of a generic type of release jitter parameter. *)
+Class JobJitter (Job : JobType) := job_jitter : Job -> duration.
+
 Section ReadinessOfJitteryJobs.
   (* Consider any kind of jobs... *)
   Context {Job : JobType}.