-
|
Hello, I'm trying the TLA+ debugger using the nightly version of the extension. I set a breakpoint and the debugger stops there. Next I'd like to evaluate an expression in the current state. Is this supported? |
Beta Was this translation helpful? Give feedback.
Replies: 3 comments 1 reply
-
|
Unfortunately, SANY lacks incremental parsing, preventing the debugger from supporting ad-hoc (debug) expressions at runtime. While it would be possible to hack something into SANY/TLC, I found adding predefined expressions as "Watch" expressions a good-enough workaround. Any constant-, state-, and action-level formula can be added as a "Watch". The screenshot below shows the
|
Beta Was this translation helpful? Give feedback.
-
|
Thanks! That's helpful. |
Beta Was this translation helpful? Give feedback.
-
|
Today's nightly build comes with (preliminary) support for actual breakpoint expressions: https://youtu.be/rgS0NtoYZZs |
Beta Was this translation helpful? Give feedback.
Unfortunately, SANY lacks incremental parsing, preventing the debugger from supporting ad-hoc (debug) expressions at runtime. While it would be possible to hack something into SANY/TLC, I found adding predefined expressions as "Watch" expressions a good-enough workaround. Any constant-, state-, and action-level formula can be added as a "Watch". The screenshot below shows the
TraceLog,TraceAccepted,TraceAlias, andTraceViewexpressions evaluated as "Watch" expressions.