Hello TLA+ community,
I've been encountering this message while checking models with temporal properties using the command-line version of TLC:
CostModel lookup failed for _expression_ <line #, col # to line #, col # of module B>. Reporting costs into <line #, col # to line #, col # of module A> instead (Safety and Liveness checking is unaffected. Please report a bug.)
Note: I've substituted #'s for the reported line and col numbers.
Since I'm not sure what is meant by "CostModel lookup", I'm not sure what details are essential to report here. If it makes any difference, module A EXTENDS module B.
My questions:
1. What is this CostModel lookup?
2. Is this really a bug that I should report?
3. Has anyone else encountered this message?
Thanks in advance!
Best,