Hierarchical Index of ‘proof-recorder’ Branch

• rt:
  • rt.restructuring:
    • rt.restructuring.analysis:
      • rt.restructuring.analysis.schedulability
      • rt.restructuring.analysis.task_schedule
      • rt.restructuring.analysis.abstract:
        • rt.restructuring.analysis.abstract.core:
          • rt.restructuring.analysis.abstract.core.abstract_rta
          • rt.restructuring.analysis.abstract.core.abstract_seq_rta
          • rt.restructuring.analysis.abstract.core.definitions
          • rt.restructuring.analysis.abstract.core.reduction_of_search_space
          • rt.restructuring.analysis.abstract.core.run_to_completion_threshold
          • rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold
        • rt.restructuring.analysis.abstract.instantiations:
          • rt.restructuring.analysis.abstract.instantiations.ideal_processor
      • rt.restructuring.analysis.arrival:
        • rt.restructuring.analysis.arrival.rbf
        • rt.restructuring.analysis.arrival.workload_bound
      • rt.restructuring.analysis.basic_facts:
        • rt.restructuring.analysis.basic_facts.all
        • rt.restructuring.analysis.basic_facts.arrivals
        • rt.restructuring.analysis.basic_facts.completion
        • rt.restructuring.analysis.basic_facts.deadlines
        • rt.restructuring.analysis.basic_facts.ideal_schedule
        • rt.restructuring.analysis.basic_facts.sequential
        • rt.restructuring.analysis.basic_facts.service
        • rt.restructuring.analysis.basic_facts.service_of_jobs
        • rt.restructuring.analysis.basic_facts.task_arrivals
        • rt.restructuring.analysis.basic_facts.workload
        • rt.restructuring.analysis.basic_facts.preemption:
          • rt.restructuring.analysis.basic_facts.preemption.job:
            • rt.restructuring.analysis.basic_facts.preemption.job.limited
            • rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive
            • rt.restructuring.analysis.basic_facts.preemption.job.preemptive
          • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold:
            • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating
            • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable
            • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited
            • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive
            • rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive
          • rt.restructuring.analysis.basic_facts.preemption.task:
            • rt.restructuring.analysis.basic_facts.preemption.task.floating
            • rt.restructuring.analysis.basic_facts.preemption.task.limited
            • rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive
            • rt.restructuring.analysis.basic_facts.preemption.task.preemptive
      • rt.restructuring.analysis.definitions:
        • rt.restructuring.analysis.definitions.busy_interval
        • rt.restructuring.analysis.definitions.no_carry_in
        • rt.restructuring.analysis.definitions.priority_inversion
      • rt.restructuring.analysis.edf:
        • rt.restructuring.analysis.edf.optimality
        • rt.restructuring.analysis.edf.rta:
          • rt.restructuring.analysis.edf.rta.response_time_bound
          • rt.restructuring.analysis.edf.rta.nonpr_reg:
            • rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound
            • rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models:
              • rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.floating
              • rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.limited
              • rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.nonpreemptive
              • rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.preemptive
      • rt.restructuring.analysis.facts:
        • rt.restructuring.analysis.facts.busy_interval_exists
        • rt.restructuring.analysis.facts.no_carry_in_exists
        • rt.restructuring.analysis.facts.priority_inversion_is_bounded
      • rt.restructuring.analysis.fixed_priority:
        • rt.restructuring.analysis.fixed_priority.rta:
          • rt.restructuring.analysis.fixed_priority.rta.response_time_bound
          • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg:
            • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound
            • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models:
              • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.floating
              • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.limited
              • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.nonpreemptive
              • rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.preemptive
      • rt.restructuring.analysis.transform:
        • rt.restructuring.analysis.transform.edf_trans
        • rt.restructuring.analysis.transform.prefix
        • rt.restructuring.analysis.transform.swap
        • rt.restructuring.analysis.transform.facts:
          • rt.restructuring.analysis.transform.facts.edf_opt
          • rt.restructuring.analysis.transform.facts.replace_at
          • rt.restructuring.analysis.transform.facts.swaps
    • rt.restructuring.behavior:
      • rt.restructuring.behavior.all
      • rt.restructuring.behavior.arrival_sequence
      • rt.restructuring.behavior.job
      • rt.restructuring.behavior.ready
      • rt.restructuring.behavior.schedule
      • rt.restructuring.behavior.service
      • rt.restructuring.behavior.time
    • rt.restructuring.model:
      • rt.restructuring.model.job_deadline
      • rt.restructuring.model.job
      • rt.restructuring.model.task
      • rt.restructuring.model.aggregate:
        • rt.restructuring.model.aggregate.service_of_jobs
        • rt.restructuring.model.aggregate.task_arrivals
        • rt.restructuring.model.aggregate.workload
      • rt.restructuring.model.arrival:
        • rt.restructuring.model.arrival.arrival_curves
        • rt.restructuring.model.arrival.sporadic
      • rt.restructuring.model.preemption:
        • rt.restructuring.model.preemption.floating
        • rt.restructuring.model.preemption.limited
        • rt.restructuring.model.preemption.nonpreemptive
        • rt.restructuring.model.preemption.preemption_time
        • rt.restructuring.model.preemption.preemptive
        • rt.restructuring.model.preemption.valid_model
        • rt.restructuring.model.preemption.valid_schedule
        • rt.restructuring.model.preemption.job:
          • rt.restructuring.model.preemption.job.parameters
          • rt.restructuring.model.preemption.job.instance:
            • rt.restructuring.model.preemption.job.instance.limited
            • rt.restructuring.model.preemption.job.instance.nonpreemptive
            • rt.restructuring.model.preemption.job.instance.preemptive
        • rt.restructuring.model.preemption.rtc_threshold:
          • rt.restructuring.model.preemption.rtc_threshold.valid_rtct
          • rt.restructuring.model.preemption.rtc_threshold.instance:
            • rt.restructuring.model.preemption.rtc_threshold.instance.floating
            • rt.restructuring.model.preemption.rtc_threshold.instance.limited
            • rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive
            • rt.restructuring.model.preemption.rtc_threshold.instance.preemptive
        • rt.restructuring.model.preemption.task:
          • rt.restructuring.model.preemption.task.parameters
          • rt.restructuring.model.preemption.task.instance:
            • rt.restructuring.model.preemption.task.instance.floating
            • rt.restructuring.model.preemption.task.instance.limited
            • rt.restructuring.model.preemption.task.instance.nonpreemptive
            • rt.restructuring.model.preemption.task.instance.preemptive
      • rt.restructuring.model.processor:
        • rt.restructuring.model.processor.ideal
        • rt.restructuring.model.processor.multiprocessor
        • rt.restructuring.model.processor.platform_properties
        • rt.restructuring.model.processor.spin
        • rt.restructuring.model.processor.varspeed
      • rt.restructuring.model.readiness:
        • rt.restructuring.model.readiness.basic
        • rt.restructuring.model.readiness.jitter
      • rt.restructuring.model.schedule:
        • rt.restructuring.model.schedule.edf
        • rt.restructuring.model.schedule.nonpreemptive
        • rt.restructuring.model.schedule.sequential
        • rt.restructuring.model.schedule.work_conserving
        • rt.restructuring.model.schedule.priority_based:
          • rt.restructuring.model.schedule.priority_based.edf
          • rt.restructuring.model.schedule.priority_based.preemption_aware
          • rt.restructuring.model.schedule.priority_based.preemptive
          • rt.restructuring.model.schedule.priority_based.priorities
        • rt.restructuring.model.schedule.tdma:
          • rt.restructuring.model.schedule.tdma.tdma_facts
          • rt.restructuring.model.schedule.tdma.tdma
  • rt.util:
    • rt.util.all
    • rt.util.bigcat
    • rt.util.counting
    • rt.util.div_mod
    • rt.util.epsilon
    • rt.util.list
    • rt.util.minmax
    • rt.util.nat
    • rt.util.nondecreasing
    • rt.util.notation
    • rt.util.rel
    • rt.util.rewrite_facilities
    • rt.util.search_arg
    • rt.util.seqset
    • rt.util.ssromega
    • rt.util.step_function
    • rt.util.sum
    • rt.util.tactics