Commit 9632d3ed authored by Björn Brandenburg's avatar Björn Brandenburg

move processor models and properties into model/ directory

parent 8313f7c6
...@@ -12,7 +12,7 @@ From rt.util Require Import tactics nat. ...@@ -12,7 +12,7 @@ From rt.util Require Import tactics nat.
schedule. *) schedule. *)
(* Throughout this file, we assume ideal uniprocessor schedules. *) (* Throughout this file, we assume ideal uniprocessor schedules. *)
From rt.restructuring.behavior Require Export schedule.ideal. From rt.restructuring.model.processor Require Export ideal.
(* Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *) (* Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
From rt.restructuring.model.readiness Require Export basic. From rt.restructuring.model.readiness Require Export basic.
......
From rt.restructuring.behavior.schedule Require Import ideal platform_properties. From rt.restructuring.model.processor Require Import ideal platform_properties.
(* Note: we do not re-export the basic definitions to avoid littering the global (* Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *) namespace with type class instances. *)
......
From mathcomp Require Import ssrnat ssrbool fintype. From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.behavior Require Export schedule schedule.platform_properties. From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.model.processor Require Export platform_properties.
From rt.util Require Import tactics step_function sum. From rt.util Require Import tactics step_function sum.
(** In this file, we establish basic facts about the service received by (** In this file, we establish basic facts about the service received by
......
From rt.restructuring.behavior Require Export schedule.ideal. From rt.restructuring.model Require Export task processor.ideal.
From rt.restructuring.model Require Export task.
From rt.util Require Export seqset list. From rt.util Require Export seqset list.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div. From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
......
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