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

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