diff --git a/README.md b/README.md index 46e96b4..82da280 100644 --- a/README.md +++ b/README.md @@ -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).