# Library prosa.analysis.definitions.service

Require Export prosa.behavior.service.

# Service Definitions

In this section, we define a set of jobs that receive service at a given time.
Section ServedAt.
Consider any kind of jobs and any kind of processor state.
Context {Job : JobType} {PState : ProcessorState Job}.
Consider any arrival sequence ...
Variable arr_seq : arrival_sequence Job.
... and any schedule.
Variable sched : schedule PState.
The set of jobs served at time t can be obtained by filtering the set of all jobs that arrive at or before time t.
Definition served_jobs_at (t : instant) :=
[seq j <- arrivals_up_to arr_seq t | receives_service_at sched j t].
For the special case of uniprocessors, we define a convenience wrapper that reduces the sequence of scheduled jobs to an option Job.
Definition served_job_at t := ohead (served_jobs_at t).
End ServedAt.