Library prosa.model.task.preemption.fully_nonpreemptive
Fully Non-Preemptive Task Model
Consider any type of tasks with WCET bounds. 
In the fully non-preemptive model, no job can be preempted until its
      completion. The maximal non-preemptive segment of a job j has length
      job_cost j, which is bounded by task_cost tsk.
Run-to-Completion Threshold
Consider any type of tasks. 
In the fully non-preemptive model, no job can be preempted prior to its
      completion. In other words, once a job starts running, it is guaranteed
      to finish. Thus, we can set the task-level run-to-completion threshold
      to ε.