# Library prosa.behavior.arrival_sequence

From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.

Require Export prosa.behavior.job.

Require Export prosa.util.notation.

Require Export prosa.behavior.job.

Require Export prosa.util.notation.

This module contains basic definitions and properties of job arrival
sequences.
We begin by defining a job arrival sequence.

# Notion of an Arrival Sequence

Given any job type with decidable equality, ...

..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs.

Consider any job arrival sequence.

First, we define the sequence of jobs arriving at time t.

Next, we say that job j arrives at a given time t iff it belongs to the
corresponding sequence.

Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
whether it belongs to the arrival sequence.

Assume that job arrival times are known.

Consider any job arrival sequence.

We say that arrival times are consistent if any job that arrives in the
sequence has the corresponding arrival time.

We say that the arrival sequence is a set iff it doesn't contain duplicate
jobs at any given time.

We say that the arrival sequence is valid iff it is a set and arrival times
are consistent

Definition valid_arrival_sequence :=

consistent_arrival_times ∧ arrival_sequence_uniq.

End ValidArrivalSequence.

consistent_arrival_times ∧ arrival_sequence_uniq.

End ValidArrivalSequence.

Assume that job arrival times are known.

Let j be any job.

We say that job j has arrived at time t iff it arrives at some time t_0
with t_0 <= t.

Next, we say that job j arrived before t iff it arrives at some time t_0
with t_0 < t.

Finally, we say that job j arrives between t1 and t2 iff it arrives at
some time t with t1 <= t < t2.

# Finite Arrival Sequence Prefixes

Assume that job arrival times are known.

Consider any job arrival sequence.

By concatenation, we construct the list of jobs that arrived in the
interval

`[t1, t2)`

.
Based on that, we define the list of jobs that arrived up to time t, ...

... the list of jobs that arrived strictly before time t, ...

... and the list of jobs that arrive in the interval

`[t1, t2)`

and
satisfy a certain predicate P.
Definition arrivals_between_P (P : Job → bool) (t1 t2 : instant) :=

[seq j <- arrivals_between t1 t2 | P j].

End ArrivalSequencePrefix.

[seq j <- arrivals_between t1 t2 | P j].

End ArrivalSequencePrefix.