CostModel lookup failed

14 views
Skip to first unread message

Isaac DeFrain

unread,
Feb 11, 2021, 5:10:10 PMFeb 11
to tla...@googlegroups.com
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,

Isaac DeFrain

Markus Kuppe

unread,
Feb 11, 2021, 7:01:28 PMFeb 11
to tla...@googlegroups.com
Hi Isaac,

please consider adding your spec and model to the relevant Github issue
[1]. The warning is "mostly harmless", saying that coverage/profiling
information will be off for the locations mentioned in the warning.

If you don't care about coverage/profiling [2], run TLC without the
"-coverage" parameter.

Thanks,
Markus

[1] https://github.com/tlaplus/tlaplus/issues/415
[2] https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/profiling.html

Leslie Lamport

unread,
Feb 11, 2021, 7:06:10 PMFeb 11
to tla...@googlegroups.com
Hi Markus,

Since it appears that a significant number of people run TLC from the command line, it seems like a bad idea to make the -coverage option produce the reams of output needed for profiling. In fact, why should that output be produced if TLC isn't being called in -tool mode?

Leslie
[1] https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ftlaplus%2Ftlaplus%2Fissues%2F415&amp;data=04%7C01%7Clamport%40microsoft.com%7C940fc9247a96405ae48608d8cee95bf3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637486849382662185%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=3xz9VB468FmKmlLEo0lfeXMGbFmjhuvR6PMBOffdxJM%3D&amp;reserved=0
[2] https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Ftla.msr-inria.inria.fr%2Ftlatoolbox%2Fdoc%2Fmodel%2Fprofiling.html&amp;data=04%7C01%7Clamport%40microsoft.com%7C940fc9247a96405ae48608d8cee95bf3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637486849382672178%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=T3Vi5avKmNeRWzPSga4LIS0UB5Ei1cJovwGN%2F2oA8NI%3D&amp;reserved=0

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Ftlaplus%2Fa392de58-4547-04bc-8aef-faf9be8ce31a%2540lemmster.de&amp;data=04%7C01%7Clamport%40microsoft.com%7C940fc9247a96405ae48608d8cee95bf3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637486849382672178%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=nFSsI%2FV2MH0Ztvo0zoWMNC8L9bc7Kj7j69KkaZnmNWo%3D&amp;reserved=0.
Reply all
Reply to author
Forward
0 new messages