Library prosa.analysis.facts.model.restricted_supply.schedule

Require Export prosa.model.processor.platform_properties.
Require Export prosa.model.processor.restricted_supply.

In this section we establish the classes to which a restricted-supply schedule belongs.
Section ScheduleClass.

  Local Transparent scheduled_in scheduled_on service_on.

We assume a restricted-supply uni-processor schedule.
  #[local] Existing Instance rs_processor_state.

Consider any job type and the ideal processor model.
  Context {Job: JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

We note that the restricted-supply processor model is indeed a uni-processor model.
  Lemma rs_proc_model_is_a_uniprocessor_model :
    uniprocessor_model (rs_processor_state Job).

Restricted-supply processor model is unit-supply.
  Lemma rs_proc_is_unit_supply :
    unit_supply_proc_model (rs_processor_state Job).

Restricted-supply processor model is a fully supply-consuming processor model.
  Lemma rs_proc_model_fully_consuming :
    fully_consuming_proc_model (rs_processor_state Job).

End ScheduleClass.

Automation

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
       rs_proc_model_is_a_uniprocessor_model
       rs_proc_is_unit_supply
       rs_proc_model_fully_consuming : basic_rt_facts.