Library prosa.model.processor.platform_properties

To reason about classes of schedule types / processor models, we define the following properties that group processor models into classes of similar models.

Consider any job type and any processor state. Note: we make the processor state an explicit variable (rather than implicit context) because it is the primary subject of the following definitions.

We say that a processor model provides unit service if no job ever receives more than one unit of service at any time.

We say that a processor model offers ideal progress if a scheduled job always receives non-zero service.

In a uniprocessor model, the scheduled job is always unique.

We say that a processor model is a unit-supply model if no state ever produces more than one unit of supply at any time.

Note that unit_supply_proc_model implies unit_service_proc_model because of the requirement service_on_le_supply_on. But not vice versa --- a unit-service processor model is not necessarily a unit-supply processor model.

We say that a processor model is a fully consuming processor model if a job scheduled at time t receives the entire supply produced at that time as service.

We add the reduction from unit_supply_proc_model to unit_service_proc_model into the "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically where needed.