Add [arrives_in] to [sequential_tasks] definition
Note that the prior definition of [sequential_tasks] did not differentiate between a job coming from the arrival sequence and any other job. However, all computable properties (such as [job_respects_task_rtc, valid_preemption_model, arrivals_have_valid_job_costs, all_deadlines_of_arrivals_met]) are stated exclusively for jobs from the arrival sequence. In order to make the definition of [sequential_tasks] compatible with computable properties, we add preconditions [arrives_in arr_seq j1] and [arrives_in arr_seq j2].
parent
e33a1ebe
No related branches found
No related tags found
Showing
- analysis/abstract/abstract_seq_rta.v 2 additions, 2 deletionsanalysis/abstract/abstract_seq_rta.v
- analysis/abstract/ideal_jlfp_rta.v 5 additions, 4 deletionsanalysis/abstract/ideal_jlfp_rta.v
- analysis/facts/model/sequential.v 13 additions, 8 deletionsanalysis/facts/model/sequential.v
- model/task/sequentiality.v 12 additions, 7 deletionsmodel/task/sequentiality.v
- results/edf/rta/bounded_nps.v 1 addition, 1 deletionresults/edf/rta/bounded_nps.v
- results/edf/rta/bounded_pi.v 2 additions, 2 deletionsresults/edf/rta/bounded_pi.v
- results/edf/rta/floating_nonpreemptive.v 1 addition, 1 deletionresults/edf/rta/floating_nonpreemptive.v
- results/edf/rta/fully_nonpreemptive.v 1 addition, 1 deletionresults/edf/rta/fully_nonpreemptive.v
- results/edf/rta/fully_preemptive.v 1 addition, 1 deletionresults/edf/rta/fully_preemptive.v
- results/edf/rta/limited_preemptive.v 1 addition, 1 deletionresults/edf/rta/limited_preemptive.v
- results/fixed_priority/rta/bounded_nps.v 1 addition, 1 deletionresults/fixed_priority/rta/bounded_nps.v
- results/fixed_priority/rta/bounded_pi.v 1 addition, 1 deletionresults/fixed_priority/rta/bounded_pi.v
- results/fixed_priority/rta/floating_nonpreemptive.v 1 addition, 1 deletionresults/fixed_priority/rta/floating_nonpreemptive.v
- results/fixed_priority/rta/fully_nonpreemptive.v 1 addition, 1 deletionresults/fixed_priority/rta/fully_nonpreemptive.v
- results/fixed_priority/rta/fully_preemptive.v 1 addition, 1 deletionresults/fixed_priority/rta/fully_preemptive.v
- results/fixed_priority/rta/limited_preemptive.v 1 addition, 1 deletionresults/fixed_priority/rta/limited_preemptive.v
Loading
Please register or sign in to comment