Cleanup job and task files

job.v

 Require Import task util_lemmas ssrnat ssrbool eqtype.  
 
+(* Properties of different types of job: *)
 Module Job.
 
-  (*We define valid parameters for different types of jobs ...*) 
-  (*...for a job*)
+  (* 1) Basic Job *)
   Section ValidJob.
 
     Context {Job: eqType}.
@@ -11,11 +11,12 @@ Module Job.
 
     Variable j: Job.
 
+    (* The job cost must be positive. *)
     Definition job_cost_positive (j: Job) := job_cost j > 0.
 
   End ValidJob.
 
-  (*... for a real time job (with a deadline) ...*)
+  (* 2) real-time job (with a deadline) *)
   Section ValidRealtimeJob.
 
     Context {Job: eqType}.
@@ -24,8 +25,9 @@ Module Job.
     
     Variable j: Job.
 
-    Definition job_cost_le_deadline := job_cost j <= job_deadline j.
+    (* The job deadline must be positive and no less than its cost. *)
     Definition job_deadline_positive := job_deadline j > 0.
+    Definition job_cost_le_deadline := job_cost j <= job_deadline j.
         
     Definition valid_realtime_job :=
       job_cost_positive job_cost j /\
@@ -34,7 +36,7 @@ Module Job.
 
   End ValidRealtimeJob.
 
-  (* ... for a job of a sporadic task ...*)
+  (* 3) Job of sporadic task *)
   Section ValidSporadicTaskJob.
 
     Context {sporadic_task: eqType}.
@@ -48,8 +50,11 @@ Module 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).
+
+    (* The job deadline must be equal to the task deadline. *)
     Definition job_deadline_eq_task_deadline :=
       job_deadline j = task_deadline (job_task j).
 
@@ -60,7 +65,7 @@ Module Job.
 
   End ValidSporadicTaskJob.
 
-  (*... for a job of a sporadic task with jitter ...*)
+  (* 4) Job of sporadic task with jitter *)
   Section ValidSporadicTaskJobWithJitter.
 
     Context {sporadic_task: eqType}.
@@ -76,6 +81,7 @@ Module Job.
     
     Variable j: Job.
 
+    (* The job jitter cannot be larger than the task (maximum) jitter.*)
     Definition job_jitter_leq_task_jitter :=
       job_jitter j <= task_jitter (job_task j).
 

task.v

 Require Import Vbase util_lemmas ssrnat ssrbool eqtype fintype seq.
 
+(* Attributes of a valid sporadic task. *)
 Module SporadicTask.
-  (* Next we define valid parameters for a sporadic task*)
+
   Section BasicTask.
     Context {Task: eqType}.
     Variable task_cost: Task -> nat.
@@ -10,10 +11,13 @@ Module SporadicTask.
 
     Section ValidParameters.
       Variable tsk: Task.
-    
+
+      (* The cost, period and deadline of the task must be positive. *)
       Definition task_cost_positive := task_cost tsk > 0.
       Definition task_period_positive := task_period 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.
       Definition task_cost_le_period := task_cost tsk <= task_period tsk.
 
@@ -27,14 +31,16 @@ Module SporadicTask.
 
 End SporadicTask.
 
+(* Definition and properties of a task set. *)
 Module SporadicTaskset.
   Export SporadicTask.
 
-  (* In this section we define a task set as a sequence of tasks. *)
   Section TasksetDefs.
- 
-    Definition taskset_of (T: eqType) := seq T.
 
+    (* A task set is just a sequence of tasks. *)
+    Definition taskset_of (Task: eqType) := seq Task.
+
+    (* Next, we define some properties of a task set. *)
     Section TasksetProperties.
 
       Context {Task: eqType}.
@@ -47,11 +53,13 @@ Module SporadicTaskset.
 
       Variable ts: taskset_of Task.
 
+      (* A valid sporadic taskset only contains valid tasks. *)
       Definition valid_sporadic_taskset :=
         forall tsk,
           tsk \in ts -> is_valid_task tsk.
 
-      (* Deadline models: implicit, restricted or arbitrary *)
+      (* A task set can satisfy one of three deadline models:
+         implicit, restricted, or arbitrary. *)
       Definition implicit_deadline_model :=
         forall tsk,
           tsk \in ts -> task_deadline tsk = task_period tsk.