Issue1133

[roeger]

This is a major revision of the translator code for finding invariants, also fixing a bug reported on discord. See issue1133 for details.

[roeger]

Let me suggest a commit message for merging this. @salome-eriksson, is the following clear enough?

[issue1133] Fix bug in invariant synthesis and revise its implementation.

It was possible that an unbalanced action passed the balance check. This was a conceptual gap in the original algorithm for which we had to significantly revise the invariant synthesis. We used the opportunity to revise wide parts of its implementation, restructuring and renaming the different components to improve clarity.

[salome-eriksson]

Let me suggest a commit message for merging this. @salome-eriksson, is the following clear enough?

[issue1133] Fix bug in invariant synthesis and revise its implementation.

It was possible that an unbalanced action passed the balance check. This was a conceptual gap in the original algorithm for which we had to significantly revise the invariant synthesis. We used the opportunity to revise wide parts of its implementation, restructuring and renaming the different components to improve clarity.

Yes that looks good to me :)