Bounded-scope generators

Apalache Research
1

Apalache currently supports value generators to restrict the scope of very large data structures.

Read the motivation for value generators and a proposal for alternative syntax/implementation in the Github discussion.