I read in the
Current and Future Tools for Interactive TLA+ article that TLC can make a graph of actions that enable other actions, but it's not documented or integrated into the GUI. I'm wondering if anyone has more info on this? A code example would be most welcome.