How to Run?

[a1424360017]

I create and run TLA models in the usual way.

But get "Attempted to compute the number of elements in the overridden value Nat.While working on the initial state" when run ParallelRaftSE spec

Is there a problem with “leaderLog = [i \in Term |-> [j \in Index |-> <<-1,Nil,FALSE>>]]” in Init ,Because "Term == Nat"?