| Hello, 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. EXTENDS Integer CONSTANT edge 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 IsCycle(p) == /\ \A n \in 1 .. Len(p)-1 : << p[n], p[n+1] >> \in edge /\ << p[Len(p)], p[1] >> \in edge It is not clear to me what you use the array for. Hope this gives you some ideas. Best regards, Stephan
|