This seems to me to be a rare situation, since it's uncommon for the next-state action of the spec being checked by TLC to be defined in an instantiated module. So, there are many more important problems with TLC that should be fixed first. (If anyone wants to go through the code and suggest how this problem can be fixed, I'd be happy to consider doing it.) It would be useful to document the current state of reporting of locations of errors that are caused by a problem in an instantiated module. I believe it may depend on whether the module is instantiated with substitutions.
Leslie
On Monday, November 9, 2015 at 8:24:50 AM UTC-8, Y2i wrote:
When "Successor state is not completely specified by the next-state action" error is reported in instantiated module, clicking on the offending action in Error-Trace moves the cursor to the line where the module is instantiated instead of the offending action definition within the instantiated module. Would it be possible to improve this in the next release?
Thank you,
Yuri