mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-02-11 06:11:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

readme update

Browse Source
This commit is contained in:
Kukovec
2022-05-31 16:28:31 +02:00
parent ae786b6751
commit fefc49fc10
1 changed files with 6 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
spec/consensus/proposer-based-timestamp/tla/readme.md
View File

@@ -16,6 +16,8 @@ The script `runApalache.sh` runs Apalache against one of the model files in this
3. `MC` is a Boolean flag that controls whether the model cehcked has a majoricty of correct processes. Default: true
4. `DD` is a Boolean flag that controls Apalache's `--discard-disabled` flag (See [here](https://apalache.informal.systems/docs/apalache/running.html)). Ignored if `CMD=typecheck`. Default: false
The results will be written to `_apalache-out` (see the [Apalache documentation](https://apalache.informal.systems/docs/adr/009adr-outputs.html)).
Example:
```sh
runApalache.sh check 2
@@ -25,3 +27,7 @@ Checks 2 steps of `MC_PBT_3C_1F.tla` and
runApalache.sh check 10 false
```
Checks 10 steps of `MC_PBT_2C_2F.tla`
# Updating the experiments log
After running a particularly significant test, copy the raw outputs from `_apalache-out` to `experiment_data` and update `experiment_log.md` accordingly.