UoY-RoboStar / robocert-textual

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

Single-action deadlines? #44

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

In UML2.5.1, it is possible to put a DurationConstraint on one element. This syntactically appears, for instance, as the label of a message:

op Foo()    {0..5}
----------------->

In robocert-sequences, DeadlineSteps implicitly box a whole subsequence, meaning that they can be used to deadline one element, but always appear as a double-arrow between the top and bottom. (Once we get to n-ary sequences (#32), we'll likely need to change this to a more UML-faithful situation where we tag two actions as being endpoints of a duration, and in the semantics we'll generate some sort of parallel checker process. But I digress.)

From a syntactic point of view, it maybe makes sense to have single-action deadlines. One issue is that this notation gives the suggestion that it's op Foo() that is itself taking up to 5 time units; in fact, it's that it might take up to 5 time units for op Foo() to happen (and when it does, it does so instantaneously). Hmm.

From a semantic point of view, there probably isn't anything other than metamodel differences here for 2-actor sequences.