search

UoY-RoboStar / robocert-textual

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

Non-local choice #105

Open MattWindsor91 opened 2 years ago

MattWindsor91 commented 2 years ago

In alternative blocks, we need a strategy for handling the issue of multiple lifelines choosing different alternatives.

When guards are evaluated in multiple lifelines at once, it is possible (if there is a race condition, for instance) for there to be a difference in how those guards evaluate, and this can exacerbate the situation.

Since in FDR we are model checking, this would result in states in the process that are difficult to explain to users.

I believe Lima et al.'s work has mitigation for this, but it might introduce undue synchronisation? I need to look.

We need to put some example in the testbed for this.

MattWindsor91 commented 2 years ago

Punting back to a future milestone because the current semantics is 'good enough' for v0.1.