will62794 / tla-web

Interactive, web-based environment for exploring TLA+ specifications.
MIT License
69 stars 7 forks source link

Handle model values #7

Closed will62794 closed 2 months ago

will62794 commented 2 years ago

Decide how to handle "model values" for instantiation of CONSTANT parameters. Currently, it is expected that string values are to be used in place of model values.

will62794 commented 8 months ago

Partial support in ca84c8e.

May still need some additional logic to handle nested sets of model values e.g., Quorum = {{n1},{n2},{n1,n2}}

will62794 commented 2 months ago

Parsing of general model values should now be handled after ffe5360. See example Paxos spec + model here.