Remove implicit trace partiality

UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert

Eclipse Public License 2.0

2 stars 0 forks source link

Remove implicit trace partiality #96

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 2 years ago

After discussion with Ana today, I've decided that it doesn't in fact make sense for traces to be implicitly partial (eg finish with ; TCHAOS(Events)). This behaviour is easily reintroduced using an anything until end gap, and makes existential properties as well as properties over terminating robots confusing. It is also non-canonical UML semantics.

MattWindsor91 commented 2 years ago

This was fixed quite some time ago :)