Cut down on Require Import statements

mentioned in merge request !12 (merged)

We're not going to change "classic" Prosa; that would be too much pointless work. However, before releasing v0.4, we should go through the restructured Prosa and see if we're having too may Requires anywhere.

changed milestone to %Prosa v0.4

Turns out we still have quite a few potentially superfluous Require statements. Here's a list of candidates that could be removed.

List of Files with Possibly Redundant `Require`s

`restructuring/analysis/abstract/core/abstract_rta.v`

`restructuring/analysis/abstract/core/abstract_seq_rta.v`

`restructuring/analysis/abstract/core/definitions.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/model/processor/ideal.v

`restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
- restructuring/analysis/abstract/core/definitions.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
- restructuring/analysis/abstract/core/definitions.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
- restructuring/analysis/abstract/core/definitions.v
Import restructuring/model/preemption/valid_model.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v

`restructuring/analysis/abstract/instantiations/ideal_processor.v`

Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/aggregate/workload.v
- restructuring/model/schedule/sequential.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/definitions.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/model/aggregate/workload.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/model/schedule/work_conserving.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/model/schedule/sequential.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following imports:
- restructuring/model/aggregate/workload.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/analysis/definitions/busy_interval.v could also be obtained via the following import:
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/analysis/abstract/core/definitions.v could also be obtained via the following import:
- restructuring/analysis/abstract/core/abstract_seq_rta.v
Import restructuring/model/processor/ideal.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/analysis/abstract/core/definitions.v
- restructuring/analysis/abstract/core/abstract_seq_rta.v
- restructuring/model/readiness/basic.v

`restructuring/analysis/arrival/rbf.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/arrival/workload_bound.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/aggregate/task_arrivals.v
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/arrival/workload_bound.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/aggregate/task_arrivals.v
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/arrival/workload_bound.v
Import restructuring/model/aggregate/task_arrivals.v could also be obtained via the following imports:
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/arrival/workload_bound.v
Import restructuring/model/arrival/arrival_curves.v could also be obtained via the following import:
- restructuring/analysis/arrival/workload_bound.v

`restructuring/analysis/arrival/workload_bound.v`

Import util/sum.v could also be obtained via the following imports:
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/arrivals.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/model/aggregate/task_arrivals.v
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/ideal_schedule.v
- restructuring/analysis/basic_facts/arrivals.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/model/aggregate/task_arrivals.v
- restructuring/model/arrival/arrival_curves.v
- restructuring/analysis/basic_facts/workload.v
Import restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/workload.v
Import restructuring/model/aggregate/task_arrivals.v could also be obtained via the following import:
- restructuring/model/arrival/arrival_curves.v
Import restructuring/analysis/basic_facts/arrivals.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/workload.v

`restructuring/analysis/basic_facts/completion.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/service.v
- restructuring/analysis/basic_facts/arrivals.v
Import util/nat.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/service.v
- restructuring/analysis/basic_facts/arrivals.v

`restructuring/analysis/basic_facts/deadlines.v`

Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/service.v
- restructuring/analysis/basic_facts/completion.v
Export restructuring/analysis/basic_facts/service.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/completion.v

`restructuring/analysis/basic_facts/preemption/job/limited.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/valid_schedule.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/valid_schedule.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/valid_model.v could also be obtained via the following import:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/valid_schedule.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/limited.v

`restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/schedule/nonpreemptive.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/schedule/nonpreemptive.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/preemption/valid_model.v could also be obtained via the following import:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v

`restructuring/analysis/basic_facts/preemption/job/preemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/preemptive.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/preemptive.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/instance/preemptive.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v`

`restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v`

`restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v`

`restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/preemptive.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/model/preemption/rtc_threshold/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/job/instance/preemptive.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/model/preemption/rtc_threshold/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/model/preemption/rtc_threshold/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/rtc_threshold/valid_rtct.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/model/preemption/rtc_threshold/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v

`restructuring/analysis/basic_facts/preemption/task/floating.v`

`restructuring/analysis/basic_facts/preemption/task/limited.v`

`restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/schedule/nonpreemptive.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/schedule/nonpreemptive.v
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/model/schedule/nonpreemptive.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
Import restructuring/model/preemption/job/instance/nonpreemptive.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v

`restructuring/analysis/basic_facts/preemption/task/preemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/instance/preemptive.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/job/preemptive.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/instance/preemptive.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/job/preemptive.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/job/preemptive.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/job/preemptive.v
Import restructuring/model/preemption/valid_model.v could also be obtained via the following imports:
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/analysis/basic_facts/preemption/job/preemptive.v
Import restructuring/model/preemption/job/instance/preemptive.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/job/preemptive.v

`restructuring/analysis/basic_facts/service.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/ideal_schedule.v
- restructuring/model/processor/platform_properties.v
- restructuring/model/processor/ideal.v
Import restructuring/model/processor/platform_properties.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/ideal_schedule.v
Import util/tactics.v could also be obtained via the following imports:
- util/step_function.v
- util/sum.v
Import restructuring/model/processor/ideal.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/ideal_schedule.v

`restructuring/analysis/basic_facts/service_of_jobs.v`

`restructuring/analysis/basic_facts/workload.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/aggregate/workload.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/basic_facts/arrivals.v
Import restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following import:
- restructuring/model/aggregate/workload.v
Import restructuring/analysis/basic_facts/arrivals.v could also be obtained via the following import:
- restructuring/model/aggregate/workload.v

`restructuring/analysis/definitions/busy_interval.v`

Export util/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v
Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/schedule/work_conserving.v
Export restructuring/model/task.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v

`restructuring/analysis/definitions/no_carry_in.v`

Export util/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v
Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
Export restructuring/model/task.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v

`restructuring/analysis/definitions/priority_inversion.v`

Export util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/schedule/work_conserving.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/model/job.v could also be obtained via the following import:
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/model/schedule/work_conserving.v could also be obtained via the following import:
- restructuring/analysis/definitions/busy_interval.v
Export restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/definitions/busy_interval.v

`restructuring/analysis/edf/optimality.v`

Import restructuring/model/schedule/edf.v could also be obtained via the following import:
- restructuring/analysis/transform/facts/edf_opt.v
Import restructuring/analysis/schedulability.v could also be obtained via the following import:
- restructuring/analysis/transform/facts/edf_opt.v

`restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v`

`restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v`

`restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v`

`restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v`

`restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v`

`restructuring/analysis/edf/rta/response_time_bound.v`

`restructuring/analysis/facts/busy_interval_exists.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/model/readiness/basic.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/schedule/work_conserving.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
- restructuring/model/readiness/basic.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/model/job.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/model/schedule/work_conserving.v could also be obtained via the following imports:
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/definitions/busy_interval.v
- restructuring/analysis/definitions/priority_inversion.v
Import restructuring/analysis/definitions/busy_interval.v could also be obtained via the following import:
- restructuring/analysis/definitions/priority_inversion.v

`restructuring/analysis/facts/no_carry_in_exists.v`

`restructuring/analysis/facts/priority_inversion_is_bounded.v`

`restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v`

`restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v`

`restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v`

`restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v`

`restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v`

`restructuring/analysis/fixed_priority/rta/response_time_bound.v`

`restructuring/analysis/schedulability.v`

Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/model/job_deadline.v
- restructuring/analysis/basic_facts/completion.v
Export restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/job_deadline.v
Export util/seqset.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/completion.v

`restructuring/analysis/task_schedule.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/analysis/basic_facts/ideal_schedule.v

`restructuring/analysis/transform/edf_trans.v`

Export util/search_arg.v could also be obtained via the following imports:
- restructuring/analysis/transform/prefix.v
- restructuring/analysis/transform/swap.v

`restructuring/analysis/transform/facts/edf_opt.v`

Import restructuring/analysis/basic_facts/all.v could also be obtained via the following imports:
- restructuring/analysis/transform/edf_trans.v
- restructuring/analysis/transform/facts/swaps.v
Import util/tactics.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/schedulability.v
- restructuring/analysis/transform/edf_trans.v
- restructuring/analysis/transform/facts/swaps.v
- util/nat.v
- restructuring/model/readiness/basic.v
Import util/nat.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/schedulability.v
- restructuring/analysis/transform/edf_trans.v
- restructuring/analysis/transform/facts/swaps.v
- restructuring/model/readiness/basic.v
Import restructuring/model/processor/ideal.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/analysis/schedulability.v
- restructuring/analysis/transform/edf_trans.v
- restructuring/analysis/transform/facts/swaps.v
- restructuring/model/readiness/basic.v

`restructuring/analysis/transform/facts/replace_at.v`

Import restructuring/analysis/basic_facts/all.v could also be obtained via the following import:
- restructuring/analysis/transform/swap.v
Import util/nat.v could also be obtained via the following imports:
- restructuring/analysis/transform/swap.v
- restructuring/analysis/basic_facts/all.v

`restructuring/analysis/transform/facts/swaps.v`

Import restructuring/analysis/transform/swap.v could also be obtained via the following import:
- restructuring/analysis/transform/facts/replace_at.v
Import restructuring/analysis/basic_facts/all.v could also be obtained via the following imports:
- restructuring/analysis/transform/swap.v
- restructuring/analysis/transform/facts/replace_at.v
Import util/nat.v could also be obtained via the following imports:
- restructuring/analysis/transform/swap.v
- restructuring/analysis/transform/facts/replace_at.v
- restructuring/analysis/basic_facts/all.v

`restructuring/analysis/transform/prefix.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v

`restructuring/analysis/transform/swap.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/all.v

`restructuring/behavior/arrival_sequence.v`

Import restructuring/behavior/time.v could also be obtained via the following import:
- restructuring/behavior/job.v

`restructuring/model/aggregate/service_of_jobs.v`

Import util/tactics.v could also be obtained via the following imports:
- util/sum.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/arrivals.v
- restructuring/analysis/basic_facts/completion.v
Import util/sum.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/arrivals.v
- restructuring/analysis/basic_facts/completion.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/model/processor/ideal.v
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/arrivals.v
- restructuring/analysis/basic_facts/completion.v
- restructuring/analysis/basic_facts/ideal_schedule.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/basic_facts/workload.v
Import restructuring/model/schedule/priority_based/priorities.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/workload.v
Import restructuring/model/processor/ideal.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/completion.v
- restructuring/analysis/basic_facts/ideal_schedule.v
Import restructuring/analysis/basic_facts/arrivals.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/workload.v
- restructuring/analysis/basic_facts/completion.v
Import restructuring/analysis/basic_facts/ideal_schedule.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/completion.v

`restructuring/model/aggregate/workload.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/task.v
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/analysis/basic_facts/arrivals.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/schedule/priority_based/priorities.v

`restructuring/model/arrival/arrival_curves.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/aggregate/task_arrivals.v

`restructuring/model/arrival/sporadic.v`

Export restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/task.v

`restructuring/model/preemption/floating.v`

`restructuring/model/preemption/job/instance/limited.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/job/instance/nonpreemptive.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/job/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/preemption/job/parameters.v

`restructuring/model/preemption/job/instance/preemptive.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/job/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/preemption/job/parameters.v

`restructuring/model/preemption/limited.v`

`restructuring/model/preemption/nonpreemptive.v`

Export util/nondecreasing.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/valid_schedule.v
- restructuring/model/preemption/job/instance/nonpreemptive.v
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/model/schedule/nonpreemptive.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/model/preemption/valid_model.v could also be obtained via the following imports:
- restructuring/model/preemption/task/instance/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/model/preemption/job/instance/nonpreemptive.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/model/preemption/task/instance/nonpreemptive.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
Export restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
- restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v

`restructuring/model/preemption/preemption_time.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/valid_model.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/ideal_schedule.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/processor/ideal.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/valid_model.v
Import restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/valid_model.v
Import restructuring/model/processor/ideal.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/ideal_schedule.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/model/preemption/preemptive.v`

Export util/nondecreasing.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/valid_schedule.v
- restructuring/model/preemption/job/instance/preemptive.v
- restructuring/model/preemption/task/instance/preemptive.v
- restructuring/model/preemption/rtc_threshold/instance/preemptive.v
Export restructuring/model/preemption/valid_model.v could also be obtained via the following import:
- restructuring/model/preemption/task/instance/preemptive.v

`restructuring/model/preemption/rtc_threshold/instance/floating.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/rtc_threshold/instance/limited.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/job.v could also be obtained via the following imports:
- restructuring/behavior/schedule.v
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/schedule.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/rtc_threshold/instance/preemptive.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/rtc_threshold/valid_rtct.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import util/nondecreasing.v could also be obtained via the following imports:
- util/all.v
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/analysis/basic_facts/all.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/model/preemption/task/instance/floating.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/job/instance/limited.v

`restructuring/model/preemption/task/instance/limited.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import util/nondecreasing.v could also be obtained via the following imports:
- util/all.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/task/parameters.v
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/job/instance/limited.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/job/instance/limited.v

`restructuring/model/preemption/task/instance/nonpreemptive.v`

Export util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Export restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Export restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Export restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/parameters.v
Export restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Export restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/model/preemption/task/instance/preemptive.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/preemption/valid_model.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v
Import restructuring/model/preemption/task/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/valid_model.v

`restructuring/model/preemption/task/parameters.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/task.v

`restructuring/model/preemption/valid_model.v`

Import util/all.v could also be obtained via the following imports:
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/job.v
- restructuring/model/task.v
- restructuring/model/preemption/job/parameters.v
- restructuring/model/preemption/task/parameters.v
Import restructuring/model/task.v could also be obtained via the following import:
- restructuring/model/preemption/task/parameters.v

`restructuring/model/preemption/valid_schedule.v`

Import util/all.v could also be obtained via the following import:
- restructuring/model/preemption/job/parameters.v
Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/processor/ideal.v
- restructuring/model/preemption/job/parameters.v

`restructuring/model/readiness/basic.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/analysis/basic_facts/completion.v

`restructuring/model/schedule/nonpreemptive.v`

Import restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/job.v

`restructuring/model/schedule/priority_based/edf.v`

Import restructuring/model/job.v could also be obtained via the following import:
- restructuring/model/job_deadline.v
Import restructuring/model/task.v could also be obtained via the following imports:
- restructuring/model/job_deadline.v
- restructuring/model/schedule/priority_based/priorities.v

`restructuring/model/schedule/priority_based/preemption_aware.v`

Import restructuring/behavior/all.v could also be obtained via the following imports:
- restructuring/model/schedule/priority_based/priorities.v
- restructuring/model/processor/ideal.v
- restructuring/model/preemption/preemption_time.v
- restructuring/model/preemption/job/parameters.v
Import restructuring/model/processor/ideal.v could also be obtained via the following import:
- restructuring/model/preemption/preemption_time.v
Import restructuring/model/preemption/job/parameters.v could also be obtained via the following import:
- restructuring/model/preemption/preemption_time.v

`restructuring/model/schedule/priority_based/preemptive.v`

Export restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/schedule/priority_based/priorities.v

`restructuring/model/schedule/sequential.v`

Export restructuring/behavior/all.v could also be obtained via the following import:
- restructuring/model/task.v

`util/div_mod.v`

Import util/ssromega.v could also be obtained via the following import:
- util/nat.v

`util/minmax.v`

Import util/tactics.v could also be obtained via the following imports:
- util/nat.v
- util/list.v

`util/nondecreasing.v`

Import util/tactics.v could also be obtained via the following imports:
- util/nat.v
- util/list.v
Import util/ssromega.v could also be obtained via the following imports:
- util/nat.v
- util/list.v

`util/sum.v`

Import util/tactics.v could also be obtained via the following import:
- util/nat.v
Import util/ssromega.v could also be obtained via the following import:
- util/nat.v

@sbozhko: A lot of these come from recently merged files related to aRTA. Can you please help me with cutting these down? Let's use the above list to coordinate.

Please base any patches on top of the disambiguate-require branch, as otherwise we'll get one heck of a merge conflict.

@mlesourd @sophie @Lucien @proux: if you have any free cycles, feel free to help with getting Prosa into shape for the v0.4 release. Any help would be greatly appreciated. :-)

I've cleaned up most files not coming from the recent aRTA merge. My progress is in the require-removal branch. Please feel free to push commits to the branch.

@sbozhko: there's a script in the branch to check for redundant Require statements. If you want to see the current state, run the following command:

scripts/redreq-finder.py `find  util restructuring -iname '*.v'`

With Sergey's update of !68 (merged), this cleanup is done.

closed

mentioned in commit 64e0d9ae

Cut down on Require Import statements

Activity

List of Files with Possibly Redundant Requires

restructuring/analysis/abstract/core/abstract_rta.v

restructuring/analysis/abstract/core/abstract_seq_rta.v

restructuring/analysis/abstract/core/definitions.v

restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v

restructuring/analysis/abstract/instantiations/ideal_processor.v

restructuring/analysis/arrival/rbf.v

restructuring/analysis/arrival/workload_bound.v

restructuring/analysis/basic_facts/completion.v

restructuring/analysis/basic_facts/deadlines.v

restructuring/analysis/basic_facts/preemption/job/limited.v

restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v

restructuring/analysis/basic_facts/preemption/job/preemptive.v

restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v

restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v

restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v

restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v

restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v

restructuring/analysis/basic_facts/preemption/task/floating.v

restructuring/analysis/basic_facts/preemption/task/limited.v

restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v

restructuring/analysis/basic_facts/preemption/task/preemptive.v

restructuring/analysis/basic_facts/service.v

restructuring/analysis/basic_facts/service_of_jobs.v

restructuring/analysis/basic_facts/workload.v

restructuring/analysis/definitions/busy_interval.v

restructuring/analysis/definitions/no_carry_in.v

restructuring/analysis/definitions/priority_inversion.v

restructuring/analysis/edf/optimality.v

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v

restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v

restructuring/analysis/edf/rta/response_time_bound.v

restructuring/analysis/facts/busy_interval_exists.v

restructuring/analysis/facts/no_carry_in_exists.v

restructuring/analysis/facts/priority_inversion_is_bounded.v

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v

restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v

restructuring/analysis/fixed_priority/rta/response_time_bound.v

restructuring/analysis/schedulability.v

restructuring/analysis/task_schedule.v

restructuring/analysis/transform/edf_trans.v

restructuring/analysis/transform/facts/edf_opt.v

restructuring/analysis/transform/facts/replace_at.v

restructuring/analysis/transform/facts/swaps.v

restructuring/analysis/transform/prefix.v

restructuring/analysis/transform/swap.v

restructuring/behavior/arrival_sequence.v

restructuring/model/aggregate/service_of_jobs.v

restructuring/model/aggregate/workload.v

restructuring/model/arrival/arrival_curves.v

restructuring/model/arrival/sporadic.v

restructuring/model/preemption/floating.v

restructuring/model/preemption/job/instance/limited.v

restructuring/model/preemption/job/instance/nonpreemptive.v

restructuring/model/preemption/job/instance/preemptive.v

restructuring/model/preemption/limited.v

restructuring/model/preemption/nonpreemptive.v

restructuring/model/preemption/preemption_time.v

restructuring/model/preemption/preemptive.v

restructuring/model/preemption/rtc_threshold/instance/floating.v

restructuring/model/preemption/rtc_threshold/instance/limited.v

restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v

restructuring/model/preemption/rtc_threshold/instance/preemptive.v

restructuring/model/preemption/rtc_threshold/valid_rtct.v

restructuring/model/preemption/task/instance/floating.v

restructuring/model/preemption/task/instance/limited.v

restructuring/model/preemption/task/instance/nonpreemptive.v

restructuring/model/preemption/task/instance/preemptive.v

restructuring/model/preemption/task/parameters.v

restructuring/model/preemption/valid_model.v

restructuring/model/preemption/valid_schedule.v

restructuring/model/readiness/basic.v