Lattice synthesis

[blexim]

Observation: when doing safety invariant generation, we can tell if a candidate is too weak (i.e. it fails the inductiveness check) or too strong (it fails initiation or safety). This induces a lattice of candidates & gives us an heuristic for walking the lattice.

Use this to build a synthesis module.