Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.model.task.arrival.sporadic. (** * Rate-Monotonic Fixed-Priority Policy *) (** We define the notion of rate-monotonic task priorities for sporadic tasks, i.e., the classic FP policy in which sporadic tasks are prioritized in order of their minimum inter-arrival times (or periods). *) #[export] Instance RM (Task : TaskType) `{SporadicModel Task} : FP_policy Task := { hep_task (tsk1 tsk2 : Task) := task_min_inter_arrival_time tsk1 <= task_min_inter_arrival_time tsk2 }. (** In this section, we prove a few basic properties of the RM policy. *) Section Properties. (** Consider sporadic tasks... *) Context {Task : TaskType}. Context `{SporadicModel Task}. (** ...and jobs stemming from these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. (** RM is reflexive. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

reflexive_task_priorities (RM Task)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

reflexive_task_priorities (RM Task)
by move=> ?; rewrite /hep_task /RM. Qed. (** RM is transitive. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

transitive_task_priorities (RM Task)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

transitive_task_priorities (RM Task)
by move=> ? ? ?; apply: leq_trans. Qed. (** RM is total. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

total_task_priorities (RM Task)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task

total_task_priorities (RM Task)
by move=> ? ?; apply: leq_total. Qed. End Properties. (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve RM_is_reflexive RM_is_transitive RM_is_total : basic_rt_facts.