TLC generates the graph of the distinct states. The difference between "states" and "distinct states" is that "states" also includes also counts when two different behaviors reach the same state at some point. That would show up as additional edges, not additional nodes.
To get a dump of the state graph, you can generate a dumpfile by adding -dump path_to_file under TLC Options > Parameters > TLC command line parameters. You can read about other TLC parameters here.
On 10/14/19 2:54 PM, Jam wrote:
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1c80acb0-6811-7d3c-3cb1-11e1be0c6354%40gmail.com.