arrival_sequence.v 3.98 KB
Newer Older
1 2
From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
From rt.behavior Require Export time job.
3
From rt.util Require Import notation.
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41

(* Definitions and properties of job arrival sequences. *)

(* We begin by defining a job arrival sequence. *)
Section ArrivalSequenceDef.

  (* Given any job type with decidable equality, ... *)
  Variable Job: JobType.

  (* ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
  Definition arrival_sequence := instant -> seq Job.

End ArrivalSequenceDef.

(* Next, we define properties of jobs in a given arrival sequence. *)
Section JobProperties.

  (* Consider any job arrival sequence. *)
  Context {Job: JobType}.
  Variable arr_seq: arrival_sequence Job.

  (* First, we define the sequence of jobs arriving at time t. *)
  Definition jobs_arriving_at (t : instant) := arr_seq t.

  (* Next, we say that job j arrives at a given time t iff it belongs to the
       corresponding sequence. *)
  Definition arrives_at (j : Job) (t : instant) := j \in jobs_arriving_at t.

  (* Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
       whether it belongs to the arrival sequence. *)
  Definition arrives_in (j : Job) := exists t, j \in jobs_arriving_at t.

End JobProperties.

(* Definition of a generic type of parameter for job_arrival *)

Class JobArrival (J : JobType) := job_arrival : J -> instant.

42 43
(* Next, we define valid arrival sequences. *)
Section ValidArrivalSequence.
44 45 46 47 48 49 50 51

  (* Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (* Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

52 53
  (* We say that arrival times are consistent if any job that arrives in the
     sequence has the corresponding arrival time. *)
54 55 56 57
  Definition arrival_times_are_consistent :=
    forall j t,
      arrives_at arr_seq j t -> job_arrival j = t.

58 59
  (* We say that the arrival sequence is a set iff it doesn't contain duplicate
     jobs at any given time. *)
60 61
  Definition arrival_sequence_is_a_set := forall t, uniq (jobs_arriving_at arr_seq t).

62 63 64 65 66 67
  (* We say that the arrival sequence is valid iff it is a set and arrival times
     are consistent *)
  Definition arrival_sequence_is_valid :=
    arrival_times_are_consistent /\ arrival_sequence_is_a_set.

End ValidArrivalSequence.
68 69

(* Next, we define properties of job arrival times. *)
70
Section ArrivalTimeProperties.
71 72 73 74 75 76 77 78

  (* Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (* Let j be any job. *)
  Variable j: Job.

79 80
  (* We say that job j has arrived at time t iff it arrives at some time t_0
     with t_0 <= t. *)
81 82
  Definition has_arrived (t : instant) := job_arrival j <= t.

83 84
  (* Next, we say that job j arrived before t iff it arrives at some time t_0
     with t_0 < t. *)
85 86
  Definition arrived_before (t : instant) := job_arrival j < t.

87 88
  (* Finally, we say that job j arrives between t1 and t2 iff it arrives at
     some time t with t1 <= t < t2. *)
89 90
  Definition arrived_between (t1 t2 : instant) := t1 <= job_arrival j < t2.

91
End ArrivalTimeProperties.
92

93 94
(* In this section, we define arrival sequence prefixes, which are useful to
   define (computable) properties over sets of jobs in the schedule. *)
95 96 97 98 99 100 101 102 103
Section ArrivalSequencePrefix.

  (* Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (* Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

104 105
  (* By concatenation, we construct the list of jobs that arrived in the
     interval [t1, t2). *)
106 107 108 109 110 111 112 113 114 115
  Definition jobs_arrived_between (t1 t2 : instant) :=
    \cat_(t1 <= t < t2) jobs_arriving_at arr_seq t.

  (* Based on that, we define the list of jobs that arrived up to time t, ...*)
  Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.

  (* ...and the list of jobs that arrived strictly before time t. *)
  Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.

End ArrivalSequencePrefix.