TLA+ Formatter
GitHub
Width
Indent
Loading…
Input
---- MODULE RecordsWithNestedRecordsAndSequences ----- EXTENDS TLC, Sequences CONSTANTS n1, n2, n3 Foo == [action |-> {<<<<1, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))]>>, [name |-> "S!Next", location |-> [beginLine |-> 46, beginColumn |-> 1, endLine |-> 46, endColumn |-> 18, module |-> "MCCRDT"]], <<2, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 1))]>>>>, <<<<2, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 1))]>>, [name |-> "S!Next", location |-> [beginLine |-> 46, beginColumn |-> 1, endLine |-> 46, endColumn |-> 18, module |-> "MCCRDT"]], <<3, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 2))]>>>>}, state |-> {<<1, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))]>>, <<2, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 1))]>>, <<3, [counter |-> (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 2))]>>}] =====
Output
Initializing CheerpJ…