Add Request Bound Functions

So that we can link them to arrival curves of Network Calculus in NCCoq as discussed in https://gitlab.mpi-sws.org/RT-PROOFS/project-administration/-/issues/23

The link with Network Calculus arrival curves can be found here : https://gitlab.mpi-sws.org/proux/nc-coq/-/tree/prosa-link/link

Hello Pierre, I am Marco. Nice to meet you, and thanks for the MR!

Hi Pierre, indeed thanks a lot for the MR, looks very good!

I wonder if these definitions will allow us to simplify / improve some parts of the abstract RTA proof — @sbozhko?

Specifically, do you think we can phrase abstract RTA generically in terms of this definition, and then just connect the existing concrete instantiations by having a default RBF instance for tasks with arrival curves and a task_cost parameter?

resolved all threads

added 3 commits

• 50dd4f5b...cff4e0d4 - 2 commits from branch RT-PROOFS:master
• a5927468 - Add Request Bound Functions

Compare with previous version

Thanks for your comments!

approved this merge request

approved this merge request

merged