From 16d9b21f8b14477b36a63ec2072cb67563884540 Mon Sep 17 00:00:00 2001 From: Queeny Date: Tue, 8 May 2018 22:32:38 -0700 Subject: [PATCH 1/2] Create README.md --- README.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..045159a --- /dev/null +++ b/README.md @@ -0,0 +1,12 @@ +# tla-plus + +TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems. + +# tla-plus in TiDB + +In TiDB, we use TLA+ for the following purposes: + +- To verify the distributed consensus algorithm - [Raft](https://github.com/pingcap/raft-rs). +- To verify the implementation of distributed transaction. + +For further information about TLA+, see [tla-plus-resources](https://github.com/cmschmtt/tla-plus-resources). From ba6dd5b7072a879b0d2e1886d55ed6bae4f6d337 Mon Sep 17 00:00:00 2001 From: Queeny Date: Tue, 8 May 2018 22:33:19 -0700 Subject: [PATCH 2/2] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 045159a..e4c3ed6 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ TLA+ is a formal specification and verification language to help engineers desig # tla-plus in TiDB -In TiDB, we use TLA+ for the following purposes: +In [TiDB](https://github.com/pingcap/tidb), we use TLA+ for the following purposes: - To verify the distributed consensus algorithm - [Raft](https://github.com/pingcap/raft-rs). - To verify the implementation of distributed transaction.