From 45853287740a6465d9509abd52dbe3ce6d992457 Mon Sep 17 00:00:00 2001
From: Maxime Lesourd <maxime.lesourd@inria.fr>
Date: Tue, 4 Jun 2019 16:29:35 +0200
Subject: [PATCH] applied naming convention to behavior
---
restructuring/behavior/arrival/arrival_sequence.v | 8 ++++----
restructuring/behavior/facts/arrivals.v | 14 +++++++-------
restructuring/behavior/schedule/schedule.v | 2 +-
3 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/restructuring/behavior/arrival/arrival_sequence.v b/restructuring/behavior/arrival/arrival_sequence.v
index 2f1252753..ab0fedfc0 100644
--- a/restructuring/behavior/arrival/arrival_sequence.v
+++ b/restructuring/behavior/arrival/arrival_sequence.v
@@ -51,18 +51,18 @@ Section ValidArrivalSequence.
(* We say that arrival times are consistent if any job that arrives in the
sequence has the corresponding arrival time. *)
- Definition arrival_times_are_consistent :=
+ Definition consistent_arrival_times :=
forall j t,
arrives_at arr_seq j t -> job_arrival j = t.
(* We say that the arrival sequence is a set iff it doesn't contain duplicate
jobs at any given time. *)
- Definition arrival_sequence_is_a_set := forall t, uniq (jobs_arriving_at arr_seq t).
+ Definition arrival_sequence_uniq := forall t, uniq (jobs_arriving_at arr_seq t).
(* We say that the arrival sequence is valid iff it is a set and arrival times
are consistent *)
- Definition arrival_sequence_is_valid :=
- arrival_times_are_consistent /\ arrival_sequence_is_a_set.
+ Definition valid_arrival_sequence :=
+ consistent_arrival_times /\ arrival_sequence_uniq.
End ValidArrivalSequence.
diff --git a/restructuring/behavior/facts/arrivals.v b/restructuring/behavior/facts/arrivals.v
index 250e6709d..ee6edac4b 100644
--- a/restructuring/behavior/facts/arrivals.v
+++ b/restructuring/behavior/facts/arrivals.v
@@ -78,8 +78,8 @@ Section ArrivalSequencePrefix.
Section ArrivalTimes.
(* Assume that job arrival times are consistent. *)
- Hypothesis H_arrival_times_are_consistent:
- arrival_times_are_consistent arr_seq.
+ Hypothesis H_consistent_arrival_times:
+ consistent_arrival_times arr_seq.
(* First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
@@ -88,7 +88,7 @@ Section ArrivalSequencePrefix.
j \in jobs_arrived_between t1 t2 ->
arrives_in arr_seq j.
Proof.
- rename H_arrival_times_are_consistent into CONS.
+ rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [arr [IN _]].
@@ -103,7 +103,7 @@ Section ArrivalSequencePrefix.
j \in jobs_arrived_between t1 t2 ->
arrived_between j t1 t2.
Proof.
- rename H_arrival_times_are_consistent into CONS.
+ rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [t0 [IN /= LT]].
@@ -131,7 +131,7 @@ Section ArrivalSequencePrefix.
arrived_between j t1 t2 ->
j \in jobs_arrived_between t1 t2.
Proof.
- rename H_arrival_times_are_consistent into CONS.
+ rename H_consistent_arrival_times into CONS.
move => j t1 t2 [a_j ARRj] BEFORE.
have SAME := ARRj; apply CONS in SAME; subst a_j.
by apply mem_bigcat_nat with (j := (job_arrival j)).
@@ -140,10 +140,10 @@ Section ArrivalSequencePrefix.
(* Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
- arrival_sequence_is_a_set arr_seq ->
+ arrival_sequence_uniq arr_seq ->
forall t1 t2, uniq (jobs_arrived_between t1 t2).
Proof.
- rename H_arrival_times_are_consistent into CONS.
+ rename H_consistent_arrival_times into CONS.
unfold jobs_arrived_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
diff --git a/restructuring/behavior/schedule/schedule.v b/restructuring/behavior/schedule/schedule.v
index 804e0cf83..7e501f338 100644
--- a/restructuring/behavior/schedule/schedule.v
+++ b/restructuring/behavior/schedule/schedule.v
@@ -85,7 +85,7 @@ Section Schedule.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job can only be scheduled if it has arrived and is not completed yet *)
- Definition schedule_is_valid (arr_seq : arrival_sequence Job) :=
+ Definition valid_schedule (arr_seq : arrival_sequence Job) :=
jobs_come_from_arrival_sequence arr_seq /\
jobs_must_arrive_to_execute /\
completed_jobs_dont_execute.
--
GitLab