Library prosa.behavior.completion_sequence
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
Require Import prosa.behavior.service.
This module contains basic definitions and properties of job
completion sequences.
We begin by defining a job completion sequence.
Notion of a Completion Sequence
Consider any kind of jobs with a cost
and any kind of processor state.
Consider any job arrival sequence.
Consider any schedule.
For each instant [t], the completion sequence returns all
arrived jobs that have completed at [t].
Definition completion_sequence : arrival_sequence Job :=
fun t ⇒ [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
End CompletionSequence.
fun t ⇒ [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
End CompletionSequence.