When you run TLC from the command line with the flag option
-dump dot outfile and you check a temporal property, then TLC makes two files,
and `outfile_liveness`. The graphviz for `outfile` is self-descriptive, but I'm having a hard time understanding the `outfile_liveness` graph. First image is a regular state space, second is the liveness dotfile.
1. Why don't all four states appear in the liveness graph?
2. What do the [t] and [f] labels on the edges mean?
3. Does the #number.0# mean anything?