1. 18 Mar, 2021 1 commit
  2. 11 Mar, 2021 1 commit
    • LailaElbeheiry's avatar
      add proof of equivalence of EDF definitions · 271464a5
      LailaElbeheiry authored
      This commit connects the two ways with which one can specify that a
      schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
      and the `respects_policy_at_preemption_point` with the EDF priority
      policy predicate. We connect these two definitions by showing that
      they're equivalent. We then restate the optimality proof of EDF
      schedules using the proven equivalence.
      271464a5
  3. 08 Mar, 2021 3 commits
  4. 01 Mar, 2021 2 commits
  5. 29 Jan, 2021 1 commit
  6. 02 Jan, 2021 1 commit
  7. 11 Dec, 2020 2 commits
  8. 25 Sep, 2020 1 commit
  9. 23 Sep, 2020 1 commit
    • Sergey Bozhko's avatar
      Add [arrives_in] to [sequential_tasks] definition · 33a48458
      Sergey Bozhko authored
      Note that the prior definition of [sequential_tasks]
      did not differentiate between a job coming from the
      arrival sequence and any other job. However, all
      computable properties (such as [job_respects_task_rtc,
      valid_preemption_model, arrivals_have_valid_job_costs,
      all_deadlines_of_arrivals_met]) are stated exclusively
      for jobs from the arrival sequence. In order to make
      the definition of [sequential_tasks] compatible with
      computable properties, we add preconditions
      [arrives_in arr_seq j1] and [arrives_in arr_seq j2].
      33a48458
  10. 22 Sep, 2020 7 commits
  11. 09 Sep, 2020 4 commits
  12. 28 Aug, 2020 2 commits
  13. 27 Aug, 2020 1 commit
  14. 10 Aug, 2020 4 commits
  15. 06 Aug, 2020 1 commit
  16. 05 Aug, 2020 6 commits
  17. 04 Aug, 2020 2 commits