PROSA - Formally Proven Schedulability Analysis issueshttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues2019-10-22T13:48:11Zhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/1Definition of JLDP priority policy is too inflexible2019-10-22T13:48:11ZBjörn BrandenburgDefinition of JLDP priority policy is too inflexibleThe current definition of JLDP priority is as follows:
```
Definition jldp_policy := time -> JobIn arr_seq -> JobIn arr_seq -> bool.
```
This is too inflexible as one cannot define common JLDP policies such as *least laxity first* ...The current definition of JLDP priority is as follows:
```
Definition jldp_policy := time -> JobIn arr_seq -> JobIn arr_seq -> bool.
```
This is too inflexible as one cannot define common JLDP policies such as *least laxity first* or *PD^2* in which the current priority of a job depends on how much service it has already received.
Instead, the definition should be generalized to depend on the schedule prefix up to the time at which it is queried.Felipe CerqueiraFelipe Cerqueira