----------------------- MODULE CompletionOrderChecksMC -----------------------
EXTENDS RuntimeChecksMC

                                                                        
                                                                           
                                                                              
OverrideCommand(rule, authorized, contradiction, prohibited, body, discharge) ==
    [op |-> "CardOverride", rule |-> rule, authorized |-> authorized,
     directContradiction |-> contradiction, prohibited |-> prohibited,
     body |-> body, discharge |-> discharge]
ScopedOverride ==
    OverrideCommand("CheckpointOrder", TRUE, TRUE, FALSE, TRUE, FALSE)
OrdinaryOverride ==
    OverrideCommand("OtherRule", TRUE, TRUE, FALSE, TRUE, FALSE)
GainCommand == [op |-> "GainResourceUnits", amount |-> 1, player |-> "SideB"]
ZeroPayment ==
    [op |-> "SpendResourceUnits", player |-> "SideB", selected |-> {}, amount |-> 0,
     permittedHosted |-> {}, permissionSources |-> [i \in {} |-> i],
     announced |-> TRUE, restrictionsHold |-> TRUE, mandatoryPrevents |-> FALSE]

                                                                        
                                                                            
                                                                            
                                                                          
                                                                        
SpecificCheckpointPermission(t, c) ==
    t.checkpointDue /\ t.turn = "SideB" /\ c.rule = "CheckpointOrder"
CheckpointTestOverride(before, c, after) ==
    /\ c.body
    /\ after = [before EXCEPT !.event = "CardOverride",
                  !.checkpointDue = IF c.discharge THEN FALSE ELSE @]

InitialCheckpointCommand(n) ==
    CASE n = 1 -> ScopedOverride
      [] n = 2 -> OrdinaryOverride
      [] n = 3 -> GainCommand
      [] n = 4 -> Check
      [] n = 5 -> ZeroPayment
      [] n = 6 -> OrdinaryOverride
      [] n = 7 -> [ScopedOverride EXCEPT !.prohibited = TRUE]
      [] n = 8 -> [ScopedOverride EXCEPT !.authorized = FALSE]
      [] n = 9 -> [ScopedOverride EXCEPT !.directContradiction = FALSE]
      [] n = 10 ->
           [op |-> "GainResourceUnits", amount |-> 1, player |-> "SideB",
            rule |-> "CheckpointOrder", authorized |-> TRUE,
            directContradiction |-> TRUE, prohibited |-> FALSE]
      [] n = 11 -> ScopedOverride
      [] n = 12 -> GainCommand
      [] n = 13 -> ScopedOverride
      [] n = 14 -> [ScopedOverride EXCEPT !.body = FALSE]
      [] n = 15 -> [ScopedOverride EXCEPT !.discharge = TRUE]
      [] n = 16 -> [OrdinaryOverride EXCEPT !.prohibited = TRUE]
      [] OTHER -> OrdinaryOverride

CheckpointTestCommands(t) ==
    CASE t.event = "Initial" -> {InitialCheckpointCommand(t.testCase)}
      [] t.testCase = 1 /\ t.event = "CardOverride" -> {Check}
      [] t.testCase = 1 /\ t.event = "Checkpoint" -> {GainCommand}
      [] t.testCase = 5 /\ t.event = "PayResourceUnits" ->
           {GainCommand, OrdinaryOverride, Check}
      [] t.testCase = 5 /\ t.event = "Checkpoint" -> {GainCommand}
      [] t.testCase = 15 /\ t.event = "CardOverride" -> {GainCommand}
      [] OTHER -> {}

CheckpointStart(n) ==
    Put([Empty EXCEPT !.checkpointDue = n \notin {5,6,12,16},
                     !.outcome = IF n = 11 THEN "SideA" ELSE "Playing",
                     !.turn = IF n = 13 THEN "SideA" ELSE "SideB"],
        "testCase", n)
InitiallyEnabled == {1,4,5,6,12,15}
CheckpointLimit(n) == IF n \in {1,5} THEN 3 ELSE IF n = 15 THEN 2 ELSE 1
CheckpointInit == /\ caseNo \in 1..16 /\ pc = 0 /\ s = CheckpointStart(caseNo)
CheckpointProgress ==
    /\ pc < CheckpointLimit(caseNo)
    /\ IF caseNo \in InitiallyEnabled
       THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ pc = 0 /\ ~ENABLED Next
            /\ pc' = 1 /\ UNCHANGED <<s, caseNo>>
CheckpointNext ==
    CheckpointProgress \/
    (pc = CheckpointLimit(caseNo) /\ UNCHANGED mcvars)
CheckpointSpec ==
    CheckpointInit /\ [][CheckpointNext]_mcvars /\ WF_mcvars(CheckpointProgress)
CheckpointCompleted == <>(pc = CheckpointLimit(caseNo))

CheckpointAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in InitiallyEnabled))
    /\ (caseNo \notin InitiallyEnabled => s = CheckpointStart(caseNo))
    /\ (caseNo = 1 /\ pc = 1 =>
         s.event = "CardOverride" /\ s.checkpointDue /\ ResourceUnits(s, "SideB") = 0)
    /\ (caseNo = 1 /\ pc = 2 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 1 /\ pc = 3 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 4 /\ pc = 1 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 1 => s.event = "PayResourceUnits" /\ s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 2 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 3 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 6 /\ pc = 1 => s.event = "CardOverride" /\ ~s.checkpointDue)
    /\ (caseNo = 12 /\ pc = 1 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 15 /\ pc = 1 => s.event = "CardOverride" /\ ~s.checkpointDue)
    /\ (caseNo = 15 /\ pc = 2 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
=============================================================================