This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa are changed to comply with the “new style”, they are placed here.
The behavior directory collects all definitions and basic properties of system behavior (i.e., trace-based semantics).
The model directory collects all definitions and basic properties of system models (e.g., sporadic tasks, arrival curves, scheduling policies etc.)
# Remarks
We have chosen and applied some renaming rules for sections and definitions, cf. arrival_sequence.v and sporadic.v. Basically, we try to consistenly use `Valid*` , `*Properties` for section names about a concept `*` and `respects_*`, `valid_*` for definitions about a system model `*`.
The behavior directory/module collects all definitions and theories about system behavior (i.e., trace-based semantics).
Any aspects related to system *modeling* (e.g., sporadic tasks, arrival curves, etc.) do *not* belong here and should go into the *model* directory/module instead.
This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa a changed to comply with the “new style”, they are placed here.
