Commit 1b7dd375 authored by Björn Brandenburg's avatar Björn Brandenburg

remove unnecessary Require statements in model.task.preemption

parent 0089c2ce
Require Import rt.restructuring.model.preemption.limited_preemptive. Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.parameters. Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Models with Floating Non-Preemptive Regions *) (** * Platform for Models with Floating Non-Preemptive Regions *)
(** In this section, we introduce a set of requirements for function (** In this section, we introduce a set of requirements for function
[task_max_nonpr_segment], so it is coherent with model with [task_max_nonpr_segment], so it is coherent with model with
......
Require Export rt.restructuring.model.task.preemption.parameters. Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Preemptive Model *) (** * Platform for Fully Non-Preemptive Model *)
(** In this section, we instantiate function (** In this section, we instantiate function
[task_max_nonpreemptive_segment] for the fully non-preemptive [task_max_nonpreemptive_segment] for the fully non-preemptive
...@@ -22,9 +20,6 @@ Section FullyNonPreemptiveModel. ...@@ -22,9 +20,6 @@ Section FullyNonPreemptiveModel.
End FullyNonPreemptiveModel. End FullyNonPreemptiveModel.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Task's Run to Completion Threshold *) (** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion (** In this section, we instantiate function [task run to completion
threshold] for the fully non-preemptive model. *) threshold] for the fully non-preemptive model. *)
......
...@@ -17,8 +17,6 @@ Section FullyPreemptiveModel. ...@@ -17,8 +17,6 @@ Section FullyPreemptiveModel.
End FullyPreemptiveModel. End FullyPreemptiveModel.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Task's Run to Completion Threshold *) (** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion (** In this section, we instantiate function [task run to completion
threshold] for the fully preemptive model. *) threshold] for the fully preemptive model. *)
......
Require Export rt.restructuring.model.task.preemption.parameters. Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.limited_preemptive. Require Import rt.restructuring.model.preemption.limited_preemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Models with Limited Preemptions *) (** * Platform for Models with Limited Preemptions *)
(** In this section, we introduce a set of requirements for function (** In this section, we introduce a set of requirements for function
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment