Commit 2e9c8416 authored by Björn Brandenburg's avatar Björn Brandenburg

remove remaining unneeded Require statements in model/

parent f1ff74c2
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.model.task.
(** Given task deadlines and a mapping from jobs to tasks
......
Require Export rt.util.nondecreasing.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.task.instance.floating.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
(** Definition of a parameter relating a job
to the sequence of its preemption points. *)
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.job.parameters.
(** * Platform for Fully Non-Preemptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.job.parameters.
(** * Platform for Fully Premptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
(** * Job Preemptable *)
(** There are many equivalent ways to represent preemption points of a job. *)
......
Require Export rt.util.nondecreasing.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.task.instance.limited.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
Require Export rt.util.nondecreasing.
Require Export rt.restructuring.model.schedule.nonpreemptive.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.preemption.task.instance.nonpreemptive.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.preemption.valid_model.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Preemption Time in Ideal Uni-Processor Model *)
......
Require Export rt.util.nondecreasing.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.preemption.task.instance.preemptive.
......
Require Export rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.job.
Require Import rt.restructuring.behavior.schedule.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
......
Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.valid_model.
(** * Task's Run-to-Completion Threshold *)
(** Since a task model may not provide exact information about
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.job.instance.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.job.instance.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.valid_model.
(** * Platform for Fully Preemptive Model *)
(** In this section, we instantiate function
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.task.
Require Export rt.util.all.
Require Export rt.restructuring.model.task.
(** * Static information about preemption points *)
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.task.parameters.
(** * Platform with limited preemptions *)
(** Since the notion of preemption points is based on an user-provided
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.preemption.job.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.job.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export rt.restructuring.behavior.all.
(** In this section we introduce the notion of a non-preemptive schedule. *)
Section NonpreemptiveSchedule.
......
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