From c8aeb14b835b62820437c312c45da9ffe1d557c0 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Wed, 8 Apr 2020 03:03:43 +0800 Subject: [PATCH] update readme --- DistributedTransaction/README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/DistributedTransaction/README.md b/DistributedTransaction/README.md index 2a1c680..1d4a4b4 100644 --- a/DistributedTransaction/README.md +++ b/DistributedTransaction/README.md @@ -4,7 +4,6 @@ The module contains a abstract specification of the transaction system implement The module contains two TLA+ files: `DistributedTransaction.tla` and `DistributedTransactionProofs.tla`. -In most cases you will only have an interest in `DistributedTransaction.tla`, where the whole specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some proofs, which are supposed to be build up gradually, to the safety invariants. - -To run formal proofs in `DistributedTransactionProofs.tla`, you'd better install [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox. +In most cases you will likely have an interest in only `DistributedTransaction.tla`, where the specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some formal proofs, which are supposed to be build up gradually (so it's not completed yet), to the safety invariants. +To run the formal proofs in `DistributedTransactionProofs.tla`, you'd like to install the [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox.