Library prosa.classic.model.schedule.global.transformation.construction

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path finfun.

Module ScheduleConstruction.

  Import ArrivalSequence Schedule.

  Section ConstructionFromPrefixes.

    Context {Job: eqType}.

    Variable arr_seq: arrival_sequence Job.

    Variable num_cpus: nat.

    Variable build_schedule:
      schedule Job num_cpus → schedule Job num_cpus.

    Variable base_sched: schedule Job num_cpus.

    Definition update_schedule (prev_sched: schedule Job num_cpus)
                               (t_next: time) : schedule Job num_cpus :=
      fun (cpu: processor num_cpus) t ⇒
        if t == t_next then
          build_schedule prev_sched cpu t
        else prev_sched cpu t.

    Fixpoint schedule_prefix (t_max: time) : schedule Job num_cpus :=
      if t_max is t_prev.+1 then
        update_schedule (schedule_prefix t_prev) t_prev.+1
      else
        update_schedule base_sched 0.

    Definition build_schedule_from_prefixes := fun cpu t ⇒ schedule_prefix t cpu t.

    Section Lemmas.

      Let sched := build_schedule_from_prefixes.

      Lemma prefix_construction_same_prefix:
        ∀ t t_max cpu,
          t ≤ t_max →
          schedule_prefix t_max cpu t = sched cpu t.

      Section ServiceDependent.

        Hypothesis H_depends_only_on_service:
          ∀ sched1 sched2 cpu t,
            (∀ j, service sched1 j t = service sched2 j t) →
            build_schedule sched1 cpu t = build_schedule sched2 cpu t.

        Lemma service_dependent_schedule_construction:
          ∀ cpu t,
            sched cpu t = build_schedule sched cpu t.

      End ServiceDependent.

      Section PrefixDependent.

        Hypothesis H_depends_only_on_prefix:
          ∀ (sched1 sched2: schedule Job num_cpus) cpu t,
            (∀ t0 cpu, t0 < t → sched1 cpu t0 = sched2 cpu t0) →
            build_schedule sched1 cpu t = build_schedule sched2 cpu t.

        Lemma prefix_dependent_schedule_construction:
          ∀ cpu t, sched cpu t = build_schedule sched cpu t.

      End PrefixDependent.

    End Lemmas.

  End ConstructionFromPrefixes.

End ScheduleConstruction.