Library prosa.analysis.transform.swap
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.all.
This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof.
We begin by defining the notion of a schedule with a "tweaked" (i.e.,
overridden) allocation.
For any given type of jobs...
... any given type of processor states, ...
...consider any given reference schedule.
Suppose we are given a specific time [t'] ...
...and a replacement state [new_state].
Then the schedule with replacement is simply one that returns the given
[new_state] at [t'], and the original allocation at all other times.
Definition replace_at (t : instant) :=
if t' == t then new_state else (original_sched t).
End ReplaceAt.
if t' == t then new_state else (original_sched t).
End ReplaceAt.
Based on [replace_at], we define the notion of a schedule with swapped
allocations.
For any given type of jobs...
... any given type of processor states, ...
...consider any given reference schedule.
Given two specific times [t1] and [t2]...
...we define the notion of a schedule in which the two allocations at [t1]
and [t2] have been swapped.
Definition swapped : schedule PState :=
let s1 := original_sched t1 in
let s2 := original_sched t2 in
let replaced_s1 := replace_at original_sched t1 s2 in
replace_at replaced_s1 t2 s1.
End Swapped.
let s1 := original_sched t1 in
let s2 := original_sched t2 in
let replaced_s1 := replace_at original_sched t1 s2 in
replace_at replaced_s1 t2 s1.
End Swapped.