Skip to content

Define completion sequences

Pierre Roux requested to merge proux/rt-proofs:completion_sequence into master

Completion sequences are defined (as arrival sequences) from an arrival sequence and a schedule.

This follows the suggestion from @bbb in https://gitlab.mpi-sws.org/RT-PROOFS/project-administration/-/issues/23#note_55292

This may already exist in a formalization of CPA, ccing @mlesourd and @sophie who may have an opinion here.

Edited by Pierre Roux

Merge request reports