Skip to content

Instantly share code, notes, and snippets.

@thpani
Created April 27, 2022 10:14
Show Gist options
  • Save thpani/a629c9a01530160f7981a6f51becebb1 to your computer and use it in GitHub Desktop.
Save thpani/a629c9a01530160f7981a6f51becebb1 to your computer and use it in GitHub Desktop.
------ MODULE Oracle --------
VARIABLES
\* @type: Set((Bool -> Int));
witness,
\* @type: Bool;
found
Init ==
/\ witness \in {[BOOLEAN -> {222521218, 0}], [{TRUE} -> {2147483647}]}
/\ found \in BOOLEAN
Next ==
UNCHANGED <<witness, found>>
NotFound ==
~found
======================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment