如何让TLC在生成的dot文件中添加动作名称标签信息？

TLAToolbox默认勾选可视化状态图选项时，生成的dot文件不会包含状态转移的动作标签，你可以通过添加TLC命令行参数来解决这个问题：

• 打开模型的「TLC Options」窗口，切换到「Advanced」标签页
• 在「Additional TLC command line parameters」输入框中，输入参数：-dot_output_edges_with_labels
• 保存配置后重新运行模型检查，完成后生成的dot文件就会把触发转移的动作名称作为边的标签显示

如果需要查看动作的完整表达式（而非仅名称），可以替换为参数：-dot_output_edges_with_full_labels

内容的提问来源于stack exchange，提问作者fwhdzh