Commit 393d2007 authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: move preemption-time notion to model.schedule

parent 4a80f261
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.preemption_time.
Require Import rt.restructuring.model.schedule.preemption_time.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.model.preemption.preemption_time.
Require Export rt.restructuring.model.schedule.preemption_time.
(** We now define what it means for a schedule to respect a priority
in the presence of jobs with non-preemptive segments. *)
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