what material did you use for learning TLA+? Since you state your problem in terms of programming notation, it is not so obvious what parts of your problem you have already expressed in TLA+, and indeed what your objective is.
I am assuming that the graph is a constant, represented by the edge relation.
ASSUME edge \subseteq Int \X Int
It looks to me that you wish to define cycles in your graph. Paths can be represented as sequences of integers, so you could define something like
/\ \A n \in 1 .. Len(p)-1 : << p[n], p[n+1] >> \in edge
/\ << p[Len(p)], p >> \in edge
It is not clear to me what you use the array for.
Hope this gives you some ideas.