From a80bfb5168db2a1f7825533d51e0a7202ac16115 Mon Sep 17 00:00:00 2001 From: b00f Date: Wed, 5 Apr 2023 00:53:31 +0800 Subject: [PATCH] fix: updating tla+ readme (#443) --- consensus/spec/README.md | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/consensus/spec/README.md b/consensus/spec/README.md index 378c46753..67296e674 100644 --- a/consensus/spec/README.md +++ b/consensus/spec/README.md @@ -1,3 +1,23 @@ -The specification of Pactus consensus algorithm. -More info can be found here: -https://pactus.org/learn/consensus/consensus-mechanism.html +# Consensus specification + +This folder contains the consensus specification for the Pactus blockchain, +which is based on the TLA+ formal language. +The specification defines the consensus algorithm used by the blockchain. + +More info can be found [here](https://pactus.org/learn/consensus/specification/) + +## Model checking + +To run the model checker, you will need to download and install the [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html), +which includes the TLC model checker. Follow the steps below to run the TLC model checker: + +- Add the `Pactus_Liveness.tla` spec to your TLA+ Toolbox project. +- Create a new model and specify the temporal formula as `LiveSpec`. +- Specify the invariants formula as `TypeOK`. +- Specify the properties formula as `Success`. +- Since we are checking for liveness, add the `Constraint` formula as the "State Constraint". +- Define the required constants: + - `NumFaulty`: the number of faulty nodes (e.g. 1) + - `MaxHeight`: the maximum height of the system (e.g. 2) + - `MaxRound`: the maximum round of the consensus algorithm (e.g. 2) +- Run the TLC checker to check the correctness of the specification.