UoY-RoboStar / robocert-textual

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

Scope explicit edges to/validate against lifelines #91

Open MattWindsor91 opened 2 years ago

MattWindsor91 commented 2 years ago

Further to #90, we need to make sure that any to and from on ExplicitEdges can only pick up actors that are in the parent sequence's lifetime set. This won't be automatic, so I'll need to add this scoping restriction explicitly.

MattWindsor91 commented 2 years ago

Actually, this is more intricate than I'd expect: not all ExplicitEdges have parent sequences. Instead, what I think we need is a validation that looks something like: any edge that appears in a sequence must have its resolved to and from appear in the lifelines.