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

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

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:
I can send you the full PDF (1.7 MB); rendering was fast.
Orange nodes satisfy the predicate RBit=1.


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