From 87486a4ef1ee95e29fa0d611466fd0162928af8a Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Thu, 9 May 2024 13:59:23 +0000 Subject: [PATCH] Repro trace and script --- tla/repro.sh | 24 ++++++++++++++++++++++++ tla/trace.ndjson | 49 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 tla/repro.sh create mode 100644 tla/trace.ndjson diff --git a/tla/repro.sh b/tla/repro.sh new file mode 100644 index 000000000000..2810d198da48 --- /dev/null +++ b/tla/repro.sh @@ -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: +# State 44: +# State 45: +# State 46: +# State 47: +# State 48: +# State 49: +# State 50: +# State 51: +# State 52: +$ JSON=trace.ndjson ./tlc.sh consistency/TraceMultiNodeReads.tla | grep State | tail +# State 45: +# State 46: +# State 47: +# State 48: +# State 49: +# State 50: +# State 51: +# State 52: +# State 53: +# State 54: \ No newline at end of file diff --git a/tla/trace.ndjson b/tla/trace.ndjson new file mode 100644 index 000000000000..78852d763ef8 --- /dev/null +++ b/tla/trace.ndjson @@ -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]}