Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

CostModel lookup failed for expression #415

Open
mryndzionek opened this issue Jan 13, 2020 · 9 comments
Open

CostModel lookup failed for expression #415

mryndzionek opened this issue Jan 13, 2020 · 9 comments
Labels
bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
Projects
mku

Comments

@mryndzionek
Copy link

When model-checking this spec I get an error:

CostModel lookup failed for expression <line 43, col 49 to line 43, col 66 of module CigaretteSmokers>. Reporting costs into <line 31, col 40 to line 31, col 43 of module CigaretteSmokers> instead (Safety and Liveness checking is unaffected. Please report a bug.)

This started occurring after adding ChooseOne in line 31. I see two similar issues closed/fixed, but this still occurs in 1.6.0
@lemmy lemmy added bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ... labels Jan 13, 2020
@lemmy
Copy link
Member

lemmy commented Jan 13, 2020

Please check if this is still an issue with https://nightly.tlapl.us/

@mryndzionek
Copy link
Author

Please check if this is still an issue with https://nightly.tlapl.us/

Yes, it's still there.

@lemmy lemmy added this to the 1.6.1 milestone Jan 13, 2020
@lemmy lemmy added this to TODO (Engineering) in mku via automation Jan 13, 2020
lemmy added a commit that referenced this issue Jan 14, 2020
@lemmy
CostModel lookup failed for LAMBDA expression.
b62ee8d 
Fixes GitHub issue #415
#415

[Bug][TLC]
@lemmy lemmy moved this from TODO (Engineering) to Done in mku Jan 14, 2020
@lemmy lemmy closed this as completed Jan 14, 2020
@lemmy lemmy reopened this Jan 17, 2020
@lemmy
Copy link
Member

lemmy commented Jan 17, 2020 •
edited

(Stripped down) test case passes but not the original spec.

@lemmy lemmy moved this from Done to Doing (Engineering) in mku Jan 17, 2020
@mryndzionek
Copy link
Author

(Stripped) down test case passes but not the original spec.

Yes, confirmed. Let me know if I can help somehow. Is there maybe a write-up on how to setup debug environment?

@lemmy
Copy link
Member

lemmy commented Jan 18, 2020

IDE setup: https://github.com/tlaplus/tlaplus/tree/master/general/ide

@lemmy lemmy moved this from Doing (Engineering) to TODO (Engineering) in mku Apr 6, 2020
@lemmy lemmy removed this from the 1.7.0 milestone Apr 20, 2020
@lemmy
Copy link
Member

lemmy commented Apr 20, 2020

Not a showstopper for 1.7.0.

@lemmy lemmy mentioned this issue Jul 2, 2020
Closed
@lemmy
Copy link
Member

lemmy commented Mar 3, 2021 

CostModel lookup failed for expression <line 174, col 93 to line 174, col 105 of module e001ClientSupplier>. Reporting costs into <line 305, col 14 to line 305, col 54 of module PWSSemantics> instead (Safety and Liveness checking is unaffected. Please report a bug.)

e001ClientSupplier.WOk3U.zip

@lemmy
Copy link
Member

lemmy commented Apr 4, 2021

#588 (comment)

@lemmy
Copy link
Member

lemmy commented Apr 12, 2021

One more CostModelCreator bug: #588 (comment)

@lemmy lemmy mentioned this issue Jul 27, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
Projects
No open projects
mku
  
TODO (Engineering)
Milestone
No milestone
Development

No branches or pull requests
2 participants
@lemmy @mryndzionek