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.

Excellent, thanks a lot! I'm busy with RTAS'19/CPSWEEK + travel in the coming days, but I'll try to take a close look at it asap. Sergey, could you please also chime in?

CC: @sbozhko

added 1 commit

• b1360834 - Remove time in favor of instant and duration

Compare with previous version

In that case I would also replace duration by time_duration.

Well, that’s getting a bit unwieldy and also somewhat redundant; there is only one kind of “instant” and only one kind of “duration” that we consider. In fact, when editing papers, I typically reduce “time instant” to “instant” precisely because it is redundant; the noun applies only to time (e.g., see: https://www.merriam-webster.com/dictionary/instant).

How about just the following two aliases of nat:

1. time — the type of (time) instants, i.e., the elements of this type are points in time;
2. duration — the type of cumulative time, i.e., the (total) length of a (possibly discontiguous set of) interval(s).

This is concise, unambiguous, and as long as we are consistent in using the right type everywhere, it should result in good readability. What do you think?

I'd rather have instant and duration, but honestly I can live with any of these.

Question: When trying to compile the behavior branch, I'm seeing warnings such as the following:

*** Warning: in file ./behavior/schedule/varspeed.v, 
    required library schedule matches several files in path
    (found schedule.v in behavior/schedule, implementation/uni/basic, implementation/uni/jitter, implementation/uni/susp, implementation/apa, implementation/global/basic, implementation/global/jitter, model/schedule/uni/nonpreemptive, model/schedule/uni, model/schedule/uni/limited, model/schedule/uni/jitter, model/schedule/uni/susp, model/schedule/partitioned, model/schedule/global/basic and model/schedule/global/jitter; used the latter)

Picking "the latter" of the list of potential alternatives seems like the wrong choice. Is this something we need to worry about?

Overall, the merge request looks very good to me. Assuming the compilation issues that I pointed above are not a show stopper, I'd say let's go ahead and merge it and start growing the new structure piece by piece. Thank you Maxime for taking the lead on this!

PS: When merging this, please make sure you squash all the little fixup commits so that the master history doesn't become too littered.

added 1 commit

• fae1f2ce - Added service_implies_scheduled to schedule.v and instances

Compare with previous version

added 1 commit

• abdbde4d - Uniformize Context commands for parameter instances

Compare with previous version

added 2 commits

• 01da447b - 1 commit from branch master
• f51db1cb - Merge branch 'master' into behavior

Compare with previous version

I suggest we merge this now so others can build on it more easily. Any objections?

Ok, I will do that now.

I will open issues with the ongoing discussions if this thread disappears when I merge.

mentioned in issue #39

mentioned in issue #40 (closed)

resolved all discussions

unmarked as a Work In Progress

added 6 commits

• a14e1328 - 1 commit from branch master
• a88f6cd5 - Initial draft of the base for the behavior part of the refactored hierarchy....
• ca16ea34 - fixes
• d5f9070a - Remove time in favor of instant and duration
• 00a0d187 - Added service_implies_scheduled to schedule.v and instances
• 3878b2e5 - Uniformize Context commands for parameter instances

Compare with previous version

added 1 commit

• f210238b - Initial draft of the base for the behavior part of the refactored hierarchy....

Compare with previous version

resolved all discussions

merged

As we've merged this, I'll remove the 'behavior' branch to avoid any possibility for confusion. Please create new merge requests for future patches.