will62794 / tla-web Goto Github PK

Interactive, web-based environment for exploring TLA+ specifications.

License: MIT License

HTML 1.08% JavaScript 44.90% TLA 51.45% Shell 0.10% Makefile 0.01% CSS 2.44% C 0.03%

tla-web's Introduction

TLA+ Web Explorer

This is an interactive, web-based environment for exploring and sharing TLA+ specifications. The motivation is to have a better way to quickly interact with a TLA+ spec and easily share results. For example, having a way to share counterexample traces in a convenient, portable, and repeatable manner.

A live version of the tool is currently hosted here, and here are some example specs to try out:

The current version of the tool utilizes the TLA+ tree-sitter grammar for parsing TLA+ specs and implements a TLA+ interpreter/executor on top of this in Javascript. This allows the tool to interpret specs natively in the browser, without relying on an external language server. The Javascript interpreter is likely much slower than TLC, but efficient model checking isn't currently a goal of the tool.

Usage Notes

The current tool expects that a specification has defined its initial state predicate and next state relation as Init and Next definitions, respectively. If your specification has these defined under different names, an error will be reported and spec evaluation will fail. Eventually this will be made configurable, but the current tool looks for these hard-coded definitions. Also, there is currently no support for user module imports, so specs are expected to be written in a single module. The interpreter does, however, by default support most operators from the TLA+ standard modules.

You can also see a live demo of the tool and its features in this presentation, which also gives a very high level overview of the tool architecture and implementation details.

tla-web's People

Contributors

Stargazers

Watchers

Forkers

lemmy teodorov zabrane bishwajitdey leauny dgomezferro ajdavis

tla-web's Issues

Encode CONSTANT value settings in URL

Allow specs to be shared via a URL that includes an assignment of concrete values to CONSTANT parameters.

Add ability to explode/split trace view on a specified constant set

It is often helpful to view the state variables in a trace by process (e.g. nodes, servers, etc.). Adding the ability to explode/split the trace on an arbitrary constant set could be one approach to this i.e. instead of the viewer displaying a single trace, a separate trace is shown for each process.

Bogus "tx_id" doesn't exist in function domain.

The following spec works fine in TLC, but fails exploration with tla-web with:

Error: argument "tx_id" doesn't exist in function domain.
    at assert (eval.js:39:15)
    at FcnRcdValue.applyArg (eval.js:422:9)
    at evalExpr (eval.js:3679:31)
    at evalExpr (eval.js:4000:16)
    at evalExpr (eval.js:3462:17)
    at evalExpr (eval.js:4000:16)
    at evalLetIn (eval.js:3161:26)
    at evalExpr (eval.js:3400:16)
    at evalExpr (eval.js:4000:16)
    at eval.js:2692:19

The source of the error appears to be StatusCommittedResponseAction.

---- MODULE SingleNode ----

EXTENDS Naturals, Sequences, SequencesExt

RwTxRequest == "RwTxRequest"
RwTxResponse == "RwTxResponse"
RoTxRequest == "RoTxRequest"
RoTxResponse == "RoTxResponse"
TxStatusReceived == "TxStatusReceived"

CommittedStatus == "CommittedStatus"
InvalidStatus == "InvalidStatus"
TxStatuses == {
    CommittedStatus,
    InvalidStatus
    }

FirstBranch == 1

Views == Nat

\* Sequence numbers start at 1, 0 is used a null value
SeqNums == Nat

\* TxIDs consist of a view and sequence number and thus start at (1,1)
TxIDs == Views \X SeqNums

\* This models uses a dummy application where read-write transactions 
\* append an integer to a list and then reads the list
\* Read-only transactions simply read the list
Txs == Nat

VARIABLES history

HistoryTypeOK ==
    \A i \in DOMAIN history:
        \/  /\ history[i].type \in {RwTxRequest, RoTxRequest}
            /\ history[i].tx \in Txs
        \/  /\ history[i].type \in {RwTxResponse, RoTxResponse}
            /\ history[i].tx \in Txs
            /\ history[i].observed \in Seq(Txs)
            /\ history[i].tx_id \in TxIDs
        \/  /\ history[i].type = TxStatusReceived
            /\ history[i].tx_id \in TxIDs
            /\ history[i].status \in TxStatuses

\* Abstract ledgers that contains only client transactions (no signatures)
\* Indexed by view, each ledger is the ledger associated with leader of that view 
\* In practice, the ledger of every CCF node is one of these or a prefix for one of these
\* This could be switched to a tree which can represent forks more elegantly
VARIABLES ledgerBranches

LedgerTypeOK ==
    \A view \in DOMAIN ledgerBranches:
        \A seqnum \in DOMAIN ledgerBranches[view]:
            \* Each ledger entry is tuple containing a view and tx
            \* The ledger entry index is the sequence number
            /\ ledgerBranches[view][seqnum].view \in Views
            /\ "tx" \in DOMAIN ledgerBranches[view][seqnum] => ledgerBranches[view][seqnum].tx \in Txs

\* In this abstract version of CCF's consensus layer, each ledger is append-only
LedgersMonoProp ==
    [][\A view \in DOMAIN ledgerBranches: IsPrefix(ledgerBranches[view], ledgerBranches'[view])]_ledgerBranches

vars == << history, ledgerBranches >>

TypeOK ==
    /\ HistoryTypeOK
    /\ LedgerTypeOK

Init ==
    /\ history = <<>>
    /\ ledgerBranches = [ x \in 1..FirstBranch |-> <<>>]

IndexOfLastRequested ==
    SelectLastInSeq(history, LAMBDA e : e.type \in {RwTxRequest, RoTxRequest})

NextRequestId ==
    IF IndexOfLastRequested = 0 THEN 0 ELSE history[IndexOfLastRequested].tx+1

\* Submit new read-write transaction
\* This could be extended to add a notion of session and then check for session consistency
RwTxRequestAction ==
    /\ history' = Append(
        history, 
        [type |-> RwTxRequest, tx |-> NextRequestId]
        )
    /\ UNCHANGED ledgerBranches

\* Execute a read-write transaction
RwTxExecuteAction ==
    /\ \E i \in DOMAIN history :
        /\ history[i].type = RwTxRequest
        \* Check transaction has not already been added to a ledger
        /\ \A view \in DOMAIN ledgerBranches: 
            \A seqnum \in DOMAIN ledgerBranches[view]: 
                "tx" \in DOMAIN ledgerBranches[view][seqnum]
                => history[i].tx /= ledgerBranches[view][seqnum].tx
        \* Note that a transaction can be added to any ledger, simulating the fact
        \* that it can be picked up by the current leader or any former leader
        /\ \E view \in FirstBranch..Len(ledgerBranches):
                ledgerBranches' = [ledgerBranches EXCEPT ![view] = 
                    Append(@,[view |-> view, tx |-> history[i].tx])]
        /\ UNCHANGED history

LedgerBranchTxOnly(branch) ==
    LET SubBranch == SelectSeq(branch, LAMBDA e : "tx" \in DOMAIN e)
    IN [i \in DOMAIN SubBranch |-> SubBranch[i].tx]

\* Response to a read-write transaction
RwTxResponseAction ==
    /\ \E i \in DOMAIN history :
        \* Check request has been received and executed but not yet responded to
        /\ history[i].type = RwTxRequest
        /\ {j \in DOMAIN history: 
            /\ j > i 
            /\ history[j].type = RwTxResponse
            /\ history[j].tx = history[i].tx} = {}
        /\ \E view \in FirstBranch..Len(ledgerBranches):
            /\ \E seqnum \in DOMAIN ledgerBranches[view]: 
                /\ "tx" \in DOMAIN ledgerBranches[view][seqnum]
                /\ history[i].tx = ledgerBranches[view][seqnum].tx
                /\ history' = Append(
                    history,[
                        type |-> RwTxResponse, 
                        tx |-> history[i].tx, 
                        observed |-> LedgerBranchTxOnly(SubSeq(ledgerBranches[view],1,seqnum)),
                        tx_id |-> <<ledgerBranches[view][seqnum].view, seqnum>>] )
    /\ UNCHANGED ledgerBranches

\* Sending a committed status message
\* Note that a request could only be committed if it's in the highest view's ledger
StatusCommittedResponseAction ==
    /\ \E i \in DOMAIN history :
        LET view == history[i].tx_id[1]
            seqno == history[i].tx_id[2]
        IN /\ history[i].type = RwTxResponse
           /\ Len(Last(ledgerBranches)) >= seqno
           /\ Last(ledgerBranches)[seqno].view = view
           \* There is no future InvalidStatus that's incompatible with this commit
           \* This is to accomodate StatusInvalidResponseAction making future commits invalid,
           \* and is an unnecessary complication for model checking. It does facilitate trace
           \* validation though, by allowing immediate processing of Invalids without
           \* needing to wait for the commit history knowledge to catch up.
           /\ \lnot \E j \in DOMAIN history:
                /\ history[j].type = TxStatusReceived
                /\ history[j].status = InvalidStatus
                /\ history[j].tx_id[1] = view
                /\ history[j].tx_id[2] <= seqno
           \* Reply
           /\ history' = Append(
              history,[
                type |-> TxStatusReceived, 
                tx_id |-> history[i].tx_id,
                status |-> CommittedStatus]
              )
    /\ UNCHANGED ledgerBranches

\* Append a transaction to the ledger which does not impact the state we are considering
AppendOtherTxnAction ==
    /\ \E view \in FirstBranch..Len(ledgerBranches):
        ledgerBranches' = [ledgerBranches EXCEPT ![view] = 
                    Append(@,[view |-> view])]
    /\ UNCHANGED history

\* A CCF service with a single node will never have a view change
\* so the log will never be rolled back and thus transaction IDs cannot be invalid
Next ==
    \/ RwTxRequestAction
    \/ RwTxExecuteAction
    \/ RwTxResponseAction
    \/ StatusCommittedResponseAction
    \/ AppendOtherTxnAction
====

/cc @heidihoward @achamayou

Next-state relation disabled when it is not

---- MODULE Foo ----

VARIABLE x

Init == x = TRUE

Next == x' = ~x
====

Four boolean values: TRUE, FALSE, false, true

See values of variable terminationDetected:

---------------------- MODULE AsyncTerminationDetection ---------------------
EXTENDS Naturals

N == 2

ASSUME NIsPosNat == N \in Nat \ {0}

Node == 0 .. N-1

VARIABLES 
  active,               \* activation status of nodes
  pending,              \* number of messages pending at a node
  terminationDetected

vars == << active, pending, terminationDetected >>

terminated == \A n \in Node : ~ active[n] /\ pending[n] = 0

-----------------------------------------------------------------------------

Init ==
    /\ active \in [ Node -> BOOLEAN ]
    /\ pending \in [ Node -> 0..1 ]
    /\ terminationDetected \in {FALSE, terminated}

Next ==
	UNCHANGED vars

====

Debug mode should show where in spec an evaluation error occurred

For debugging, clearly show where an evaluation error occurred, either in the browser console or visually in the spec text pane.

Add additional tests for ENABLED construct

Initial support was added in 29b803b, but more tests should be added.

Add additional tests for RECURSIVE operators

Some initial tests for RECURSIVE operators exist, but should test more thoroughly.

Real-world spec challenge

Handle https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677.tla. :-)

Should notify user if spec fails to load

Two cases I'm thinking of:

Loading a PlusCal file without translation will cause it to spin forever (since it can't translate the pluscal file)
Loading a github link like https://github.com/hwayne/tla-graphing-demo/blob/master/threads.tla will fail because it's not the raw link: you need https://raw.githubusercontent.com/hwayne/tla-graphing-demo/master/threads.tla

Parse error if Next is defined on one line

This module causes a parse error, although it's correct syntax:

------------------------------- MODULE Conjunct ----------------------------- 
EXTENDS TLC, Naturals

VARIABLES x

Action1 == 1 = 2 /\ <<>>[0]
Action2 == x' = x + 1

Next == Action1 \/ Action 2
Init == x = 176
=============================================================================

Replace the Next definition thus to allow parsing:

Next ==
  \/ Action1
  \/ Action 2

The first module should parse identically.

Comments preceding the TLA+ module break the web explorer

a
------------------------------- MODULE Foo -------------------------------
EXTENDS Integers

VARIABLE x

Init ==
	x = 2

Next ==
	x' = 2

=====

Show an error message if any action doesn't assign all variables

Such actions are ignored according to this comment, but the spec should fail to evaluate, with a helpful error.

Operators from standard modules do not work

---- MODULE Issue7 ----
EXTENDS TLC, Naturals, FiniteSets

VARIABLES x

Init == x = {}

Next == x' = Cardinality(x)

====

---- MODULE Issue7 ----
EXTENDS TLC, Naturals, Sequences

VARIABLES x

Init == x = <<>>

Next == x' = Len(x)

====

TypeError: Cannot read properties of undefined (reading 'length')
    at eval.js:900:40
    at lodash.min.js:98:241
    at lodash.min.js:54:66
    at ue (lodash.min.js:35:327)
    at Function.Kc [as mapValues] (lodash.min.js:98:213)
    at evalEq (eval.js:896:30)
    at evalBoundInfix (eval.js:1025:16)
    at evalBoundInfix (eval.js:2079:15)
    at evalExpr (eval.js:1598:16)
    at evalExpr (eval.js:2070:15)

Allow unit tests to execute in background

Execution of these unit tests runs synchronously, blocking the UI until they complete, which can take several seconds. It may be better to use a standard unit testing framework that allows for async/background execution along with better diagnostics, reporting, etc.

Various issues with example spec (see debug console)

https://will62794.github.io/tla-web/?specpath=https://raw.githubusercontent.com/lemmy/tla-web/master/specs/EWD998.tla

Finite stuttering should be possible?

---- MODULE Foo ----

VARIABLE x

Init == x = TRUE

Next == x'\in BOOLEAN
====

Variables values undefined when operator is primed

See undefined value of variable terminationDetected and priming of terminated operator:

---------------------- MODULE AsyncTerminationDetection ---------------------
EXTENDS Naturals

N == 2

ASSUME NIsPosNat == N \in Nat \ {0}

Node == 0 .. N-1

VARIABLES 
  active,               \* activation status of nodes
  pending,              \* number of messages pending at a node
  terminationDetected

vars == << active, pending, terminationDetected >>

terminated == \A n \in Node : ~ active[n] /\ pending[n] = 0

-----------------------------------------------------------------------------

Init ==
    /\ active \in [ Node -> BOOLEAN ]
    /\ pending \in [ Node -> 0..1 ]
    /\ terminationDetected \in {FALSE, terminated}

Terminate(i) ==
    /\ active' \in { f \in [ Node -> BOOLEAN] : \A n \in Node: ~active[n] => ~f[n] }
    /\ pending' = pending
    /\ terminationDetected' \in {terminationDetected, terminated'}

SendMsg(i, j) ==
    /\ active[i]
    /\ pending' = [pending EXCEPT ![j] = @ + 1]
    /\ UNCHANGED << active, terminationDetected >>

Wakeup(i) ==
    /\ pending[i] > 0
    /\ active' = [active EXCEPT ![i] = TRUE]
    /\ pending' = [pending EXCEPT ![i] = @ - 1]
    /\ UNCHANGED << terminationDetected >>

DetectTermination ==
    /\ terminated
    /\ ~terminationDetected
    /\ terminationDetected' = TRUE
    /\ UNCHANGED << active, pending >>

-----------------------------------------------------------------------------

Next ==
    \/ DetectTermination
    \/ \E i \in Node, j \in Node:   
        \/ Terminate(i)
        \/ Wakeup(i)
        \/ SendMsg(i, j)
=============================================================================

Folds not supported

I'd like to use folds over sequences, but they don't seem to be supported. See an example below. I assume that recursive definitions are tricky to add? Could you suggest a workaround? This is at the moment a bit of a blocker for me - I'd like to use tla-web as "interactive docs" for some of the subsystems I've modeled in TLA, but the models do rely on folds.

---- MODULE Web ----

\* The following two definitions are copied verbatim from the community modules
MapThenFoldSet(op(_,_), base, f(_), choose(_), S) ==
  LET iter[s \in SUBSET S] ==
        IF s = {} THEN base
        ELSE LET x == choose(s)
             IN  op(f(x), iter[s \ {x}])
  IN  iter[S]

FoldLeft(op(_, _), base, seq) == 
  MapThenFoldSet(LAMBDA x,y : op(y,x), base,
                 LAMBDA i : seq[i],
                 LAMBDA S : Max(S),
                 DOMAIN seq)


VARIABLE
    seq,
    val

Init ==
    /\ seq = << 1, 2, 3 >>
    /\ val = FoldLeft(LAMBDA x, y: x + y, 0, seq)

Next == UNCHANGED << seq, val >>
   
====

Lasso detection rules out behaviors

-------------------------------- MODULE S -------------------------------
VARIABLES p

Init == p = FALSE

Next == p' \in BOOLEAN
============================================================================

The evaluator won't let me generate a behavior such as F, T, T, F, ... The moment when two consecutive states are equivalent, the back to state marker is added, causing, e.g., this example to become F, T, T, T, T, T, ....

Bogus results for trace expressions

The trace expressions RoTxRequestAction and RwTxRequestAction for https://github.com/lemmy/CCF/blob/mku-ConsistencyMonolith/tla/consistency/Consistency.tla are certainly not true in the shown trace.

Handle primed expressions correctly

See simple failing spec.

Add Linearizability spec as example

@lorin's linearizability spec at https://github.com/lorin/tla-linearizability is a great use-case for tla-web. Imagine exploring the scenarios interactively while studying the original lin paper.

Feature Request: ALIAS

Hi - I'm Finn, a Microsoft Research intern working with @lemmy on some TLA+ specifications. You'll have seen me CC'd in one or two other issues. This issue is on the same theme, but now I'm closer to the polishing stage and have a bit more leeway to put effort into e.g tech for visualizing our work.
I'm trying to make this issue as complete as possible, so apologies if I re-state something you already know about.

When exploring more complex specifications, sometimes a feature of interest will not directly be in the state space. When in this situation, TLC offers the option (called ALIAS) to override the way it displays state, such that other features can be shown alongside / instead of the raw state variables.

Here's a heavily abridged fragment of something I'm working on that would benefit from this (I made sure this version works in the current explorer):

---- MODULE Example ----
EXTENDS Naturals, Sequences

VARIABLE log, idx

Init ==
    /\ log = <<>>
    /\ idx = 0

IncIdx ==
    /\ idx' = idx + 1
    /\ UNCHANGED log

JumpIdx ==
    /\ idx > 0
    /\ idx' \in 0..Len(log)
    /\ UNCHANGED log

GrowLog ==
    /\ log' = Append(log, idx)
    /\ UNCHANGED idx

Read ==
    IF   idx < Len(log)
    THEN {log[idx]}
    ELSE {}

Next ==
    \/ IncIdx
    \/ JumpIdx
    \/ GrowLog

Spec == Init /\ [][Next]_<<log, idx>>

Alias == [
    log |-> log,
    idx |-> idx,
    Read |-> Read
]

====

The take-away is that Read is derivable from any given state, but it might hard to calculate on the spot for humans, so having it spelled out in the visuals would improve the exploring experience for specs like this one. In particular, forcing someone unfamiliar with a spec to run one or more operator definitions in their heads as they try to understand a spec would be ... headache inducing.

From my perspective, an MVP implementation would be to look for an operator called Alias and, if it's there, assume it will yield a function associating a "virtual" set of state variables with a set of values to display at each state.

I have some cycles available to help develop such a thing, if that's of interest. Let me know if I should go and try to put together a PR.

Priority of :> not handled correctly

Hi, first off thanks for the project, this is very nice! However, there seems to be a bug in the interpreter, in handling the priority of the :> operator. It gets confused by this spec:

---- MODULE Web ----
EXTENDS TLC

VARIABLES
    x,
    y

Init ==
    /\ x = 0 :> 0
    /\ y = 1 :> 1

Next == UNCHANGED <<x, y>>

====

But this works:

---- MODULE Web ----
EXTENDS TLC

VARIABLES
    x,
    y

Init ==
    /\ x = (0 :> 0)
    /\ y = (1 :> 1)

Next == UNCHANGED <<x, y>>

====

Can I embed this in another website?

This is amazingly cool, thank you for making this.
If possible, I think this would be a great addition to learntla. Is it something I can embed in another website? If so, how? No worries if this is impossible or would take too long to explain!

Can't use EXCEPT on sequences, or Append on sequence-domain functions

Sometimes, you need to "reassign" part of a sequence in your next-state relation.

Here's a minimal example of what I mean (this spec does not work):

---- MODULE test ----
EXTENDS Naturals

VARIABLE seq

Init ==
    /\ seq = <<1, 2, 3>>

Next ==
    /\ seq' = [seq EXCEPT ![1] = IF @ = 5 THEN 1 ELSE @ + 1]

Spec == Init /\ [][Next]_seq

====

This doesn't work currently, because I imagine EXCEPT's implementation asserts that it was given a function or record.
On its own, it would be nice if this worked. I think, however, that this exposes a slightly more fundamental things that could be addressed.

The problem is that it doesn't work the "other way round" either. I can sort of work around the issue like this (this spec works):

---- MODULE test ----
EXTENDS Naturals

VARIABLE seq

Init ==
    /\ seq = <<1, 2, 3>>

Next ==
    /\ seq' = [ i \in DOMAIN seq |->
    	IF i = 1 THEN
        	IF seq[1] = 5 THEN 1 ELSE seq[1] + 1
        ELSE seq[i]]

Spec == Init /\ [][Next]_seq

====

The problem, then, becomes that I can't go back to using seq like a sequence. If I have a spec that uses both EXCEPT and Append on the same value in alternation, then that itself becomes a problem. See this last example, which also does not work:

---- MODULE test ----
EXTENDS Naturals, Sequences

VARIABLE seq

Init ==
    /\ seq = <<1, 2, 3>>

Inc ==
    /\ seq' = [ i \in DOMAIN seq |->
    	IF i = 1 THEN
        	IF seq[1] = 5 THEN 1 ELSE seq[1] + 1
        ELSE seq[i]]

App ==
	/\ seq' = Append(seq, seq[1])

Next ==
	\/ Inc
    \/ App

Spec == Init /\ [][Next]_seq

====

I guess, ultimately, it would be very nice if <<0, 0, 0>> = [i \in DOMAIN {1, 2, 3} |-> 0] (or, enough implementation edge cases to make this true for the user, at least).

Let me know if you'd like more test cases along this theme - I can probably come up with a couple more.

Quantification over two or more variables not supported

---- MODULE Issue ----
EXTENDS Naturals

VARIABLE x, y

Init == 
    /\ x = 0
    /\ y = 0

Next == 
    \E i,j \in 1..3:
    	/\ x' = i
        /\ y' = j
====

Workaround:

---- MODULE Issue ----
EXTENDS Naturals

VARIABLE x, y

Init == 
    /\ x = 0
    /\ y = 0

Next == 
    \E i \in 1..3, j \in 1..3:
    	/\ x' = i
        /\ y' = j
====

Support recursive operators

Add support for recursive (RECURSIVE) operator definitions. See one basic example.

Handle model values

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.

UNCHANGED vars disjunct

---- MODULE lockserver_nodefs ----
EXTENDS TLC, Naturals

Server == {"s1", "s2"}
Client == {"c1", "c2"}

VARIABLE semaphore
VARIABLE clientlocks
vars==<<semaphore, clientlocks>>

TypeOK ==
    /\ semaphore \in [Server -> {TRUE, FALSE}]
    /\ clientlocks \in [Client -> SUBSET Server]

\* Initially each server holds its lock, and all clients hold no locks.
Init == 
    /\ semaphore = [i \in Server |-> TRUE]
    /\ clientlocks = [i \in Client |-> {}]

Next == 
    \/ \E c \in Client, s \in Server : 
        /\ semaphore[s] = TRUE
        /\ clientlocks' = [clientlocks EXCEPT ![c] = clientlocks[c] \cup {s}]
        /\ semaphore' = [semaphore EXCEPT ![s] = FALSE]
    \/ \E c \in Client, s \in Server : 
        /\ s \in clientlocks[c]
        /\ clientlocks' = [clientlocks EXCEPT ![c] = clientlocks[c] \ {s}]
        /\ semaphore' = [semaphore EXCEPT ![s] = TRUE]
    \/ UNCHANGED vars

====

TypeError: Cannot read properties of null (reading 'fingerprint')
    at eval.js:412:45
    at Array.map (<anonymous>)
    at FcnRcdValue.fingerprint (eval.js:412:34)
    at TupleValue.fingerprint (eval.js:279:20)
    at evalEq (eval.js:1217:32)
    at evalBoundInfix (eval.js:1338:16)
    at evalBoundInfix (eval.js:2530:15)
    at evalExpr (eval.js:2075:16)
    at evalExpr (eval.js:2517:15)
    at evalExpr (eval.js:2066:16)

The problem appears to be UNCHANGED vars, whereas the equivalent formula UNCHANGED <<semaphore, clientlocks>> works fine.

Incomplete set of initial states

With e.g. EWD998 to N == 2 and Init!3 to /\ color \in [Node -> {"white"}], there should be four initial states, but there are only three.

Support CASE construct

Implement support for the CASE construct.

Short-circuit evaluation in conjunctions

Repro for disjunct: type TRUE \/ <<"a">>[2] = "b" in the REPL.

Expected: result TRUE, the second half isn't evaluated.

Actual: no result, "swallowing parse errors during repl evaluation" is logged in the console. The REPL tried to interpret the second half and failed with an index error.

Repro for conjunct: type FALSE /\ <<>>[1] = "a" in the REPL.

Expected: result FALSE, the second half isn't evaluated.

Actual: no result, "swallowing parse errors during repl evaluation" is logged in the console. The REPL tried to interpret the second half and failed with an index error.

Consider Github.dev as the frontend

See tlaplus/vscode-tlaplus#239

Support module semantics

For the use cases I envision, I was not planning to implement full blown semantics of modules and module imports e.g. EXTENDS, etc. For example, for now I'm just considering operators from the standard modules to be globally available at all times, even without being explicitly imported. This behavior could be re-considered in the future, though, if necessary.

Display action names with next state choices

Parse and display action names when choosing next states.

Use fields instead of indexes to address children

Super impressed with this! Just letting you know in case you weren't aware - you can use fields instead of indexes to address specific child nodes. I admit I've been pretty lazy about adding fields to the grammar because they aren't very useful in highlighting, but if this would be useful to you I would be happy to add the missing ones according to whatever scheme is most helpful.

What license is this released under?

...most TLA+ projects are released under https://opensource.org/licenses/MIT.

LAMBDA expressions

---- MODULE Issue123 ----

Op(l(_), v) ==
	l(v)

VARIABLE x

Init ==
    x = FALSE
    
Next ==
    x' = Op(LAMBDA v: ~v, x)

Spec == Init /\ [][Next]_x

====

TypeError: Cannot read properties of undefined (reading 'val')
    at evalBoundOp (eval.js:1788:71)
    at evalExpr (eval.js:2070:16)
    at evalExpr (eval.js:2517:15)
    at eval.js:1187:31
    at lodash.min.js:98:241
    at lodash.min.js:54:66
    at ue (lodash.min.js:35:327)
    at Function.Kc [as mapValues] (lodash.min.js:98:213)
    at evalEq (eval.js:1184:30)
    at evalBoundInfix (eval.js:1338:16)

Explicitly defined op doesn't work either:

---- MODULE Issue123 ----
EXTENDS Naturals

Neg(v) ==
   v

Op(l(_), v) ==
	l(v)

VARIABLE x

Init ==
	x = FALSE
    
Next ==
    x' = Op(Neg, x)

Spec == Init /\ [][Next]_x

====

Support ENABLED

Support the ENABLED built-in operator.

Opening trace link loads forever

Opening the following trace link takes forever (spinning wheel next to "root spec") in Edge (Vivaldi) and Safari: https://will62794.github.io/tla-web/#!/home?specpath=https%3A%2F%2Fraw.githubusercontent.com%2Flemmy%2FCCF%2Fmku-ConsistencyMonolith%2Ftla%2Fconsistency%2FConsistency.tla&traceExprs%5B0%5D=AllCommittedObservedRoInv&trace=297cc69b%2Cd0b53816%2Cc64ffa94%2C28d6a04f%2C266f1e96%2C44617b58%2C551598da%2C150d05ea%2C14022610%2C74fe4aa9%2Cae2a49a2%2Cd54bbb48