Errors occurred during the build. Errors running builder 'TLA+ Syntax Parser' on ...

Start at tla2sany.semantic.Generator.processAction in Generator.java:3853 and follow the semantic-analysis path shown in the stack trace through SANY.frontEndSemanticAnalysis. Use the provided GithubIssue5xx specification, especially the malformed final line, as the reproducer; done means the invalid input is handled without an ArrayIndexOutOfBoundsException during the TLA+ Toolbox build.

--------------------- MODULE GithubIssue5xx ---------------------
EXTENDS Naturals, FiniteSets, Sequences

Max(S) ==
  CHOOSE max \in S : \A o \in (S \ {max}) : max >= o

foo(a, b) == 
  IF a = b THEN 1 ELSE IF a > b THEN 0 ELSE 2

Handled(f1, f2) ==
   LET F[n \in DOMAIN f1] == 
          IF n = 1
          THEN foo(f1[n], f2[n])
          ELSE F[n-1] + foo(f1[n], f2[n])
   IN F[Max(DOMAIN f1)]

CONSTANTS Load, Server, Request, Capacity(_), Recover(_)

ASSUME Server \subseteq (Nat \ {0})
ASSUME Load \subseteq Nat
ASSUME Request \subseteq Nat

VARIABLE loads,
         requests
vars == << loads, requests>>
         
TypeOk ==
  /\ loads \in [ Server -> Nat ]
  /\ requests \in Nat

Init ==
  /\ loads \in [ Server -> Load ]
  /\ requests \in Request

Handle ==
     /\ requests > 0
     /\ \E f \in [ Server -> Load ]:
            /\ \A s \in Server:
                 f[s] \in (loads[s](* - 1*))..(loads[s] + 1)
            /\ Handled(loads, f) <= requests
            /\ loads' = f
            /\ \E r \in Request: 
                 requests' = 
                      Max({0, requests + r - Handled(loads, f)} ) 

Idle ==
     /\ requests = 0
     /\ loads' = [ s \in Server |-> loads[s] ]
     /\ requests' \in Request

Next ==
  \/ Idle
  \/ Handle

Spec ==
  Init /\ [][Next]_vars /\ WF_vars(Next)
  
OperatingNormally ==
  /\ (requests < 2 * Max(Request))

R ==
  /\ requests' > requests
  /\ loads' \in [ Server -> Nat ]

EventuallyOperatingNormally ==
  /\ <>[](loads \notin [ Server -> {Max(Load)}])
  /\ <>[]<<>>_vars  
  =====

Note that the last line (before the end of module marker) is incorrect and causing the exception.

java.lang.ArrayIndexOutOfBoundsException: Index 3 out of bounds for length 3
	at tla2sany.semantic.Generator.processAction(Generator.java:3853)
	at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3204)
	at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
	at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:2877)
	at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
	at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:2877)
	at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
	at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3167)
	at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
	at tla2sany.semantic.Generator.processOperator(Generator.java:2436)
	at tla2sany.semantic.Generator.generateModule(Generator.java:2032)
	at tla2sany.semantic.Generator.generate(Generator.java:1973)
	at tla2sany.drivers.SANY.frontEndSemanticAnalysis(SANY.java:313)
	at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:162)
	at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:83)
	at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:56)
	at org.lamport.tla.toolbox.spec.parser.SpecificationParserLauncher.parseSpecification(SpecificationParserLauncher.java:38)
	at org.lamport.tla.toolbox.spec.nature.ParserHelper$2.run(ParserHelper.java:68)
	at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2292)
	at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2312)
	at org.lamport.tla.toolbox.spec.nature.ParserHelper.rebuildSpec(ParserHelper.java:73)
	at org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.build(TLAParsingBuilder.java:95)
	at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:832)
	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
	at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:220)
	at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:263)
	at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:316)
	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
	at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:319)
	at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:371)
	at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:392)
	at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:154)
	at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:244)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)