Library prosa.analysis.facts.transform.replace_at

Require Export prosa.analysis.transform.swap.
Require Export prosa.analysis.facts.behavior.completion.

In this file, we make a few simple observations about schedules with replacements.

Section ReplaceAtFacts.

For any given type of jobs...

Context {Job : JobType}.

... and any given type of processor states, ...

Context {PState: ProcessorState Job}.

...consider any given reference schedule.

Variable sched: schedule PState.

Suppose we are given a specific time t' ...

Variable t': instant.

...and a replacement state state.

Variable nstate: PState.

In the following, let sched' denote the schedule with replacement at time t'.

Let sched' := replace_at sched t' nstate.

We begin with the trivial observation that replace_at sched t' nstate indeed returns nstate at time t'.

Lemma replace_at_def:
sched' t' = nstate.

Equally trivially, the schedule doesn't change at other times.

Lemma rest_of_schedule_invariant:
∀ t, t ≠ t' → sched' t = sched t.

As a result, the service in intervals that do not intersect with t' is invariant, too.

  Lemma service_at_other_times_invariant:
    ∀ t1 t2,
      t2 ≤ t' ∨ t' < t1 →
      ∀ j,
        service_during sched j t1 t2
        =
        service_during sched' j t1 t2.

Next, we consider the amount of service received in intervals that do span across the replacement point. We can relate the service received in the original and the new schedules by adding the service in the respective "missing" state...

  Lemma service_delta:
    ∀ t1 t2,
      t1 ≤ t' < t2 →
      ∀ j,
        service_during sched j t1 t2 + service_at sched' j t'
        =
        service_during sched' j t1 t2 + service_at sched j t'.

...which we can also rewrite as follows.

  Corollary service_in_replaced:
    ∀ t1 t2,
      t1 ≤ t' < t2 →
      ∀ j,
        service_during sched' j t1 t2
        =
        service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.

As another simple invariant (useful for case analysis), we observe that if a job is scheduled neither in the replaced nor in the new state, then at any time it receives exactly the same amount of service in the new schedule with replacements as in the original schedule.

  Lemma service_at_of_others_invariant (j: Job):
    ~~ scheduled_in j (sched' t') →
    ~~ scheduled_in j (sched t') →
    ∀ t,
      service_at sched j t = service_at sched' j t.

Based on the previous observation, we can trivially lift the invariant that jobs not involved in the replacement receive equal service to the cumulative service received in any interval.

  Corollary service_during_of_others_invariant (j: Job):
    ~~ scheduled_in j (sched' t') →
    ~~ scheduled_in j (sched t') →
    ∀ t1 t2,
      service_during sched j t1 t2 = service_during sched' j t1 t2.

End ReplaceAtFacts.