The Prosa notion of priority-driven scheduling depends on the
preemption model. That is ok; any theory that doesn't want to deal
with non-preemptive sections can simply Require Export the fully
preemptive model and be done with it.