UoY-RoboStar / robocert-textual

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

Missing tau-prioritisations in CorePropertyGenerator #131

Open MattWindsor91 opened 2 years ago

MattWindsor91 commented 2 years ago

Looking at the untimed and timed generators, it would seem that each rule (deadlock, timelock, divergence, determinism, termination) gets tau-prioritised. Currently, termination is missing this. The easiest way to fix this would be to lift the csp.tauPrioritiseTock to the top level.