# Library prosa.analysis.definitions.service

Consider any kind of jobs and any kind of processor state.

Consider any arrival sequence ...

... and any schedule.

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].

[seq j <- arrivals_up_to arr_seq t | receives_service_at sched j t].