Add pointer to explore the spec interactively with tla-web

Related: will62794/spectacle#26

simple-model/README.md

@@ -14,7 +14,7 @@ PRs increasing this set with new possibilities, including potentially failing ca
 If you need to consider network delay in addition to Cosmos DB's base semantics (although it may not make a meaningful difference in most cases, and may complicate your model), `CosmosDBClient.tla` contains definitions that can be used to do this.
 
 For examples of how to use the specifications here in order to model a specific situation, the files `show*.tla` contain variations of a model of the same [outage at Microsoft Azure](https://portal.microsofticm.com/imp/v3/incidents/postmortem/521677).
-The spec [show521677simple.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simple.tla) models the outage *above* the network layer, while [show521677.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677.tla) is more detailed and includes network communication.  Similarly, two PlusCal specifications model the outage at the same two levels of abstraction ([show521677simplePCal](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simplePCal.tla) and [show521677PCal.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677PCal.tla)).
+The spec [show521677simple.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simple.tla) models the outage *above* the network layer, while [show521677.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677.tla) is more detailed and includes network communication (you can [interactively create and explore traces of the spec](https://will62794.github.io/spectacle/#!/home?specpath=https%3A%2F%2Fraw.githubusercontent.com%2Ftlaplus%2Fazure-cosmos-tla%2Frefs%2Fheads%2Fmaster%2Fsimple-model%2Fshow521677.tla&constants%5BStrongConsistency%5D=%22Strong%22&constants%5BBoundedStaleness%5D=%22Bounded%22&constants%5BSessionConsistency%5D=%22SessionCon%22&constants%5BConsistentPrefix%5D=%22ConPre%22&constants%5BEventualConsistency%5D=%22Event%22&constants%5BVersionBound%5D=1&constants%5BStalenessBound%5D=1) with tla-web).  Similarly, two PlusCal specifications model the outage at the same two levels of abstraction ([show521677simplePCal](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simplePCal.tla) and [show521677PCal.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677PCal.tla)).
 Model checking each spec with TLC will provide a counter-example which represents the root cause of the relevant outage.
 
 ## Analysis-specific files