William Schultz

Looks like this would require handling [module instantiation](https://github.com/tlaplus/azure-cosmos-tla/blob/23f2c1c51b82a53603d5395360956a6b2c8516da/simple-model/show521677.tla#L23-L25)? (i.e. addressing #14 properly)

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

Parsing of general model values should now be handled after ffe5360. See example Paxos spec + model [here](https://will62794.github.io/tla-web/#!/home?specpath=.%2Fspecs%2FPaxos.tla&constants%5BServer%5D=%7B%22s1%22%2C%22s2%22%2C%20%22s3%22%7D&constants%5BSecondary%5D=%22Secondary%22&constants%5BPrimary%5D=%22Primary%22&constants%5BNil%5D=%22Nil%22&constants%5BInitTerm%5D=0&constants%5BAcceptor%5D=%7Ba1%2Ca2%2Ca3%7D&constants%5BQuorum%5D=%7B%7Ba1%2Ca2%7D%2C%7Ba2%2Ca3%7D%2C%7Ba1%2Ca3%7D%2C%7Ba1%2Ca2%2Ca3%7D%7D&constants%5BProposer%5D=%7Bp1%2Cp2%7D&constants%5BValue%5D=%7Bv1%2Cv2%7D&constants%5BBallot%5D=%7B0%2C1%2C2%2C3%7D&constants%5BNone%5D=None).

@fintara I just pushed a [change](https://github.com/will62794/tla-web/commit/5933fa65e6744e36b1f2fb4196449f5a3a8d92cf) (see #44) so that simple conjunctions now short-circuit as well when possible. See if that fixes the issue in your spec above.

I expect this is due to them including primed expressions, which likely won't be handled properly right now.

Closing unless you believe there is some other underlying bug here.

Related: b0e1ae5.

Partially addressed in 6045e4c.

Nothing too fancy yet, but this should now be reported as an error in the UI ([example spec](https://will62794.github.io/spectacle/#!/home?specpath=.%2Fspecs%2Ftest_missing_assigned_vars.tla)).

This appears to be due to [this](https://web.git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/qspinlock.tla#n13) `CHOOSE` statement, which is [overridden in their config](https://web.git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/qspinlock.cfg#n6). For example, [this spec](https://will62794.github.io/spectacle/#!/home?specpath=.%2Fspecs%2Fwith_state_graphs%2Fqspinlock.tla&constants%5BCPUS%5D=%7Bp1%2Cp2%7D&constants%5BMAX_NODES%5D=1&constants%5BPENDING_LOOPS%5D=1&constants%5BdefaultInitValue%5D=%22default%22) works after slightly modifying the `CHOOSE`. I plan to add a...