Created
June 9, 2026 15:41
-
-
Save hwayne/1104255d2ddaaf08e6d8b53661b49fc6 to your computer and use it in GitHub Desktop.
How to override a spec operator with itself and something else
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ---- MODULE foo ---- | |
| EXTENDS Integers | |
| VARIABLE x | |
| \* ... | |
| Init == x \in 1..1000 | |
| \* ... | |
| ==== |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Same as the foo spec, expect it forces the initialized value of x to be 1. | |
| Tying FastInit to a quantified import prevents the stack overflow bug we get otherwise | |
| ---- MODULE foo_fast ---- | |
| EXTENDS foo | |
| Overrides == INSTANCE foo | |
| FastInit == Overrides!Init /\ x = 1 | |
| ==== | |
| ---- CONFIG foo_fast ---- | |
| CONSTANT Init <- FastInit | |
| ==== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment