Library rt.restructuring.model.processor.varspeed
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
From rt.restructuring.behavior Require Export all.
Next, let us define a schedule with variable execution speed.
Section State.
Variable Job: JobType.
Inductive processor_state :=
Idle
| Progress (j : Job) (speed : nat).
Section Service.
Variable j : Job.
Definition scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
| Idle ⇒ false
| Progress j' _ ⇒ j' == j
end.
Definition service_in (s : processor_state) : nat :=
match s with
| Idle ⇒ 0
| Progress j' speed ⇒ if j' == j then speed else 0
end.
End Service.
Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
scheduled_on := scheduled_on;
service_in := service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
j : Job
s : processor_state
H : ~~ [exists c, scheduled_on j s c]
============================
service_in j s = 0
----------------------------------------------------------------------------- *)
move: H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Job : JobType
j : Job
s : processor_state
============================
~~ [exists c, scheduled_on j s c] -> service_in j s = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' v /existsP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 373)
Job : JobType
j, j' : Job
v : nat
============================
~ (exists _ : unit_finType, j' == j) -> (if j' == j then v else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP=>//=_[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
Job : JobType
j, j' : Job
v : nat
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
Variable Job: JobType.
Inductive processor_state :=
Idle
| Progress (j : Job) (speed : nat).
Section Service.
Variable j : Job.
Definition scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
| Idle ⇒ false
| Progress j' _ ⇒ j' == j
end.
Definition service_in (s : processor_state) : nat :=
match s with
| Idle ⇒ 0
| Progress j' speed ⇒ if j' == j then speed else 0
end.
End Service.
Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
scheduled_on := scheduled_on;
service_in := service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
j : Job
s : processor_state
H : ~~ [exists c, scheduled_on j s c]
============================
service_in j s = 0
----------------------------------------------------------------------------- *)
move: H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Job : JobType
j : Job
s : processor_state
============================
~~ [exists c, scheduled_on j s c] -> service_in j s = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' v /existsP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 373)
Job : JobType
j, j' : Job
v : nat
============================
~ (exists _ : unit_finType, j' == j) -> (if j' == j then v else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP=>//=_[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
Job : JobType
j, j' : Job
v : nat
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.