mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-05-21 22:51:30 +00:00
Code Issues Packages Projects Releases Wiki Activity

formatting

Browse Source
This commit is contained in:
Kukovec
2022-05-06 15:10:33 +02:00
parent 026f378e50
commit cd48156f66
1 changed files with 9 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
spec/consensus/proposer-based-timestamp/tla/HowToRun.md
View File

@@ -2,18 +2,19 @@
The script `runApalache.sh` runs Apalache against one of the model files in this repository. This document describes how to use it.
1. Get Apalache, by following [these](https://apalache.informal.systems/docs/apalache/installation/index.html) instructions.
TLDR (recommended: build from source):
1. `git clone https://github.com/informalsystems/apalache.git`
2. `make package`
1. Get Apalache, by following [these](https://apalache.informal.systems/docs/apalache/installation/index.html) instructions. TLDR (recommended: build from source):
1. `git clone https://github.com/informalsystems/apalache.git`
2. `make package`
2. Define an environment variable `APALACHE_HOME` and set it to the directory where you cloned the repository (resp. unpacked the prebuilt release). `$APALACHE_HOME/bin/apalache-mc` should point to the run script.
3. Call `runApalache.sh CMD N CM DD` where:
1. `CMD` is the command. Either "check" or "typecheck". Default: "typecheck"
2. `N` is the number of steps if `CMD=check`. Ignored if `CMD=typecheck`. Default: 10
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
1. `CMD` is the command. Either "check" or "typecheck". Default: "typecheck"
2. `N` is the number of steps if `CMD=check`. Ignored if `CMD=typecheck`. Default: 10
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
Example:
```sh