I have a model with an `Init` and `Next` formula.
While going through an error trace, I would like to see a list of all possible next steps it could transition to.
I assume that I could add some _expression_ based on `Next`, that will provide a set of all solutions for `var'`,
but I have no idea of how to express that?
Thanks,
Andreas