Commit 55dab03e authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add Makefile

parent 551ccd02
MODULES := job priority schedule identmp apa helper liulayland
VS := $(MODULES:%=%.v)
.PHONY: coq clean
coq: Makefile.coq
$(MAKE) -f Makefile.coq
Makefile.coq: Makefile $(VS)
coq_makefile -R . Sched $(VS) -o Makefile.coq
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -f Makefile.coq
(* Restrictions on task parameters *)
Record valid_task (tsk: task) : Prop :=
{ job_cost_positive: job_cost tsk > 0;
job_cost_le_deadline: job_cost tsk <= job_deadline tsk;
job_deadline_positive: job_deadline tsk > 0
}.
(* A sporadic task has an interarrival time *)
Record sporadic_task : Type :=
{ sporadic_task_is_task :> task;
task_period : nat
}.
(* Restrictions on sporadic task parameters *)
Record valid_sporadic_task (tsk: sporadic_task) : Prop :=
{ sporadic_task_valid: valid_task tsk;
job_interarrival:
forall t1 t2, (t1 <> t2
/\ job_arrival tsk t1
/\ job_arrival tsk t2)
-> t1 <= t2 + task_period tsk
}.
Definition job_interarrival_fixed (tsk: sporadic_task) := forall t1 t2,
(t1 <> t2
/\ job_arrival tsk t1
/\ job_arrival tsk t2)
-> t1 <= t2 + task_period tsk.
Definition periodic_task := {tsk: sporadic_task | valid_sporadic_task tsk
/\ job_interarrival_fixed tsk }.
\ No newline at end of file
Add LoadPath "/home/felipec/dev/coq/rt-scheduling-spec".
Require Import job.
Require Import schedule.
Definition uniprocessor (s: schedule) := ident_mp 1 s.
Section LiuLayland.
Variable tau : list periodic_task.
Variable s : schedule.
Axiom uniprocessor_schedule : uniprocessor s.
End LiuLayland.
Define critical_instant()
Section RM.
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