Verifying topological sort

[Sorawee Porncharoenwase <sorawee_por...@xxxxxxxxx>]

Hi,

I wrote a spec verifying that a naive topological sort algorithm (take a node that has indegree = 0 to the output list) is correct for all graphs up to N nodes in Alloy before. Now I am learning TLA+ so I did the same in TLA+. Surprisingly, TLC consumes considerably much more time compared to Alloy (with 6 Nodes, computing initial states alone does not finish in 1 minute. Alloy finishes very quickly).

Is it simply that these kind of problems are not suitable for TLC? I suspect that Alloy's symmetry breaking helps a lot with speed, but SYMMETRY in TLA+ can't be applied because the graph, for example, is not a CONSTANT.