[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Sorawee Porncharoenwase <sorawee_por...@xxxxxxxxx>*Date*: Tue, 19 Dec 2017 00:46:17 -0800 (PST)

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.

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.

**Follow-Ups**:**Re: Verifying topological sort***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Could I estimate how long will it take for TLC to finish checking a model?** - Next by Date:
**Re: Verifying topological sort** - Previous by thread:
**Re: [tlaplus] Could I estimate how long will it take for TLC to finish checking a model?** - Next by thread:
**Re: Verifying topological sort** - Index(es):