Yes, that looks very impressive indeed.
Thanks to your posts, I have also found this link which also mentions the sfdp tool:
sdfp accepts dot files as input; so it could be used for Mark’s TLC visualization.
I have just updated ProB so that there is now the option to use sfdp instead of dot for rendering the state space.
It renders much faster for larger state spaces; but I am not really sure that it will be that useful for users yet. Probably one would have to add some custom colouring of the nodes, depending on some user-specified _expression_/property, to help a human make sense of the visualization.
I can publish some of the state space visualizations for TLC models on a website if you are interested (the size of the generated PDFs get larger; so I am not inclined to post them here on the mailing list).