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

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


FYI: I have added a few more examples to the web page (http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples).
I agree and I also believe the projection diagrams to be the most useful; they have already enabled me to uncover various issues with several models.
But sometimes the visualization of the full state space can yield surprising results; see, e.g., the visualization of the Hanoi model.


On 20 Dec 2015, at 13:08, fl wrote:

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

Hi, Michael,

the first one is difficult to interpret. And I don't know how people could take advantage of it (1). The second one
on the contrary can be useful.

(1) But maybe it is due to the idiosyncrasy of the alternating bit protocol. A more traditional algorithm would be
easier to make sense of it.