forked from microsoft/CCF
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
2 changed files
with
73 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| # Run in the same directory as tlc.sh | ||
| # With DFS | ||
| JSON=trace.ndjson JVM_OPTIONS=-Dtlc2.tool.queue.IStateQueue=StateDeque ./tlc.sh consistency/TraceMultiNodeReads.tla | grep State | tail | ||
| # State 43: <IsRoTxResponseAction line 97, col 5 to line 108, col 67 of module TraceMultiNodeReads> | ||
| # State 44: <IsRwTxRequestAction line 50, col 5 to line 55, col 37 of module TraceMultiNodeReads> | ||
| # State 45: <BackfillLedgerBranch line 128, col 5 to line 141, col 24 of module TraceMultiNodeReads> | ||
| # State 46: <IsRwTxExecuteAction line 58, col 5 to line 68, col 67 of module TraceMultiNodeReads> | ||
| # State 47: <IsRwTxResponseAction line 71, col 5 to line 77, col 43 of module TraceMultiNodeReads> | ||
| # State 48: <IsStatusInvalidResponseAction line 111, col 5 to line 117, col 43 of module TraceMultiNodeReads> | ||
| # State 49: <IsRwTxRequestAction line 50, col 5 to line 55, col 37 of module TraceMultiNodeReads> | ||
| # State 50: <BackfillLedgerBranches line 144, col 5 to line 155, col 24 of module TraceMultiNodeReads> | ||
| # State 51: <BackfillLedgerBranch line 128, col 5 to line 141, col 24 of module TraceMultiNodeReads> | ||
| # State 52: <IsRwTxExecuteAction line 58, col 5 to line 68, col 67 of module TraceMultiNodeReads> | ||
| $ JSON=trace.ndjson ./tlc.sh consistency/TraceMultiNodeReads.tla | grep State | tail | ||
| # State 45: <BackfillLedgerBranch line 128, col 5 to line 141, col 24 of module TraceMultiNodeReads> | ||
| # State 46: <IsRwTxExecuteAction line 58, col 5 to line 68, col 67 of module TraceMultiNodeReads> | ||
| # State 47: <IsRwTxResponseAction line 71, col 5 to line 77, col 43 of module TraceMultiNodeReads> | ||
| # State 48: <IsStatusInvalidResponseAction line 111, col 5 to line 117, col 43 of module TraceMultiNodeReads> | ||
| # State 49: <IsRwTxRequestAction line 50, col 5 to line 55, col 37 of module TraceMultiNodeReads> | ||
| # State 50: <BackfillLedgerBranches line 144, col 5 to line 155, col 24 of module TraceMultiNodeReads> | ||
| # State 51: <BackfillLedgerBranch line 128, col 5 to line 141, col 24 of module TraceMultiNodeReads> | ||
| # State 52: <IsRwTxExecuteAction line 58, col 5 to line 68, col 67 of module TraceMultiNodeReads> | ||
| # State 53: <IsRwTxResponseAction line 71, col 5 to line 77, col 43 of module TraceMultiNodeReads> | ||
| # State 54: <IsStatusCommittedResponseAction line 80, col 5 to line 86, col 43 of module TraceMultiNodeReads> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,49 @@ | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 0} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [2, 29], "tx": 0} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 0, "tx_id": [2, 29]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [2, 29], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 1} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 1, "tx_id": [2, 30]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 2} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [2, 31], "tx": 2} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 2, "tx_id": [2, 31]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [2, 31], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 3} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 3, "tx_id": [2, 33]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 4} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [2, 34], "tx": 4} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 4, "tx_id": [2, 34]} | ||
| {"action": "StatusInvalidResponseAction", "type": "TxStatusReceived", "tx_id": [2, 34], "status": "InvalidStatus"} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 5} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [3, 36], "tx": 5} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 5, "tx_id": [3, 36]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [3, 36], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 7} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 7, "tx_id": [3, 37]} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 8} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 8, "tx_id": [3, 37]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 9} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [4, 38], "tx": 9} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 9, "tx_id": [4, 38]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [4, 38], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 10} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 10, "tx_id": [4, 39]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 11} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [4, 40], "tx": 11} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 11, "tx_id": [4, 40]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [4, 40], "status": "CommittedStatus"} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 12} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [4, 42], "tx": 12} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 12, "tx_id": [4, 42]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [4, 42], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 13} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 13, "tx_id": [4, 44]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 14} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [4, 45], "tx": 14} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 14, "tx_id": [4, 45]} | ||
| {"action": "StatusCommittedResponseAction", "type": "TxStatusReceived", "tx_id": [4, 45], "status": "CommittedStatus"} | ||
| {"action": "RoTxRequestAction", "type": "RoTxRequest", "tx": 15} | ||
| {"action": "RoTxResponseAction", "type": "RoTxResponse", "tx": 15, "tx_id": [4, 46]} | ||
| {"action": "RwTxRequestAction", "type": "RwTxRequest", "tx": 16} | ||
| {"action": "RwTxExecuteAction", "type": "RwTxExecute", "tx_id": [4, 47], "tx": 16} | ||
| {"action": "RwTxResponseAction", "type": "RwTxResponse", "tx": 16, "tx_id": [4, 47]} |