RE: [tlaplus] CostModel lookup failed

["'Leslie Lamport' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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

-----Original Message-----
From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Markus Kuppe
Sent: Thursday, February 11, 2021 4:01 PM
To: tlaplus@xxxxxxxxxxxxxxxx
Subject: Re: [tlaplus] CostModel lookup failed

On 11.02.21 14:09, Isaac DeFrain wrote:
> 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?


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://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+unsubscribe@xxxxxxxxxxxxxxxx.
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.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BYAPR21MB1256C1620858EF906289EDF9B88B9%40BYAPR21MB1256.namprd21.prod.outlook.com.