You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
@@ -55,4 +55,4 @@ You can also see a live demo of the tool and its features in [this presentation]
## Testing
Currently, nearly all testing of the tool is done via conformance testing against TLC. That is, for a given specification, we [generate its reachable state graph using TLC](https://github.com/will62794/tla-web/blob/0060a9bedfbf78c9c6ef1eacf701b13f85048f5e/specs/with_state_graphs/gen_state_graphs.sh) and compare this for equivalence against the reachable state graph generated by the Javascript interpreter. You can see the result of all current tests that are run on [this page](https://will62794.github.io/tla-web/test.html), and the underlying test specs [here](https://github.com/will62794/tla-web/tree/0060a9bedfbf78c9c6ef1eacf701b13f85048f5e/specs/with_state_graphs).
Currently, nearly all testing of the tool is done via conformance testing against TLC. That is, for a given specification, we [generate its reachable state graph using TLC](https://github.com/will62794/spectacle/blob/0060a9bedfbf78c9c6ef1eacf701b13f85048f5e/specs/with_state_graphs/gen_state_graphs.sh) and compare this for equivalence against the reachable state graph generated by the Javascript interpreter. You can see the result of all current tests that are run on [this page](https://will62794.github.io/tla-web/test.html), and the underlying test specs [here](https://github.com/will62794/spectacle/tree/0060a9bedfbf78c9c6ef1eacf701b13f85048f5e/specs/with_state_graphs).
