Skip to content

Instantly share code, notes, and snippets.

@JeremyLWright
Created January 12, 2022 18:00
Show Gist options
  • Save JeremyLWright/151d3b03b81fa24f2274895fa520ee66 to your computer and use it in GitHub Desktop.
Save JeremyLWright/151d3b03b81fa24f2274895fa520ee66 to your computer and use it in GitHub Desktop.
TLA+ Specification of the a scene in the movie "A Brilliant Young Mind"
------------------------ MODULE ABrilliantYoungMind ------------------------
EXTENDS TLC, Sequences, Naturals
CONSTANTS NumCards
ASSUME NumCards > 1
VARIABLES Game
vars == <<Game>>
Max(xs) == CHOOSE x \in xs :
\A y \in xs: y <= x
Init == \E size \in 1..NumCards :
Game = [i \in 1..size |-> "D"]
FlipCard(i) == IF Game[i] = "U" THEN "D" ELSE "U"
MakeMove == \E i \in DOMAIN Game :
/\ Game[i] = "D"
/\ Game' = IF i = Max(DOMAIN Game) THEN [Game EXCEPT ![i] = "U"]
ELSE [Game EXCEPT ![i] = "U",
![i+1] = FlipCard(i+1)]
AllCardsFaceUp == \A i \in DOMAIN Game : Game[i] = "U"
GameFinished ==
/\ AllCardsFaceUp
/\ UNCHANGED Game
Next ==
\/ AllCardsFaceUp /\ GameFinished
\/ MakeMove
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
EventuallyAllFaceUp == <>[]AllCardsFaceUp
TypeOK == \A i \in DOMAIN Game : Game[i] \in {"D", "U"}
=============================================================================
\* Modification History
\* Last modified Wed Jan 12 09:23:19 MST 2022 by jeremy
\* Created Wed Jan 12 08:53:58 MST 2022 by jeremy
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment