Require Export prosa.model.priority.classes.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(** * FIFO Priority Policy *)

(** We define the basic FIFO priority policy, under which jobs are prioritized
    in order of their arrival times. The FIFO policy belongs to the class of
    JLFP policies. *)
Instance FIFO (Job : JobType) `{JobArrival Job} : JLFP_policy Job :=
{
  hep_job (j1 j2 : Job) := job_arrival j1 <= job_arrival j2
}.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

(** In this section, we prove a few basic properties of the FIFO policy. *)
Section Properties.

  (**  Consider any type of jobs with arrival times. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.

  (** FIFO is reflexive. *)
  Lemma FIFO_is_reflexive : reflexive_priorities.
Job: JobType
H: JobArrival Job
reflexive_priorities
  Proof.
Job: JobType
H: JobArrival Job
reflexive_priorities  by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO. Qed.

  (** FIFO is transitive. *)
  Lemma FIFO_is_transitive : transitive_priorities.
Job: JobType
H: JobArrival Job
transitive_priorities
  Proof.
Job: JobType
H: JobArrival Job
transitive_priorities by intros t y x z; apply leq_trans. Qed.

  (** FIFO is total. *)
  Lemma FIFO_is_total : total_priorities.
Job: JobType
H: JobArrival Job
total_priorities
  Proof.
Job: JobType
H: JobArrival Job
total_priorities by move=> t j1 j2; apply leq_total. Qed.

End Properties.

(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
    will be able to apply them automatically. *)
Global Hint Resolve
     FIFO_is_reflexive
     FIFO_is_transitive
     FIFO_is_total
  : basic_facts.