Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
586 commits behind the upstream repository.
-
Björn Brandenburg authoredThe two concepts are tightly coupled and it does not make sense to mix and match them. Therefore, it's cleaner and easier to understand if both aspects of the preemption model are instantiated in the same module next to each other.
Björn Brandenburg authoredThe two concepts are tightly coupled and it does not make sense to mix and match them. Therefore, it's cleaner and easier to understand if both aspects of the preemption model are instantiated in the same module next to each other.
preemptive.v 213 B
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.fully_preemptive.