Variables not working as Watch expression

[nano-o]

Variables not working as Watch expression

[nano-o]

Sorry I spoke too fast. It does work for defined parameterless operators. If I define Votep1 == vote[p1] in my spec, then watching Votep1 works.

[lemmy]

Indeed, variables don't work as watch expressions. I was assuming that users would prefer to see the variables in the debugger's "View" section. Can you explain why that's not satisfactory? Please try the next nightly that includes tlaplus/tlaplus@503a1e4

[nano-o]

Thanks! Now it works for variables but seemingly not anything else (this is strictly better than before, where didn't work at all). Let's say I add the watch expression vote[p1], where p1 is a model value, then I only get vote[p1]: with nothing after.

By the way, I think it's nice to be able to watch a variable as it's more readable than have to open up the state and scroll to find the variable of interest.

[lemmy]

Closing, hoping my commit addresses your itch. By the way, Watch expressions don't support anything that requires parsing such as vote[p1]. :-(

[nano-o]

Thanks! Maybe just displaying vote[p1]: unsupported expression would help users.

[lemmy]

Do you want to provide a patch? :-)

https://github.com/tlaplus/tlaplus/blob/503a1e483a1909e15fe027043a4db719c8ad8021/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java#L536-L563