TLA + Graph Explorer

该应用程序通过解析由TLA +规范生成的点文件，然后具有可视化表示更容易理解并通过可访问状态。

编写该应用程序以支持大点文件，不会将整个文件加载到内存中。这是通过在块中读取文件并仅存储文件中的节点的位置来实现。在我的实验中保存节点位置的结构需要左右的点文件大小的1/10。

表示状态的默认方法显示了漂亮的打印版本，如例1所示。

可以通过更改文件tla-state.js中的函数绘制窗口来个性化状态的表示。在示例2中示出了个性化状态表示的示例，并且源代码处于示例/ ceph- 3mon中。

为了帮助创建一个状态的个性化表示，应用程序附带一个解析器，将TLA +状态解析为JavaScript结构。解析器定义是在文件夹中，解析器expr-parser，解析器的示例用法（函数parsevars）可以在示例/ ceph-consensus-3mon中找到。