TLC cannot handle this conjunct of the spec
up vote
0
down vote
favorite
I have a TLA+ module, which, summarized, looks like this:
--- MODULE Group ---
CONSTANTS People
VARIABLES members
Join(person) == ...
Leave(person) == ...
Init == members subseteq People
Next == E p in People :
/ Join(p)
/ Leave(p)
====================
When I try to model-check this with TLC, I get 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.RuntimeException
:
TLC cannot handle this conjunct of the spec:
line X, col Y to line Z, col T of module Group
...pointing to the entire content of Next.
I believe my Next is well-written, because here's an example model that has a very similar Next to mine: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
Also, section 14.2.2 of Leslie Lamport's Specifying Systems says:
TLC can evaluate a set-valued expression only if that expression equals a finite set[...]. TLC will evaluate expressions of the following forms only if it can enumerate the set S:
and provides the example of "there exists x in S such that p".
How can I solve this error?
tla+ tlc
asked Nov 22 at 2:25
Philip
1,017818
add a comment |
up vote
0
down vote
favorite
I have a TLA+ module, which, summarized, looks like this:
--- MODULE Group ---
CONSTANTS People
VARIABLES members
Join(person) == ...
Leave(person) == ...
Init == members subseteq People
Next == E p in People :
/ Join(p)
/ Leave(p)
====================
When I try to model-check this with TLC, I get 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.RuntimeException
:
TLC cannot handle this conjunct of the spec:
line X, col Y to line Z, col T of module Group
...pointing to the entire content of Next.
I believe my Next is well-written, because here's an example model that has a very similar Next to mine: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
Also, section 14.2.2 of Leslie Lamport's Specifying Systems says:
TLC can evaluate a set-valued expression only if that expression equals a finite set[...]. TLC will evaluate expressions of the following forms only if it can enumerate the set S:
and provides the example of "there exists x in S such that p".
How can I solve this error?
tla+ tlc
asked Nov 22 at 2:25
Philip
1,017818
1
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points toNext? Because that's a disjunct, not a conjunct. It's more likely to be a problem inSpec.
– Jorge Adriano
Nov 22 at 19:30
add a comment |
up vote
0
down vote
favorite
up vote
0
down vote
favorite
I have a TLA+ module, which, summarized, looks like this:
--- MODULE Group ---
CONSTANTS People
VARIABLES members
Join(person) == ...
Leave(person) == ...
Init == members subseteq People
Next == E p in People :
/ Join(p)
/ Leave(p)
====================
When I try to model-check this with TLC, I get 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.RuntimeException
:
TLC cannot handle this conjunct of the spec:
line X, col Y to line Z, col T of module Group
...pointing to the entire content of Next.
I believe my Next is well-written, because here's an example model that has a very similar Next to mine: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
Also, section 14.2.2 of Leslie Lamport's Specifying Systems says:
TLC can evaluate a set-valued expression only if that expression equals a finite set[...]. TLC will evaluate expressions of the following forms only if it can enumerate the set S:
and provides the example of "there exists x in S such that p".
How can I solve this error?
tla+ tlc
asked Nov 22 at 2:25
Philip
1,017818
I have a TLA+ module, which, summarized, looks like this:
--- MODULE Group ---
CONSTANTS People
VARIABLES members
Join(person) == ...
Leave(person) == ...
Init == members subseteq People
Next == E p in People :
/ Join(p)
/ Leave(p)
====================
When I try to model-check this with TLC, I get 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.RuntimeException
:
TLC cannot handle this conjunct of the spec:
line X, col Y to line Z, col T of module Group
...pointing to the entire content of Next.
I believe my Next is well-written, because here's an example model that has a very similar Next to mine: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
Also, section 14.2.2 of Leslie Lamport's Specifying Systems says:
TLC can evaluate a set-valued expression only if that expression equals a finite set[...]. TLC will evaluate expressions of the following forms only if it can enumerate the set S:
and provides the example of "there exists x in S such that p".
How can I solve this error?
tla+ tlc
tla+ tlc
asked Nov 22 at 2:25
Philip
1,017818
asked Nov 22 at 2:25
Philip
1,017818
asked Nov 22 at 2:25
Philip
1,017818
asked Nov 22 at 2:25
Philip
1,017818
asked Nov 22 at 2:25
Philip
1,017818
1,017818
1
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points toNext? Because that's a disjunct, not a conjunct. It's more likely to be a problem inSpec.
– Jorge Adriano
Nov 22 at 19:30
add a comment |
1
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points toNext? Because that's a disjunct, not a conjunct. It's more likely to be a problem inSpec.
– Jorge Adriano
Nov 22 at 19:30
1
1
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points to
Next? Because that's a disjunct, not a conjunct. It's more likely to be a problem in Spec.– Jorge Adriano
Nov 22 at 19:30
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points to
Next? Because that's a disjunct, not a conjunct. It's more likely to be a problem in Spec.– Jorge Adriano
Nov 22 at 19:30
add a comment |
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53423052%2ftlc-cannot-handle-this-conjunct-of-the-spec%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
You need to provide a minimal self-contained example. Try to reduce your code to a small example that shows the error. Also are you sure it points to
Next? Because that's a disjunct, not a conjunct. It's more likely to be a problem inSpec.– Jorge Adriano
Nov 22 at 19:30