UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert
Eclipse Public License 2.0
2 stars 0 forks source link

Bind durations to an actor #103

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 2 years ago

Currently, duration constraints have no specified lifeline. This is not a problem in component diagrams, as there is only one lifeline, but generalising to multiple lifelines means that it is now unclear as to which lifeline(s) are constrained by a duration constraint.

For now, my preference is to change duration constraints so that they take an actor, and only lift into a deadline the part of the subsequence that is on that lifeline. So, assuming the syntax change on #51, we would have:

taking at most N units on A:
  <subsequence>

This also makes the graphical notation closer to UML, as there will now be a clear lifeline to which the |<->| should attach.

Future generalisations might make it so that we can bind to some sort of synchronised block. (The issue is that we need to make sure that once the deadline occurs, it timelocks all of the lifelines) I'm generally not very sure about synchronisation across lifelines yet so we'll see.

MattWindsor91 commented 2 years ago

Done ages ago!