Commit 84e2e2c7 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Hack up task definitions with jitter

parent ebc9b234
......@@ -54,6 +54,27 @@ Module Job.
End ValidSporadicTaskJob.
Section ValidSporadicTaskJobWithJitter.
Import SporadicTaskWithJitter.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task_with_jitter.
Variable job_jitter: Job -> nat.
Variable j: Job.
Definition job_jitter_leq_task_jitter :=
job_jitter j <= task_jitter (job_task j).
Definition valid_sporadic_job_with_jitter :=
valid_sporadic_job job_cost job_deadline job_task j /\
job_jitter_leq_task_jitter.
End ValidSporadicTaskJobWithJitter.
End Job.
(* Definition job := (nat * nat) % type.
......
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile apa.v BertognaResponseTimeDefs.v BertognaResponseTimeFP.v divround.v eqtask_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v seq_nat_notation.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefs.v
# coq_makefile apa.v BertognaResponseTimeDefs.v BertognaResponseTimeFP.v divround.v eqtask_dec.v eqtaskjitter_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v
#
.DEFAULT_GOAL := all
......@@ -80,8 +80,7 @@ endif
# #
######################
VFILES:=apa.v\
BertognaResponseTimeDefs.v\
VFILES:=BertognaResponseTimeDefs.v\
BertognaResponseTimeFP.v\
divround.v\
extralib.v\
......@@ -97,6 +96,7 @@ VFILES:=apa.v\
TaskArrivalDefs.v\
TaskDefs.v\
Vbase.v\
WorkloadDefsJitter.v\
WorkloadDefs.v
-include $(addsuffix .d,$(VFILES))
......
Require Import Vbase helper ssrnat.
Require Import Vbase helper ssrnat ssrbool fintype seq.
Module SporadicTask.
......@@ -31,8 +31,24 @@ Module SporadicTask.
End SporadicTask.
Module SporadicTaskWithJitter.
Import SporadicTask.
Definition sporadic_task_with_jitter := (sporadic_task * nat) % type.
Section TaskParameters.
Coercion task_with_jitter_is_task (tsk: sporadic_task_with_jitter) :=
pair_1st tsk.
Definition task_jitter (tsk: sporadic_task_with_jitter) := pair_2nd tsk.
End TaskParameters.
(* Assume decidable equality for computations involving tasks. *)
Load eqtaskjitter_dec.
End SporadicTaskWithJitter.
Module SporadicTaskset.
Require Import ssrbool fintype seq.
Export SporadicTask.
(* Define task set as a sequence of sporadic tasks. *)
......@@ -57,3 +73,13 @@ Module SporadicTaskset.
End TasksetProperties.
End SporadicTaskset.
Module SporadicTasksetWithJitter.
Export SporadicTaskWithJitter SporadicTaskset.
Definition sporadic_taskset_with_jitter := seq sporadic_task_with_jitter.
Coercion taskset_with_jitter_is_taskset (ts: sporadic_taskset_with_jitter) := map task_with_jitter_is_task ts.
End SporadicTasksetWithJitter.
\ No newline at end of file
......@@ -9,7 +9,6 @@ Axiom eqn_task : Equality.axiom task_eq_dec.
Canonical task_eqMixin := EqMixin eqn_task.
Canonical task_eqType := Eval hnf in EqType sporadic_task task_eqMixin.
(*Definition task_eq_dec (x y: sporadic_task) : {x = y} + {x <> y}.
destruct x, y.
destruct (eq_op task_id0 task_id1) eqn:Eid;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment