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

Parse TLC configuration files #76

Closed
konnov opened this issue Dec 6, 2019 · 2 comments
Closed

Parse TLC configuration files #76

konnov opened this issue Dec 6, 2019 · 2 comments
Assignees
@andrey-kuprianov
Labels
new New issue to be triaged.
Milestone
v0.7-dev-integration

Comments

@konnov
Copy link
Collaborator

konnov commented Dec 6, 2019

Apalache supports two approaches to dealing with constants: (1) asking the user to overwrite them with constant definitions, and (2) declaring a ConstInit operator that restricts the constants. The both approaches are incompatible with automation.

We should take the approach of TLC and simply parse the TLC config files.
@konnov konnov added the new New issue to be triaged. label Dec 6, 2019
@konnov konnov added this to the BMCMT-0.7-dev-tlc-compat milestone Dec 6, 2019
@konnov konnov self-assigned this Dec 6, 2019
@lemmy
Copy link
Contributor

lemmy commented Dec 6, 2019

In reverse, we want TLC to support something like ConstInit: tlaplus/tlaplus#272

konnov pushed a commit that referenced this issue Dec 10, 2019
towards #76: a parser for TLC config files (not integrated yet), 8 hours
b71186a
@andrey-kuprianov
Copy link
Contributor

implemented with the last commit a7028ba

@konnov konnov mentioned this issue Apr 10, 2020
Closed
Kukovec pushed a commit that referenced this issue Jun 26, 2020
towards #76: a parser for TLC config files (not integrated yet), 8 hours
16ca130
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andrey-kuprianov andrey-kuprianov

Labels
new New issue to be triaged.
Projects
None yet
Milestone
v0.7-dev-integration
Development

No branches or pull requests
3 participants
@lemmy @konnov @andrey-kuprianov