Library rt.restructuring.model.preemption.task.instance.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Export all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Export
valid_model job.parameters task.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform for Fully Non-Preemptive Model
In this section, we instantiate function [task_max_nonpreemptive_segment] for the fully non-preemptive model.
Consider any type of jobs.
In fully non-preemptive model no job can be preempted until its
completion. The maximal non-preemptive segment of a job
[j] has length [job_cost j] which is bounded by [task_cost tsk].
Global Program Instance fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.
End FullyNonPreemptiveModel.
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.
End FullyNonPreemptiveModel.