tlaplus-graph-explorer:一个静态Web应用程序，用于浏览TLA +状态图并对其进行动画处理

TLA +图形浏览器 这是一个静态Web应用程序，用于浏览TLA +状态图并对其进行动画处理。 该应用程序的工作方式是解析TLA +规范生成的点文件，然后使用可视化表示形式更轻松地理解并经历可达状态。 编写该应用程序是为了支持大点文件，而不是将整个文件加载到内存中。 这是通过分块读取文件并将节点的位置仅存储在文件中来实现的。 在我的实验中，用于保存节点位置的结构大约占点文件大小的1/10。 例子 示例1-传教士和食人族 规格： : 。 示例2-Ceph共识算法 规格： ： 。 如何使用 该应用程序位于文件夹。 表示状态的默认方式是显示漂亮的印刷版本，如示例1所示。 可以通过更改文件函数来个性化状态的表示。 示例2中显示了个性化状态表示的示例，源代码在。 为了帮助创建状态的个性化表示，该应用程序附带了一个解析器，该解析器将tla +状态解析为JavaScript结构。 解析