Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa protected
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.025Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov2423201817Make the basic readiness hypothesis more explicitRemove multiprocessor Global InstanceRemove var. speed processor model Global InstanceRemove spin processor model Global InstanceRemove unused RequiresMake the ideal uniprocessor hypothesis more explicitmake the policy explicit in policy-compliance predicatesadd lemmas to exploit basic behavior hypotheses introduce [rt_auto] and [rt_eauto] tacticsProperly deprecate ltn_leq_transsimplify `conversion_preserves_equivalence` proofbe explicit in how service is accrued on ideal processorsdefine GEL priority policyupdate esy packagedocument #86 in the style guidelinesremove ssrlia entirelyupdate documentation to mention the mczify dependencyCI: run `opam update` before `opam install`CI: don't remove dependencies of coq-mathcomp-zifyReplace ssrlia with mczifyPut State inside ProcessorStateRemove unused sectionDeprecate ltn_leq_transRestore compatibility with Coq 8.13examples of how to avoid `apply with`Rename arguments of [apply _ with (NAME0 := _)]update Alectryon imagecoqdoc: remove unnecessary --coqlib flagbump supported Coq and mathcomp versions and update CIdefine `service_on` in the class `ProcessorState`change [job_task j = tsk] to [job_of_task tsk j]update coding guidlines (require external deps first)Fix some AdmittedfsetfsetRequire external libraries first[WIP] Replace seq with finite setsEmbeds arrival_uniq into arrival sequencesembed_arr_seq_u…embed_arr_seq_uniqadd an RTA for FIFO scheduling based on aRTAadd new helper lemma about RBFIntroduce extrapolated arrival curve Add bounded tardiness definition