Commit 5fc2e7dd authored by Sergey Bozhko's avatar Sergey Bozhko

Restructure facts.model

parent 3b9b6f20
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.rbf.
Require Export prosa.analysis.facts.task_arrivals.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.abstract.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Abstract Response-Time Analysis with sequential tasks *)
(** In this section we propose the general framework for response-time analysis (RTA)
......
Require Export prosa.analysis.facts.service_of_jobs.
Require Export prosa.analysis.facts.model.service_of_jobs.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.abstract.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Run-to-Completion Threshold of a job *)
(** In this module, we provide a sufficient condition under which a job
receives enough service to become non-preemptive. *)
......
......@@ -2,7 +2,7 @@ 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.
Require Export prosa.analysis.facts.service_of_jobs.
Require Export prosa.analysis.facts.model.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.facts.model.workload.
Require Export prosa.analysis.definitions.carry_in.
Require Export prosa.analysis.facts.busy_interval.busy_interval.
......
Require Export prosa.analysis.facts.workload.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Facts about Request Bound Functions (RBFs) *)
(** In this file, we prove some lemmas about request bound functions. *)
......
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.sequential.
Require Export prosa.analysis.facts.model.ideal_schedule.
(** *)
Require Import prosa.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
......
Require Import prosa.model.priority.edf.
Require Export prosa.analysis.facts.rbf.
Require Export prosa.analysis.facts.sequential.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.results.edf.rta.bounded_pi.
(** 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.analysis.facts.sequential.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
......
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