Commit e56ad10b authored by Sergey Bozhko's avatar Sergey Bozhko

Restructure facts.behavior

parent e27bc9ac
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.rbf.
Require Export prosa.analysis.facts.behavior.task_arrivals.
Require Export prosa.analysis.facts.task_arrivals.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.abstract.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export prosa.analysis.facts.service_of_jobs.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.abstract.definitions.
......
Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import prosa.model.processor.ideal.
......
Require Export prosa.model.task.arrival.curves.
Require Export prosa.model.priority.classes.
(** The following definitions assume ideal uni-processor schedules. This
restriction exists for historic reasons; the defined concepts could be
generalized in future work. *)
Require Import prosa.analysis.facts.behavior.ideal_schedule.
(** The following definitions assume ideal uni-processor schedules.
This restriction exists for historic reasons; the defined concepts
could be generalized in future work. *)
Require Import prosa.analysis.facts.model.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export prosa.model.task.concept.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export prosa.model.processor.ideal.
(** Due to historical reasons this file defines the notion of a schedule of
a task for the ideal uni-processor model. This is not a fundamental limitation
......
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.analysis.facts.behavior.sequential.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.facts.behavior.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export prosa.analysis.facts.service_of_jobs.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
......
Require Export prosa.analysis.facts.workload.
Require Export prosa.analysis.definitions.carry_in.
Require Export prosa.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.limited_preemptive.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Import prosa.model.preemption.limited_preemptive.
......
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.
Require Import prosa.model.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Preemptive model *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully non-preemptive model indeed
......
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.busy_interval.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
......
Require Export prosa.analysis.facts.behavior.workload.
Require Export prosa.analysis.facts.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
......
Require Export prosa.model.aggregate.workload.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Import prosa.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export prosa.analysis.transform.prefix.
Require Export prosa.analysis.transform.swap.
Require Export prosa.analysis.facts.model.ideal_schedule.
(** In this file we define the EDF transformation of a schedule, which turns a
(finite prefix of a) schedule into an EDF schedule. This operation is at
......
Require Import prosa.model.priority.edf.
Require Export prosa.analysis.facts.rbf.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.facts.priority_inversion.
Require Export prosa.results.edf.rta.bounded_pi.
Require Export prosa.analysis.facts.rbf.
Require Import prosa.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
......
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.facts.priority_inversion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
......
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