Translation of BEEM benchmark
The BEEM benchmark is a popular benchmark for explicit model-checker.
It supports atomic transitions with multiples effects. Thus, an automatic
translation of these models is not trivial.
Indeed, we can opt for the following strategy:
- if this transition uses only local variables: no problem we can just split that into multiple transitions
- otherwise build an extern fonction that regroup all the effect of this transition (even thought it can be tricky with local variables) in a function and consider this function as blackbox.
This strategy will fail since even if the model (including blackboxing) will be correct, the go file will not be be. Indeed, the multiples effects of the original BEEM model will now be considered as multiple ones which is really problematic.
How can we solve that?