Re: [tlaplus] Re: How to read the graph generated by TLC? Is there a way to specify its location?

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

Hi Frederic,

I tried one TLA+ example, the MCAlternatingBit protocol example in the TLC distribution.

I have put a png of the visualization for about 2000 states and 11,000 transitions at this wiki page:

 http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples

I can send you the full PDF (1.7 MB); rendering was fast.

Orange nodes satisfy the predicate RBit=1.

Greetings,

Michael

On 18 Dec 2015, at 13:59, fl <freder...@xxxxxxxxxxx> wrote:

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).