Commit d1b319e6 authored by Björn Brandenburg's avatar Björn Brandenburg

merge analysis.concepts and analysis.definitions

In anticipation of future reorganization efforts by Sophie, there's no
point in keeping the two kinds of definitions separate.
parent 57c1ba7a
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.run_to_completion.
......
Require Export prosa.analysis.concepts.priority_inversion.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.abstract.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export prosa.analysis.concepts.busy_interval.
Require Export prosa.analysis.definitions.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.concepts.priority_inversion.
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.
......
......@@ -3,7 +3,7 @@ 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.concepts.busy_interval.
Require Export prosa.analysis.definitions.busy_interval.
Require Export prosa.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export prosa.analysis.facts.behavior.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.concepts.request_bound_function.
Require Export prosa.analysis.definitions.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export prosa.model.schedule.edf.
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.transform.edf_trans.
Require Export prosa.analysis.facts.transform.swaps.
Require Export prosa.analysis.facts.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Export prosa.analysis.facts.edf.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.priority_inversion.
Require Export prosa.analysis.facts.carry_in.
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.definitions.schedulability.
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
Require Import prosa.analysis.abstract.ideal_jlfp_rta.
......
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.concepts.request_bound_function.
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.priority_inversion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
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