TLC throw an error while verifying Raft TLA+ spec

[kikimo]

While checking the Raft TLA+ spec in this repo, TLC throw an error reporting that:

Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply tuple
<<>>
to integer 1 which is out of domain.
Error: The behavior up to this point is:
...

The TLA+ code triggered this error was:

tla-plus/Raft/Raft.tla

Lines 354 to 361 in 8ae629d

	/\ LET index == m.mprevLogIndex + 1
	IN \/ \* already done with request
	/\ \/ m.mentries = << >>
	\/ /\ Len(log[i]) >= index
	/\ log[i][index].term = m.mentries[1].term
	\* This could make our commitIndex decrease (for
	\* example if we process an old, duplicated request),
	\* but that doesn't really affect anything.

The main problem is that TLC might still execute /\ log[i][index].term = m.mentries[1].term at line 358 even though m.mentries = << >> at line 356 is true(and that's how TLC evaluate an TLA+ expression). We might apply the patch below to fix the error:

 /\ LET index == m.mprevLogIndex + 1 
    IN \/ \* already done with request 
           /\ \/ m.mentries = << >> 
              \/ /\ Len(log[i]) >= index 
                 /\ m.mentries # << >>
                 /\ log[i][index].term = m.mentries[1].term 

PS: Is this repo still maintained? It seems that the TLA+ spec in this repo and the Raft implementation in TiKV have diverge quiet a lot!