UoY-RoboStar / robocert-textual

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

Accept sequences as CSP processes #36

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

A sequence diagram should be visible as a CSP process (perhaps after fixing all of its constants), and able to participate in CSP refinement questions. Why? The main reason is to check that a sequence diagram appropriately captures a CSP process, which is useful both for debugging the diagram semantics and also for transitioning from CSP to sequences.

Related to #35 (which is tracking targets as CSP processes; a consequence of both going through is that sequence assertions are effectively sugar over CSP assertions for now!), and #34 (which is tracking implementing process-bound CSP fragments).