Commit 92ca9c76 authored by Pierre Roux's avatar Pierre Roux

Example

parent d01dc34e
Require Import rt.model.time rt.model.arrival.basic.task_record.
Require Import rt.model.time rt.util.n0nat rt.model.arrival.basic.task_record.
Import Time. (* This Time module in time module seems useless *)
From mathcomp
Require Import ssreflect ssrnat ssrbool eqtype seq.
......@@ -16,15 +16,13 @@ Variable T : eqType.
(* 1) Basic Job *)
Record validJob := ValidJob {
job_id :> T;
job_cost : time;
job_cost_positive : job_cost > 0
job_cost : n0nat;
}.
(* 2) real-time job (with a deadline) *)
Record validRealTimeJob := ValidRealTimeJob {
rt_job :> validJob;
job_deadline : time;
job_deadline_positive : job_deadline > 0;
job_deadline : n0nat;
job_cost_le_deadline : job_cost rt_job <= job_deadline
}.
......@@ -32,8 +30,8 @@ Record validRealTimeJob := ValidRealTimeJob {
Record validSporadicTaskJob := ValidSporadicTaskJob {
task_job :> validRealTimeJob;
task : basicTask T;
_ : job_cost task_job <= task_cost task;
_ : job_deadline task_job = task_deadline task
job_cost_le_task_cost : job_cost task_job <= task_cost task;
job_deadline_le_task_deadline : job_deadline task_job = task_deadline task
}.
End Job.
Require Import rt.model.time.
Import Time. (* This Time module in time module seems useless *)
Require Import rt.util.n0nat.
From mathcomp
Require Import ssreflect ssrnat ssrbool eqtype seq.
......@@ -14,10 +13,9 @@ Variable T : eqType.
(* A basicTask holds and id, a cost, a period and a deadline *)
Record basicTask := {
basicTask_id_cost_period_deadline : T * time * time * time;
basicTask_id_cost_period_deadline : T * n0nat * n0nat * n0nat;
_ : let: (_, cost, period, deadline) := basicTask_id_cost_period_deadline in
[&& cost > 0, period > 0, deadline > 0,
cost <= deadline & cost <= period]
(cost <= deadline) && (cost <= period)
}.
(* We have an eqType on basicTasks *)
......@@ -28,53 +26,41 @@ Canonical basicTask_eqType := Eval hnf in EqType basicTask basicTask_eqMixin.
(* constructor *)
Program Definition BasicTask
(id : T)
(cost : time)
(period : time)
(deadline : time)
(cost_positive : cost > 0)
(period_positive : period > 0)
(deadline_positive : deadline > 0)
(cost : n0nat)
(period : n0nat)
(deadline : n0nat)
(cost_le_deadline : cost <= deadline)
(cost_le_period : cost <= period) :=
@Build_basicTask (id, cost, period, deadline) _.
Next Obligation.
rewrite cost_positive period_positive deadline_positive.
by rewrite cost_le_deadline cost_le_period.
Qed.
Next Obligation. by rewrite cost_le_deadline cost_le_period. Qed.
(* destructors *)
Coercion task_id (t : basicTask) : T :=
let: (id, _, _, _) := basicTask_id_cost_period_deadline t in id.
Definition task_cost (t : basicTask) : time :=
Definition task_cost (t : basicTask) : n0nat :=
let: (_, c, _, _) := basicTask_id_cost_period_deadline t in c.
Definition task_period (t : basicTask) : time :=
Definition task_period (t : basicTask) : n0nat :=
let: (_, _, p, _) := basicTask_id_cost_period_deadline t in p.
Definition task_deadline (t : basicTask) : time :=
Definition task_deadline (t : basicTask) : n0nat :=
let: (_, _, _, d) := basicTask_id_cost_period_deadline t in d.
Lemma task_cost_positive (t : basicTask) : task_cost t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /=.
by move=> /and5P [].
Qed.
Lemma task_period_positive (t : basicTask) : task_period t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_period /=.
by move=> /and5P [].
Qed.
Lemma task_deadline_positive (t : basicTask) : task_deadline t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_deadline /=.
by move=> /and5P [].
Qed.
Lemma task_cost_le_deadline (t : basicTask) : task_cost t <= task_deadline t.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /task_deadline /=.
by move=> /and5P [].
by move=> /andP [].
Qed.
Lemma task_cost_le_period (t : basicTask) : task_cost t <= task_period t.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /task_period /=.
by move=> /and5P [].
by move=> /andP [].
Qed.
Lemma task_cost_positive (t : basicTask) : task_cost t > 0.
rewrite /task_cost /=; case t => [[[[? ?] ?] ?] _] /=; apply n0nat_pos.
Qed.
Lemma task_period_positive (t : basicTask) : task_period t > 0.
rewrite /task_period /=; case t => [[[[? ?] ?] ?] _] /=; apply n0nat_pos.
Qed.
Lemma task_deadline_positive (t : basicTask) : task_deadline t > 0.
rewrite /task_deadline /=; case t => [[[[? ?] ?] ?] _] /=; apply n0nat_pos.
Qed.
(* A task set is defined as a sequence of tasks with no duplicates. *)
......
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