Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Dec20Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029remove unneeded Require statements in model/arrivalremove unneeded Require statements in model/aggregateremove unneeded Require statements in model/schedulefix dependency of preemption time model on analysis factsfix dependency of basic readiness model on analysis factsfix dependency of preemption model on analysis factsremove unneeded 'Require' statement in behavior specremove unneeded `Require Import` statements in rt.utilCI: re-enable parallel builds in proof-state generationdisambiguate Require commands in rt.restructuringdisambiguate Require commands in rt.util and rt.classic.utiluse Gitlab DAG feature and re-organize CI orderproofloc.py: "Next Obligation" also starts a proofCI: build docs with interspersed proof stateadd script for interspersing proof state in source filesdon't pick up annotated copies in create_makefile.shadd script for recording proof stateEDF instantiationsFP instantiationsAdd concise imports of preemption modelsAdd add instances of rtc_thresholdAdd add instances of task_preemptableAdd add instances of job_preemptableAdd notion of schedule with limited preemptionsAdd proof that priority inversion is boundedAdd notion of preemptions for priority-aware schedulerAdd notion of preemption timeRestructure preemption parameters of jobAdd instantiation for ideal uni-processorAdd EDF priorityRestructure model.taskAdd notion of sequential jobs -aware policyAdd notion of busy intervalAdd lemmas about service of jobsAdd destruction tactic for ideal uni-processorAdd notion of idleness for ideal uni-processorRename and move preemption.util fileAdd notion of non-preemptive scheduleAdd lemmas about incremental serviceAdd lemma about arrivals in empty interval