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.sequential

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.curve_as_rbf

Library prosa.model.task.arrival.curves

Library prosa.model.task.arrival.example

Library prosa.model.task.arrival.periodic

Library prosa.model.task.arrival.periodic_as_sporadic

Library prosa.model.task.arrival.request_bound_functions

Library prosa.model.task.arrival.sporadic

Library prosa.model.task.arrival.sporadic_as_curve

Library prosa.model.task.arrival.task_max_inter_arrival

Library prosa.model.task.arrivals

Library prosa.model.task.concept

Library prosa.model.task.offset

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.gel

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.fifo.rta

Library prosa.results.fixed_priority.rta.bounded_nps

Library prosa.results.fixed_priority.rta.bounded_pi

Library prosa.results.fixed_priority.rta.comp.fully_preemptive

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.results.gel.rta.bounded_pi

Library prosa.analysis.abstract.abstract_rta

Library prosa.analysis.abstract.busy_interval

Library prosa.analysis.abstract.definitions

Library prosa.analysis.abstract.ideal.abstract_rta

Library prosa.analysis.abstract.ideal.abstract_seq_rta

Library prosa.analysis.abstract.ideal.iw_instantiation

Library prosa.analysis.abstract.iw_auxiliary

Library prosa.analysis.abstract.lower_bound_on_service

Library prosa.analysis.abstract.search_space

Library prosa.analysis.definitions.always_higher_priority

Library prosa.analysis.definitions.busy_interval

Library prosa.analysis.definitions.carry_in

Library prosa.analysis.definitions.completion_sequence

Library prosa.analysis.definitions.hyperperiod

Library prosa.analysis.definitions.infinite_jobs

Library prosa.analysis.definitions.job_properties

Library prosa.analysis.definitions.job_response_time

Library prosa.analysis.definitions.priority_inversion

Library prosa.analysis.definitions.progress

Library prosa.analysis.definitions.readiness

Library prosa.analysis.definitions.request_bound_function

Library prosa.analysis.definitions.schedulability

Library prosa.analysis.definitions.schedule_prefix

Library prosa.analysis.definitions.tardiness

Library prosa.analysis.definitions.task_schedule

Library prosa.analysis.definitions.work_bearing_readiness

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.ideal.hep_job_scheduled

Library prosa.analysis.facts.busy_interval.ideal.inequalities

Library prosa.analysis.facts.busy_interval.ideal.priority_inversion

Library prosa.analysis.facts.busy_interval.ideal.priority_inversion_bounded

Library prosa.analysis.facts.busy_interval.priority_inversion

Library prosa.analysis.facts.busy_interval.quiet_time

Library prosa.analysis.facts.edf_definitions

Library prosa.analysis.facts.hyperperiod

Library prosa.analysis.facts.job_index

Library prosa.analysis.facts.model.arrival_curves

Library prosa.analysis.facts.model.ideal.schedule

Library prosa.analysis.facts.model.ideal.service_of_jobs

Library prosa.analysis.facts.model.offset

Library prosa.analysis.facts.model.preemption

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.task_cost

Library prosa.analysis.facts.model.task_schedule

Library prosa.analysis.facts.model.workload

Library prosa.analysis.facts.periodic.arrival_separation

Library prosa.analysis.facts.periodic.arrival_times

Library prosa.analysis.facts.periodic.max_inter_arrival

Library prosa.analysis.facts.periodic.task_arrivals_size

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.priority.classes

Library prosa.analysis.facts.priority.edf

Library prosa.analysis.facts.priority.fifo

Library prosa.analysis.facts.priority.gel

Library prosa.analysis.facts.priority.sequential

Library prosa.analysis.facts.readiness.backlogged

Library prosa.analysis.facts.readiness.basic

Library prosa.analysis.facts.readiness.sequential

Library prosa.analysis.facts.shifted_job_costs

Library prosa.analysis.facts.sporadic.arrival_bound

Library prosa.analysis.facts.sporadic.arrival_sequence

Library prosa.analysis.facts.sporadic.arrival_times

Library prosa.analysis.facts.tdma

Library prosa.analysis.facts.transform.edf_opt

Library prosa.analysis.facts.transform.edf_wc

Library prosa.analysis.facts.transform.replace_at

Library prosa.analysis.facts.transform.swaps

Library prosa.analysis.facts.transform.wc_correctness

Library prosa.analysis.transform.edf_trans

Library prosa.analysis.transform.prefix

Library prosa.analysis.transform.swap

Library prosa.analysis.transform.wc_trans

Library prosa.util.all

Library prosa.util.bigcat

Library prosa.util.div_mod

Library prosa.util.epsilon

Library prosa.util.fixpoint

Library prosa.util.lcmseq

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.search_arg

Library prosa.util.seqset

Library prosa.util.setoid

Library prosa.util.subadditivity

Library prosa.util.sum

Library prosa.util.superadditivity

Library prosa.util.supremum

Library prosa.util.tactics

Library prosa.util.unit_growth

Library prosa.implementation.definitions.arrival_bound

Library prosa.implementation.definitions.extrapolated_arrival_curve

Library prosa.implementation.definitions.generic_scheduler

Library prosa.implementation.definitions.ideal_uni_scheduler

Library prosa.implementation.definitions.job_constructor

Library prosa.implementation.definitions.maximal_arrival_sequence

Library prosa.implementation.definitions.task

Library prosa.implementation.facts.extrapolated_arrival_curve

Library prosa.implementation.facts.generic_schedule

Library prosa.implementation.facts.ideal_uni.preemption_aware

Library prosa.implementation.facts.ideal_uni.prio_aware

Library prosa.implementation.facts.job_constructor

Library prosa.implementation.facts.maximal_arrival_sequence

Library prosa.implementation.refinements.EDF.fast_search_space

Library prosa.implementation.refinements.EDF.nonpreemptive_sched

Library prosa.implementation.refinements.EDF.preemptive_sched

Library prosa.implementation.refinements.EDF.refinements

Library prosa.implementation.refinements.FP.fast_search_space

Library prosa.implementation.refinements.FP.nonpreemptive_sched

Library prosa.implementation.refinements.FP.preemptive_sched

Library prosa.implementation.refinements.FP.refinements

Library prosa.implementation.refinements.arrival_bound

Library prosa.implementation.refinements.arrival_curve

Library prosa.implementation.refinements.arrival_curve_prefix

Library prosa.implementation.refinements.fast_search_space_computation

Library prosa.implementation.refinements.refinements

Library prosa.implementation.refinements.task


This page has been generated by coqdoc