Devise replacements for 'in the X model' for sequences

UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert

Eclipse Public License 2.0

2 stars 0 forks source link

Devise replacements for 'in the X model' for sequences #56

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

Need to double-check this, but I don't think we should expose (or at least always expose) traces/tick-tock at the sequence level if possible. There should maybe be a more approachable vernacular that tells users what properties they'll get:

traces refinement: 'behaviours', or 'safety'
tick-tock refinement: 'behaviours and deadlocks', or 'safety and liveness' (tick-tock deals with divergence, right?)

MattWindsor91 commented 2 years ago

We currently use 'traces' and 'timed'; this might change, so I'm keeping the issue open for now.