Commit 12b573c3 authored by Björn Brandenburg's avatar Björn Brandenburg

remove task dependency in job limited-preemptive preemption model

Job-level definitions should not depend on task-related modules.
parent 1306c75c
Require Export rt.restructuring.model.preemption.parameter. Require Export rt.restructuring.model.preemption.parameter.
Require Export rt.restructuring.model.task.preemption.parameters.
(** Definition of a parameter relating a job (** Definition of a parameter relating a job
to the sequence of its preemption points. *) to the sequence of its preemption points. *)
......
Require Export rt.restructuring.model.preemption.limited_preemptive. Require Export rt.restructuring.model.preemption.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop. From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.preemption.limited_preemptive. Require Export rt.restructuring.model.preemption.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop. From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq 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