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.019Nov181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029Add 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 intervalMove workload lemma to basic filesAdd file to util.allAdd lemma to util.sumAdd lemmas to util.listAdd tactics for inequalitiesImprove documentation in restructuring/behaviorUpdate coqdocjsdocument the --only-classic optioncleanup create_makefile.shcreate_makefile.sh: add --only-classic optionmention classic/util in READMEmove unused helper lemmas/notations/tactics to rt.classicdo not rely on simpl_sum_const tacticdo not use vlib 'edone' when plain 'eassumption' will dodo not rely on vlib 'des' tacticdo not rely on vlib x <= y <= z auto-splittingDon't re-generate _CoqProject in create_makefile.shcreate_makefile.sh: support --without-classicproofloc.py: do not count proofs that have been commented outproofloc.py: fix single-line proof patternadd READMEs to behavior and model modulesupdate explanation of new Prosa's structuredocument additional guidelinesupdate documentation and guidelinesUpdate top-level and classic/ READMEsupdate paths in the known long proofs databaseupdate Require'd module names to rt.classic namespacemove classic Prosa into rt.classic namespace