Debugger does not support monolith/multi-module specs

[pfeodrippe]

I will check the debugger and add any issues here so it's easy for us to track, if we find more convenient we can split them into their own issues (or what I find that are issues, feel free to ignore it if you think it's fine).

Great work BTW, it will certainly help the TLA+ community to bring more people to the table.

Some issues below (I will add more as I find them (and add a comment for notification if there are any watchers for this issue)):

1. While debugging a monolith step and after stepping into, I've got

Unable to open 'BlockingQueue_TE.tla': 
Unable to read file '/Users/paulo.feodrippe/dev/BlockingQueue/BlockingQueue_TE.tla'
(Error: Unable to resolve non-existing file '/Users/paulo.feodrippe/dev/BlockingQueue/BlockingQueue_TE.tla').

As expected, creating the file did allow me to step into it.

2. In a monolith spec, I cannot add a breakpoint to a module that it's not the first one (the module which gives name to the TLA file).

3. Evaluate in Debug Console is not working yet, placeholder for a future implementation?

4. Let's say we have the expression /\ waitSet' = _TETrace[j].waitSet, when I hover my mouse cursor over waitSet (and after waitSet' has the value of _TETrace[j].waitSet), it only shows "waitSet", should this show the value correspondent to it? I guess this will be solved when the debug console evaluation is implemented.

[lemmy]

3. Yes, this is not yet implemented
4. Does it show a value when you hover over _TETrace?