William Schultz

> Looking at a trace of that spec makes me curious—does Spectacle support ALIASES? Not directly, but you can sort of emulate it with hidden variables + trace expressions. Aliases...

You should now be able to [override definitions](https://will62794.github.io/spectacle/#!/home?specpath=https%3A%2F%2Fgist.githubusercontent.com%2Fwill62794%2F50e25a51f981f4370418d3bee860546d%2Fraw%2Fab76ea1caa2c34ae45ffe37bdc125946162db2df%2Fqspinlock.tla&initPred=Init&nextPred=Next&constants%5BCPUS%5D=%7Bp1%2Cp2%2Cp3%7D&constants%5BMAX_NODES%5D=1&constants%5BPENDING_LOOPS%5D=1&constants%5BdefaultInitValue%5D=defaultInitValue&defOverrides%5BNoCPU%5D=%22Nil%22&trace=62d2c484) in a manner to support loading of this spec's initial states.

@Vanlightly I just pushed a fix (1346b7f) to handle an issue where `CASE` statements were not evaluating variable assignments correctly. See if this addresses some of the issues you were...

@ahelwer If it might be of any help, I wrote a [small Python script](https://github.com/will62794/endive/blob/8b6f2abd1988eeb308f965813635e9871f253e2d/checkproofs.py) a bit ago to parse the command line output of the TLAPS proof manager into a...

@helwer No, the script is not published, but feel free to extend/modify it and publish it there if you want.

Eventually the interface should handle this case better, but I just pushed a [small change](https://github.com/will62794/tla-web/commit/9458efca302f102751dee150b2cac3bf67bbd20b) that may help you work around the confusion in the current tool. The change allows...