Commit 03863f8f authored by Maxime Lesourd's avatar Maxime Lesourd

simplify structure of behavior, move arrival_sequence and schedule to...

simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model
parent 37121eb7
......@@ -35,10 +35,6 @@ Section JobProperties.
End JobProperties.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J -> instant.
(* Next, we define valid arrival sequences. *)
Section ValidArrivalSequence.
......
From rt.restructuring.behavior.arrival Require Export arrival_sequence.
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.util Require Import all.
(* In this section, we establish useful facts about arrival sequence prefixes. *)
......
From rt.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.behavior.facts Require Export service.
(** In this file, we establish basic facts about job completions. *)
......
From rt.restructuring.behavior.schedule Require Import schedule ideal.
From rt.restructuring.behavior.schedule Require Import ideal.
(* Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
......
From rt.restructuring.behavior Require Export schedule.sequential.
From rt.restructuring.model 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.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import tactics step_function sum.
(** In this file, we establish basic facts about the service received by
......@@ -581,4 +581,3 @@ Section RelationToScheduled.
End TimesWithSameService.
End RelationToScheduled.
From rt.restructuring.behavior Require Export time.
From mathcomp Require Export eqtype.
(* Throughout the library we assume that jobs have decidable equality *)
......@@ -7,3 +8,7 @@ Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J -> nat.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J -> instant.
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export arrival.arrival_sequence.
From rt.restructuring.behavior Require Export 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.restructuring.behavior Require Export schedule.schedule.
From rt.restructuring.behavior Require Export 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. *)
......@@ -18,5 +18,3 @@ Section State.
by move=> j [j'->|].
Defined.
End State.
From mathcomp Require Export fintype.
From rt.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior Require Export schedule.
Section Schedule.
......
From rt.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior 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.restructuring.behavior.schedule Require Export schedule.
From rt.restructuring.behavior Require Export schedule.
(** Next, let us define a schedule with variable execution speed. *)
Section State.
......
From rt.restructuring.behavior Require Export arrival.arrival_sequence task.
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
Section TaskMinInterArrivalTime.
Context {T : TaskType}.
......
From rt.restructuring.behavior Require Export schedule task.
From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.model Require Export task.
Section PropertyOfSequentiality.
(* Consider any type of job associated with any type of tasks... *)
......
From rt.restructuring.behavior Require Import task schedule.ideal.
From rt.restructuring.behavior Require Export schedule.ideal.
From rt.restructuring.model Require Export task.
From rt.util Require Export seqset list.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
......
From rt.restructuring.behavior Require Export task arrival.arrival_sequence.
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
Section TaskCost.
Context {T : TaskType}.
......
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