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

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

Hi,

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.

Greetings,

Michael

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:
> http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples

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.

-- 

FL