TLA+ Specification of the a scene in the movie "A Brilliant Young Mind"

ABrilliantYoungMind.tla

------------------------ 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