Tla+ web explorer

src/SUMMARY.md

@@ -33,6 +33,7 @@
     - [Community Modules](./using/community-modules.md)
     - [Debugger](./using/debugger.md)
     - [Generating stage graphs](./using/generating-state-graphs.md)
+    - [TLA+ Web Explorer](./using/tla-web-explorer.md)
     - [CI for your specifications](./using/ci-for-specs.md)
     - [Known limitations](./using/limitations.md)
 - [TLA+ Community: what to do when you're stuck](community.md)

src/using/tla-web-explorer.md

@@ -0,0 +1,9 @@
+# TLA+ Web Explorer
+[Homepage](https://will62794.github.io/tla-web/#!/home?specpath=.%2Fspecs%2FTwoPhase.tla) and the source code is hosted on [GitHub](https://github.com/will62794/tla-web).
+
+The current version of the tool utilizes the TLA+ tree-sitter grammar for parsing TLA+ specs and implements a TLA+ interpreter/executor on top of this in Javascript. This allows the tool to interpret specs natively in the browser, without relying on an external language server. The Javascript interpreter is likely much slower than TLC, but efficient model checking isn't currently a goal of the tool.
+
+Watch the presentation:
+
+<iframe width="1333" height="485" src="https://www.youtube.com/embed/kSSWmxQLvmw" title="TLA+ Conf - William Schultz - Towards Interactive Formal Specs" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen></iframe>
+