Add support to evaluate trace expression

[lemmy]

https://github.com/tlaplus/tlaplus/issues/485 https://github.com/tlaplus/tlaplus/issues/393

[will62794]

@lemmy Is the support for this in TLC complete?

[lemmy]

http://tla.msr-inria.inria.fr/kuppe/vscode/ hosts builds of vscode-tlaplus with the most recent nightly build of TLC. If one adds -generateSpecTE as a TLC command-line parameter in vscode-tlaplus, TLC will create SpecTE.tla after model checking that has boilerplate (at the bottom of SpecTE.tla) to define trace expressions. One then has TLC check SpecTE.tla to evaluate the expression.

I consider this feature sufficiently complete to suggest somebody prototypes an integration into vscode-tlaplus.

[will62794]

@lemmy What is the intended usage of the command line trace explorer functionality? There seem to be a few different ways to invoke it i.e.

java -cp tla2tools.jar tlc2.TraceExplorer -traceExpressions -expressionsFile=expr.txt -overwrite spec

or

java -cp tla2tools.jar tlc2.TLC -generateSpecTE -config spec.cfg spec.tla

For usage in VS Code extension I would imagine that we would be running the trace explorer after we have already generated TLC output from a model checking run that produced an error trace. So, it seems the first usage would be the one we want to use? I'm not sure exactly what you had in mind though when designing the command line interface.

[lemmy]

https://www.youtube.com/watch?v=pTN3nHvSm84

/cc @quaeler