will62794 / tla-web Goto Github PK

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

License: MIT License

HTML 0.94% JavaScript 42.61% TLA 54.27% Shell 0.08% Makefile 0.01% CSS 2.06% C 0.02%

tla-web's Issues

Finite stuttering should be possible?

---- MODULE Foo ----

VARIABLE x

Init == x = TRUE

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

Real-world spec challenge

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

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.

Handle primed expressions correctly

See simple failing spec.

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.

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)

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.

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.

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)
=============================================================================

Support CASE construct

Implement support for the CASE construct.

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>>

====

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.

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.

Encode CONSTANT value settings in URL

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

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.

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!

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.

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.

What license is this released under?

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

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.

Support recursive operators

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

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 >>
   
====

Consider Github.dev as the frontend

See tlaplus/vscode-tlaplus#239

Add additional tests for RECURSIVE operators

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

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.

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.

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.

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.

Multiline-comments between constants are treated as constants

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

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
====

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

Display action names with next state choices

Parse and display action names when choosing next states.

Support ENABLED

Support the ENABLED built-in operator.

Show action details on hover in next state selection

When hovering over an action name in the next-state selection pane, it would be helpful if additional details of that action were shown e.g., the code for that action and/or structured details about the specific set of enabled guards, modified variables, etc.

@muratdem

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

Comments preceding the TLA+ module break the web explorer

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

VARIABLE x

Init ==
	x = 2

Next ==
	x' = 2

=====

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

====

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.

Next-state relation disabled when it is not

---- MODULE Foo ----

VARIABLE x

Init == x = TRUE

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

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

====

Add additional tests for ENABLED construct

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

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

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, ....

will62794 / tla-web Goto Github PK

tla-web's Issues

Recommend Projects

Recommend Topics

Recommend Org