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.027Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029port notions of job/task deadlines and schedulability to restructuringsimplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to modelclean up the new schedule definitionsautomatically build HTML docs as part of CIsplit out 'make validate' into individual jobsimplify CI setup by using official mathcomp Docker imagesChange definition of completionport existing proofs to ssreflect 1.9.0Copied model/schedule/uni/basic/platform_tdma.v to restructuring/model/schedule/tdma.vcopied everything from model/policy_tdma.vapplied naming convention to behaviormove readme to restructuring rootfix indentation in completion.vAdd sporadic task modeladd task_cost containing definitions related to the WCET modelmove job_cost to job.vMoved behavior to restructuring/behaviorIndentation in factsRenaming in arrival_sequence.vRenaming in schedule.vMoved sequential to scheduleRenaming in arrival_sequence.vEnable continuous integrationDelete redundant busy_interval fileDelete useless assumption in util-lemmamove existing arrival facts to behavior/facts/arrivals.vport scheduler_executes_job_with_earliest_arrivalport only_one_job_scheduled for the ideal scheduleport same_service_implies_scheduled_at_earlier_timesmake all behavioral facts available as rt.behavior.facts.all.Re-organize facts layoutmake processor state instances global and transparentPort lemmas from model/schedule/uni/schedule.vexpand on the relation of service to scheduled_atadd helper lemmas about zero sumsgit: ignore Emacs temp filesack: don't search through generated HTML filesRestructure EDF folderRestructure FP folderGeneralize instantiation of Interference and Interfering Workload for FP and EDF