Loading TLC traces

[craft095]

Is it possible to load TLC counter example or simulation as a Spectacle trace? E.g., I got a counter example and want to explore with Spectacle.

[lemmy]

I believe that if TLC would use the same state-normalization and hashing function as Spectacle, then TLC could emit a counterexample using Spectacle-compatible state fingerprints.

[will62794]

The feature has crossed my mind in past.

One thing to consider here is how to ensure that config parameters (e.g. CONSTANT value assignments) are the same between the model that generated the trace and the model currently loaded into Spectacle. We could just assume they match to get started, but this was one subtle aspect of the user experience flow, if we want the tool to actually re-load/re-execute the trace upon loading, as it does currently.