From mathcomp Require Export ssrbool.
Require Export prosa.behavior.all.

As in case of the job model, we make no assumptions about the structure or type of tasks, i.e., like jobs, we consider tasks to be mathematically opaque objects. We only assume that any type that represents tasks has a decidable equality.

First, we define a job-model parameter job_task that maps each job to its corresponding task.
Third, we define a task-model parameter to express each task's worst-case execution cost (WCET).
And finally, we define a task-model parameter to express each task's best-case execution cost (BCET).

In the following section, we introduce properties that a reasonable task model must satisfy.
Section ModelValidity.

First, we constrain the possible WCET values of a valid task.
Section ValidCost.

The WCET of the task should be positive.

The WCET should not be larger than the deadline, as otherwise the task is trivially infeasible.
Second, we relate the cost of a task's jobs to its WCET.
Section ValidJobCost.

Consider any type of jobs associated with the tasks ...
Context {Job : JobType}.
... and consider the cost of each job.
Context `{JobCost Job}.

The cost of any job j cannot exceed the WCET of its respective task.
Definition valid_job_cost j :=

Every job have a valid job cost
Definition jobs_have_valid_job_costs :=
j, valid_job_cost j.

Next, consider any arrival sequence.
Variable arr_seq : arrival_sequence Job.

The cost of a job from the arrival sequence cannot be larger than the task cost.
Definition arrivals_have_valid_job_costs :=
j,
arrives_in arr_seq j
valid_job_cost j.

End ValidJobCost.

Third, we relate the cost of a task's jobs to its BCET.
Section ValidMinJobCost.

Consider any type of jobs associated with the tasks ...
Context {Job : JobType}.
... and consider the cost of each job.
Context `{JobCost Job}.

The cost of any job j cannot be less than the BCET of its respective task.
Definition valid_min_job_cost j :=

Every job have a valid job cost
Definition jobs_have_valid_min_job_costs :=
j, valid_min_job_cost j.

Next, consider any arrival sequence.
Variable arr_seq : arrival_sequence Job.

The cost of a job from the arrival sequence cannot be less than the task cost.

Next, we introduce the notion of a task set and define properties of valid task sets.
For simplicity, we represent sets of such tasks simply as (finite) sequences of tasks.

Consider any type of tasks with WCETs ...

... and any type of jobs associated with these tasks ...
Context {Job : JobType}.
... as well as their individual execution costs.
Context `{JobCost Job}.

Further, consider an arrival sequence of these jobs...
Variable arr_seq : arrival_sequence Job.

...and the set of tasks that generate them.

All jobs in the arrival sequence should come from the task set.
j,
arrives_in arr_seq j

Finally, for readability, we define two ways in which jobs and tasks relate.