Commit 1e4bc527 authored by Maxime Lesourd's avatar Maxime Lesourd Committed by Björn Brandenburg

Moved behavior to restructuring/behavior

parent edaa526b
Require Export rt.behavior.facts.service.
Require Export rt.behavior.facts.completion.
Require Export rt.behavior.facts.ideal_schedule.
Require Export rt.behavior.facts.sequential.
Require Export rt.behavior.facts.arrivals.
From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
From rt.behavior Require Export time job.
From rt.restructuring.behavior Require Export time job.
From rt.util Require Import notation.
(* Definitions and properties of job arrival sequences. *)
......
Require Export rt.restructuring.behavior.facts.service.
Require Export rt.restructuring.behavior.facts.completion.
Require Export rt.restructuring.behavior.facts.ideal_schedule.
Require Export rt.restructuring.behavior.facts.sequential.
Require Export rt.restructuring.behavior.facts.arrivals.
From rt.behavior.arrival Require Export arrival_sequence.
From rt.restructuring.behavior.arrival Require Export arrival_sequence.
From rt.util Require Import all.
(* In this section, we establish useful facts about arrival sequence prefixes. *)
......
From rt.behavior.schedule Require Export schedule.
From rt.behavior.facts Require Export service.
From rt.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior.facts Require Export service.
(** In this file, we establish basic facts about job completions. *)
......
From rt.behavior.schedule Require Import schedule ideal.
From rt.restructuring.behavior.schedule Require Import schedule ideal.
(* Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
......
From rt.behavior Require Export schedule.sequential.
From rt.restructuring.behavior Require Export schedule.sequential.
Section ExecutionOrder.
(* Consider any type of job associated with any type of tasks... *)
......
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.behavior.schedule Require Export schedule.
From rt.restructuring.behavior.schedule Require Export schedule.
From rt.util Require Import tactics step_function sum.
(** In this file, we establish basic facts about the service received by
......
From rt.behavior Require Export schedule.schedule.
From rt.restructuring.behavior Require Export schedule.schedule.
(** First let us define the notion of an ideal schedule state,
* as done in Prosa so far: either a job is scheduled or the system is idle.
......
From mathcomp Require Export fintype.
From rt.behavior.schedule Require Export schedule.
From rt.restructuring.behavior.schedule Require Export schedule.
Section Schedule.
......
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.behavior Require Export arrival.arrival_sequence.
From rt.restructuring.behavior Require Export arrival.arrival_sequence.
(* We define the notion of a generic processor state. The processor state type
* determines aspects of the execution environment are modeled (e.g., overheads, spinning).
......
From rt.behavior Require Export schedule task.
From rt.restructuring.behavior Require Export schedule task.
Section PropertyOfSequentiality.
(* Consider any type of job associated with any type of tasks... *)
......
From rt.behavior.schedule Require Export schedule.
From rt.restructuring.behavior.schedule Require Export schedule.
(** Next we define a processor state that includes the possibility of spinning,
* where spinning jobs do not progress (= don't get service). *)
......
From rt.behavior.schedule Require Export schedule.
From rt.restructuring.behavior.schedule Require Export schedule.
(** Next, let us define a schedule with variable execution speed. *)
Section State.
......
From mathcomp Require Export ssrbool.
From rt.behavior Require Export job.
From rt.restructuring.behavior Require Export job.
(* Throughout the library we assume that jobs have decidable equality *)
......
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