Library prosa.behavior.time

Library prosa.behavior.job

Library prosa.behavior.schedule

Library prosa.behavior.service

Library prosa.behavior.arrival_sequence

Library prosa.behavior.ready

Library prosa.behavior.all

Library prosa.model.processor.ideal

Library prosa.model.processor.multiprocessor

Library prosa.model.processor.platform_properties

Library prosa.model.processor.spin

Library prosa.model.processor.varspeed

Library prosa.model.readiness.basic

Library prosa.model.readiness.jitter

Library prosa.model.readiness.suspension

Library prosa.model.preemption.fully_nonpreemptive

Library prosa.model.preemption.fully_preemptive

Library prosa.model.preemption.limited_preemptive

Library prosa.model.preemption.parameter

Library prosa.model.task.absolute_deadline

Library prosa.model.task.arrival.curves

Library prosa.model.task.arrival.periodic

Library prosa.model.task.arrival.sporadic

Library prosa.model.task.arrivals

Library prosa.model.task.concept

Library prosa.model.task.preemption.floating_nonpreemptive

Library prosa.model.task.preemption.fully_nonpreemptive

Library prosa.model.task.preemption.fully_preemptive

Library prosa.model.task.preemption.limited_preemptive

Library prosa.model.task.preemption.parameters

Library prosa.model.task.sequentiality

Library prosa.model.task.suspension.dynamic

Library prosa.model.priority.classes

Library prosa.model.priority.deadline_monotonic

Library prosa.model.priority.edf

Library prosa.model.priority.fifo

Library prosa.model.priority.numeric_fixed_priority

Library prosa.model.priority.rate_monotonic

Library prosa.model.schedule.edf

Library prosa.model.schedule.limited_preemptive

Library prosa.model.schedule.nonpreemptive

Library prosa.model.schedule.preemption_time

Library prosa.model.schedule.priority_driven

Library prosa.model.schedule.tdma

Library prosa.model.schedule.work_conserving

Library prosa.model.aggregate.service_of_jobs

Library prosa.model.aggregate.workload

Library prosa.results.edf.optimality

Library prosa.results.edf.rta.bounded_nps

Library prosa.results.edf.rta.bounded_pi

Library prosa.results.edf.rta.floating_nonpreemptive

Library prosa.results.edf.rta.fully_nonpreemptive

Library prosa.results.edf.rta.fully_preemptive

Library prosa.results.edf.rta.limited_preemptive

Library prosa.results.fixed_priority.rta.bounded_nps

Library prosa.results.fixed_priority.rta.bounded_pi

Library prosa.results.fixed_priority.rta.floating_nonpreemptive

Library prosa.results.fixed_priority.rta.fully_nonpreemptive

Library prosa.results.fixed_priority.rta.fully_preemptive

Library prosa.results.fixed_priority.rta.limited_preemptive

Library prosa.analysis.abstract.abstract_rta

Library prosa.analysis.abstract.abstract_seq_rta

Library prosa.analysis.abstract.definitions

Library prosa.analysis.abstract.ideal_jlfp_rta

Library prosa.analysis.abstract.run_to_completion

Library prosa.analysis.abstract.search_space

Library prosa.analysis.definitions.busy_interval

Library prosa.analysis.definitions.carry_in

Library prosa.analysis.definitions.job_properties

Library prosa.analysis.definitions.priority_inversion

Library prosa.analysis.definitions.progress

Library prosa.analysis.definitions.request_bound_function

Library prosa.analysis.definitions.schedulability

Library prosa.analysis.definitions.task_schedule

Library prosa.analysis.facts.behavior.all

Library prosa.analysis.facts.behavior.arrivals

Library prosa.analysis.facts.behavior.completion

Library prosa.analysis.facts.behavior.deadlines

Library prosa.analysis.facts.behavior.service

Library prosa.analysis.facts.busy_interval.busy_interval

Library prosa.analysis.facts.busy_interval.carry_in

Library prosa.analysis.facts.busy_interval.priority_inversion

Library prosa.analysis.facts.edf

Library prosa.analysis.facts.model.ideal_schedule

Library prosa.analysis.facts.model.rbf

Library prosa.analysis.facts.model.sequential

Library prosa.analysis.facts.model.service_of_jobs

Library prosa.analysis.facts.model.task_arrivals

Library prosa.analysis.facts.model.workload

Library prosa.analysis.facts.preemption.job.limited

Library prosa.analysis.facts.preemption.job.nonpreemptive

Library prosa.analysis.facts.preemption.job.preemptive

Library prosa.analysis.facts.preemption.rtc_threshold.floating

Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable

Library prosa.analysis.facts.preemption.rtc_threshold.limited

Library prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive

Library prosa.analysis.facts.preemption.rtc_threshold.preemptive

Library prosa.analysis.facts.preemption.task.floating

Library prosa.analysis.facts.preemption.task.limited

Library prosa.analysis.facts.preemption.task.nonpreemptive

Library prosa.analysis.facts.preemption.task.preemptive

Library prosa.analysis.facts.readiness.basic

Library prosa.analysis.facts.tdma

Library prosa.analysis.facts.transform.edf_opt

Library prosa.analysis.facts.transform.replace_at

Library prosa.analysis.facts.transform.swaps

Library prosa.analysis.transform.edf_trans

Library prosa.analysis.transform.prefix

Library prosa.analysis.transform.swap

Library prosa.util.all

Library prosa.util.bigcat

Library prosa.util.counting

Library prosa.util.div_mod

Library prosa.util.epsilon

Library prosa.util.list

Library prosa.util.minmax

Library prosa.util.nat

Library prosa.util.nondecreasing

Library prosa.util.notation

Library prosa.util.rel

Library prosa.util.rewrite_facilities

Library prosa.util.search_arg

Library prosa.util.seqset

Library prosa.util.ssromega

Library prosa.util.step_function

Library prosa.util.sum

Library prosa.util.supremum

Library prosa.util.tactics


This page has been generated by coqdoc