TLC cannot handle this conjunct of the spec
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 '18 at 2:25
PhilipPhilip
1,044818
add a comment |
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 '18 at 2:25
PhilipPhilip
1,044818
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 '18 at 19:30
add a comment |
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 '18 at 2:25
PhilipPhilip
1,044818
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 '18 at 2:25
PhilipPhilip
1,044818
asked Nov 22 '18 at 2:25
PhilipPhilip
1,044818
asked Nov 22 '18 at 2:25
PhilipPhilip
1,044818
asked Nov 22 '18 at 2:25
PhilipPhilip
1,044818
asked Nov 22 '18 at 2:25
PhilipPhilip
1,044818
1,044818
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 '18 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 '18 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 '18 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 '18 at 19:30
add a comment |
1 Answer
1
active
oldest
votes
The problem was with my use of subseteq in Init, as answered here: in works, while subseteq gives a "identifier undefined" error
answered yesterday
PhilipPhilip
1,044818
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
The problem was with my use of subseteq in Init, as answered here: in works, while subseteq gives a "identifier undefined" error
answered yesterday
PhilipPhilip
1,044818
add a comment |
The problem was with my use of subseteq in Init, as answered here: in works, while subseteq gives a "identifier undefined" error
answered yesterday
PhilipPhilip
1,044818
add a comment |
The problem was with my use of subseteq in Init, as answered here: in works, while subseteq gives a "identifier undefined" error
answered yesterday
PhilipPhilip
1,044818
The problem was with my use of subseteq in Init, as answered here: in works, while subseteq gives a "identifier undefined" error
answered yesterday
PhilipPhilip
1,044818
answered yesterday
PhilipPhilip
1,044818
answered yesterday
PhilipPhilip
1,044818
answered yesterday
PhilipPhilip
1,044818
1,044818
add a comment |
add a comment |
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.
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 '18 at 19:30