Mixing
in works, while subseteq gives a “identifier undefined” error
I have the following spec:
------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members
Init == members subseteq People
Next == members' = members
Group == Init / [Next]_members
=============================================================================
(I simplified this spec to the point where it's not doing anything useful.)
When I try to run it through TLC, I get the following error:
In evaluation, the identifier members is either undefined or not an operator.
The error points to the Init line.
When I change the Init line to:
Init == members in People
it validates fine.
I want the former functionality because I mean for members to be a collection of People, not a single person.
According to section 16.1.6 of Leslie Lamport's Specifying Systems, "TLA+ provides the following operators on sets:" and lists both in and subseteq.
Why is TLA+ not letting me use subseteq?
tla+ tlc
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
add a comment |
I have the following spec:
------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members
Init == members subseteq People
Next == members' = members
Group == Init / [Next]_members
=============================================================================
(I simplified this spec to the point where it's not doing anything useful.)
When I try to run it through TLC, I get the following error:
In evaluation, the identifier members is either undefined or not an operator.
The error points to the Init line.
When I change the Init line to:
Init == members in People
it validates fine.
I want the former functionality because I mean for members to be a collection of People, not a single person.
According to section 16.1.6 of Leslie Lamport's Specifying Systems, "TLA+ provides the following operators on sets:" and lists both in and subseteq.
Why is TLA+ not letting me use subseteq?
tla+ tlc
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
add a comment |
I have the following spec:
------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members
Init == members subseteq People
Next == members' = members
Group == Init / [Next]_members
=============================================================================
(I simplified this spec to the point where it's not doing anything useful.)
When I try to run it through TLC, I get the following error:
In evaluation, the identifier members is either undefined or not an operator.
The error points to the Init line.
When I change the Init line to:
Init == members in People
it validates fine.
I want the former functionality because I mean for members to be a collection of People, not a single person.
According to section 16.1.6 of Leslie Lamport's Specifying Systems, "TLA+ provides the following operators on sets:" and lists both in and subseteq.
Why is TLA+ not letting me use subseteq?
tla+ tlc
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
I have the following spec:
------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members
Init == members subseteq People
Next == members' = members
Group == Init / [Next]_members
=============================================================================
(I simplified this spec to the point where it's not doing anything useful.)
When I try to run it through TLC, I get the following error:
In evaluation, the identifier members is either undefined or not an operator.
The error points to the Init line.
When I change the Init line to:
Init == members in People
it validates fine.
I want the former functionality because I mean for members to be a collection of People, not a single person.
According to section 16.1.6 of Leslie Lamport's Specifying Systems, "TLA+ provides the following operators on sets:" and lists both in and subseteq.
Why is TLA+ not letting me use subseteq?
tla+ tlc
tla+ tlc
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
edited Nov 22 '18 at 8:07
Philip
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
asked Nov 22 '18 at 7:42
PhilipPhilip
1,044818
1,044818
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members in SUBSET People.
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
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%2f53426052%2fin-works-while-subseteq-gives-a-identifier-undefined-error%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
While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members in SUBSET People.
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
add a comment |
While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members in SUBSET People.
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
add a comment |
While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members in SUBSET People.
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members in SUBSET People.
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
edited Nov 22 '18 at 9:22
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
answered Nov 22 '18 at 9:17
HovercouchHovercouch
90078
90078
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%2f53426052%2fin-works-while-subseteq-gives-a-identifier-undefined-error%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
