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