From 18d6d851a7b061faa650f11f37b2e976fbbdde83 Mon Sep 17 00:00:00 2001
From: Maxime Lesourd <maxime.lesourd@inria.fr>
Date: Tue, 15 Oct 2019 16:29:08 +0200
Subject: [PATCH] Change definition of service_implies_scheduled
---
restructuring/analysis/basic_facts/service.v | 4 +---
restructuring/behavior/schedule.v | 7 +++----
restructuring/model/processor/ideal.v | 2 +-
restructuring/model/processor/spin.v | 3 ++-
restructuring/model/processor/varspeed.v | 4 ++--
5 files changed, 9 insertions(+), 11 deletions(-)
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 44539d945..9c01810c7 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -250,7 +250,6 @@ Section RelationToScheduled.
rewrite /service_at /scheduled_at.
move=> t NOT_SCHED.
rewrite service_implies_scheduled //.
- by apply: negbTE.
Qed.
(* Conversely, if a job receives service, then it must be scheduled. *)
@@ -354,8 +353,7 @@ Section RelationToScheduled.
Proof.
move=> t. rewrite /scheduled_at /service_at.
split => [NOT_SCHED | NO_SERVICE].
- - apply negbTE in NOT_SCHED.
- by rewrite service_implies_scheduled //.
+ - by rewrite service_implies_scheduled //.
- apply (contra (H_scheduled_implies_serviced j (sched t))).
by rewrite -eqn0Ngt; apply /eqP => //.
Qed.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index d52e29116..a80b3b697 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -9,16 +9,15 @@ Class ProcessorState (Job : JobType) (State : Type) :=
{
(* For a given processor state, the [scheduled_in] predicate checks whether a given
job is running in that state. *)
- scheduled_in: Job -> State -> bool;
+ scheduled_in : Job -> State -> bool;
(* For a given processor state, the [service_in] function determines how much
service a given job receives in that state. *)
- service_in: Job -> State -> work;
+ service_in : Job -> State -> work;
(* For a given processor state, a job does not receive service if it is not scheduled
in that state *)
service_implies_scheduled :
- forall j s, scheduled_in j s = false -> service_in j s = 0
+ forall j s, ~~ scheduled_in j s -> service_in j s = 0
}.
(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant -> PState.
-
diff --git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index ca65de81f..e692211e0 100644
--- a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ -15,6 +15,6 @@ Section State.
service_in j s := s == Some j;
}.
Next Obligation.
- by rewrite H.
+ by move: H=> /negbTE->.
Defined.
End State.
diff --git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index 44826d232..931dc457f 100644
--- a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ -37,6 +37,7 @@ Section State.
service_in := service_in
}.
Next Obligation.
- by move: H; case s => //= j' ->.
+ move: H.
+ by case: s=>//= j' /negbTE->.
Defined.
End State.
diff --git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index 2708b1490..a0dccb4b7 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ -34,7 +34,7 @@ Section State.
}.
Next Obligation.
move: j s H.
- by move=> j []//= j' s->.
+ by move=> j []//= j' s/negbTE->.
Defined.
-
+
End State.
--
GitLab