From cd48156f662af8fc325a6478dfa34de6be0e36c8 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Fri, 6 May 2022 15:10:33 +0200 Subject: [PATCH] formatting --- .../proposer-based-timestamp/tla/HowToRun.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/tla/HowToRun.md b/spec/consensus/proposer-based-timestamp/tla/HowToRun.md index bc1434092..ba1352c09 100644 --- a/spec/consensus/proposer-based-timestamp/tla/HowToRun.md +++ b/spec/consensus/proposer-based-timestamp/tla/HowToRun.md @@ -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