Skip to content

Restructure analysis folder

As discussed at the Paris RT-PROOFS meeting:

  • one definitions folder for analysis-related definitions like schedulability, busy-window, etc.
  • main results should appear at the top level, without clutter
  • basic_facts about trace semantics ➔ facts.behavior
  • similarly, introduce facts.model to collect facts about model entities and definitions
  • facts about busy windows can go into facts.busy_window etc.

This is blocking #51 (closed) and is awaiting the conclusion of !54 (merged) to avoid further rebasing pain.

Ideally, !45 (merged) should also make it in before this is done to avoid creating more rebasing friction in the aRTA porting effort, too.

CC: @mlesourd @sbozhko @sophie

Edited by Björn Brandenburg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information