Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add GUI element to reevaluate ALIAS #282

Open
Tracked by #342
JoshuaRowePhantom opened this issue Apr 17, 2023 · 1 comment
Open
Tracked by #342

Add GUI element to reevaluate ALIAS #282

JoshuaRowePhantom opened this issue Apr 17, 2023 · 1 comment
Labels
enhancement New feature or request

Comments

@JoshuaRowePhantom
Copy link
Contributor

JoshuaRowePhantom commented Apr 17, 2023

Problem:
When inspecting an error trace, it is frequently useful to update the ALIAS evaluation. The only GUI elements I see to do this are the "check again" button in the results pane. Having an easy-to-find button that just reevaluates ALIAS on the error trace would shorten the cycle of error exploration.
Compare this with the toolbox's error exploration: https://learntla.com/topics/toolbox.html#trace-explorer
Check alias definition: https://learntla.com/topics/cli.html#config-format

@lemmy lemmy added the enhancement New feature or request label Apr 17, 2023
@lemmy lemmy transferred this issue from tlaplus/tlaplus Apr 17, 2023
@lemmy lemmy changed the title Visual Studio Code: Add GUI element to reevaluate ALIAS Add GUI element to reevaluate ALIAS Apr 17, 2023
@lemmy
Copy link
Member

lemmy commented Apr 17, 2023

Workaround:

  • Have TLC generate a trace exploration spec (MySpec_TTrace_$timestamp.tla) by passing -generateSpecTE (not passing -noTE)
  • Manually add you Alias to the trace exploration spec
  • Repeatedly check the trace exploration spec

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Development

No branches or pull requests

2 participants