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

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
Projects

Comments

@mryndzionek
Copy link

@mryndzionek mryndzionek commented Jan 13, 2020

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
Copy link
Member

@lemmy lemmy commented Jan 13, 2020

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

@mryndzionek
Copy link
Author

@mryndzionek mryndzionek commented Jan 13, 2020

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
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 Jan 14, 2020
@lemmy lemmy reopened this Jan 17, 2020
@lemmy
Copy link
Member

@lemmy lemmy commented Jan 17, 2020

(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

@mryndzionek mryndzionek commented Jan 18, 2020

(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 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 lemmy commented Apr 20, 2020

Not a showstopper for 1.7.0.

@lemmy
Copy link
Member

@lemmy 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 lemmy commented Apr 4, 2021

@lemmy
Copy link
Member

@lemmy lemmy commented Apr 12, 2021

One more CostModelCreator bug: #588 (comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
mku
  
TODO (Engineering)
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants