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.

Sign up for GitHub

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

ClassCastException in profiler's CostModel when top-level expression of action, init-predicate, invariant, constraints ... is declared RECURSIVE #649

Closed
ahelwer opened this issue Jul 26, 2021 · 3 comments
Closed

ClassCastException in profiler's CostModel when top-level expression of action, init-predicate, invariant, constraints ... is declared RECURSIVE #649

ahelwer opened this issue Jul 26, 2021 · 3 comments
Labels
bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
Projects
mku
Milestone
1.8.0

Comments

@ahelwer
Copy link
Contributor

ahelwer commented Jul 26, 2021 •
edited

Example one-bit-clock spec:

---- MODULE OneBitClock ----
VARIABLE clock
RECURSIVE Check(_)
Check(c) == c \in BOOLEAN
TypeOK == Check(clock)
Init == clock = FALSE
Next == clock' = ~clock
====

When asked to check TypeOK, TLC emits the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.ClassCastException
: class tlc2.tool.coverage.ActionWrapper cannot be cast to class tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader 'app')

Encountered during this thread on the google group.
@lemmy
Copy link
Member

lemmy commented Jul 27, 2021

Workaround: Run TLC without the -coverage parameter.

Related: #314 #415 #588 (comment)

@lemmy lemmy changed the title TLC cannot handle RECURSIVE operators when checking invariants ClassCastException in profiler's CostModel when checking invariants involving RECURSIVE Jul 27, 2021
@lemmy lemmy added bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ... labels Jul 27, 2021
@ahelwer
Copy link
Contributor Author

ahelwer commented Jul 27, 2021

@lemmy is there any way to run TLC without the -coverage parameter from within the toolbox, or does it have to be from the command line?

@lemmy
Copy link
Member

lemmy commented Jul 27, 2021 •
edited

Turn off Profiling on the model's TLC Options page:

Screenshot from 2021-07-27 08-56-14

@lemmy lemmy changed the title ClassCastException in profiler's CostModel when checking invariants involving RECURSIVE ClassCastException in profiler's CostModel when top-level expression of action, init-predicate, invariant, constraints ... is declared RECURSIVE Jul 27, 2021
lemmy added a commit that referenced this issue Jul 27, 2021
@lemmy
ClassCastException in profiler's CostModel when top-level expression of
df1946c 
action, init-predicate, invariant, constraints ... is declared RECURSIVE

Fixes Github issue #649
#649

[Bug][TLC]
@lemmy lemmy added this to TODO (Engineering) in mku via automation Jul 27, 2021
@lemmy lemmy added this to the 1.8.0 milestone Jul 27, 2021
@lemmy lemmy closed this as completed Jul 27, 2021
mku automation moved this from TODO (Engineering) to Done Jul 27, 2021
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
  
Done
Milestone
1.8.0
Development

No branches or pull requests
2 participants
@lemmy @ahelwer