Base for the behavior part of refactored PROSA.
This is an initial draft of behavior part of the refactored hierarchy containing (parts of) the definitions for arrival sequences and schedules.
I have tried to implement most of the proposed improvements discussed in Braunschweig:
- Removal of spurious toplevel modules
- Changing "Require Import" into "Require Export" as discussed in #37 (closed)
- Generic definition of schedule based on processor state as discussed in #34 (closed)
- Several instances of processor state including the existing ones (basic, multi)
- Use of typeclasses for job-related parameters as discussed in #35 (closed)
I will add comments pointing to specific parts of the code in the comments below.
Feedback would be appreciated as the choices we make here are going to have consequences when porting the rest of the developments.
Edited by Maxime Lesourd