# Library prosa.analysis.transform.swap

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.

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.