From 026f378e50ea449ddd5bcf147b5c5d667ce07709 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Fri, 6 May 2022 15:07:20 +0200 Subject: [PATCH] run script/docs --- .../proposer-based-timestamp/tla/HowToRun.md | 26 +++++++ .../proposer-based-timestamp/tla/MC_PBT.tla | 77 ------------------- .../tla/TendermintPBT.tla | 4 +- .../tla/runApalache.sh | 35 +++++++++ 4 files changed, 63 insertions(+), 79 deletions(-) create mode 100644 spec/consensus/proposer-based-timestamp/tla/HowToRun.md delete mode 100644 spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla create mode 100755 spec/consensus/proposer-based-timestamp/tla/runApalache.sh diff --git a/spec/consensus/proposer-based-timestamp/tla/HowToRun.md b/spec/consensus/proposer-based-timestamp/tla/HowToRun.md new file mode 100644 index 000000000..bc1434092 --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/HowToRun.md @@ -0,0 +1,26 @@ +# How to run tests + +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` + +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 + +Example: +```sh +runApalache.sh check 2 +``` +Checks 2 steps of `MC_PBT_3C_1F.tla` and +```sh +runApalache.sh check 10 false +``` +Checks 10 steps of `MC_PBT_2C_2F.tla` diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla deleted file mode 100644 index 53f7336fb..000000000 --- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla +++ /dev/null @@ -1,77 +0,0 @@ ------------------------------ MODULE MC_PBT ------------------------------- -CONSTANT - \* @type: ROUND -> PROCESS; - Proposer - -VARIABLES - \* @type: PROCESS -> ROUND; - round, \* a process round number - \* @type: PROCESS -> STEP; - step, \* a process step - \* @type: PROCESS -> DECISION; - decision, \* process decision - \* @type: PROCESS -> VALUE; - lockedValue, \* a locked value - \* @type: PROCESS -> ROUND; - lockedRound, \* a locked round - \* @type: PROCESS -> PROPOSAL; - validValue, \* a valid value - \* @type: PROCESS -> ROUND; - validRound \* a valid round - -\* time-related variables -VARIABLES - \* @type: PROCESS -> TIME; - localClock, \* a process local clock: Corr -> Ticks - \* @type: TIME; - realTime \* a reference Newtonian real time - -\* book-keeping variables -VARIABLES - \* @type: ROUND -> Set(PROPMESSAGE); - msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages - \* @type: ROUND -> Set(PREMESSAGE); - msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages - \* @type: ROUND -> Set(PREMESSAGE); - msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages - \* @type: Set(MESSAGE); - evidence, \* the messages that were used by the correct processes to make transitions - \* @type: ACTION; - action, \* we use this variable to see which action was taken - \* @type: PROCESS -> Set(PROPMESSAGE); - receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message - \* @type: <> -> TIME; - inspectedProposal \* used to keep track when a process tries to receive a message - -\* Invariant support -VARIABLES - \* @type: ROUND -> TIME; - beginRound, \* the minimum of the local clocks at the time any process entered a new round - \* @type: PROCESS -> TIME; - endConsensus, \* the local time when a decision is made - \* @type: ROUND -> TIME; - lastBeginRound, \* the maximum of the local clocks in each round - \* @type: ROUND -> TIME; - proposalTime, \* the real time when a proposer proposes in a round - \* @type: ROUND -> TIME; - proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round - - -INSTANCE TendermintPBT_002_draft WITH - Corr <- {"c1", "c2"}, - Faulty <- {"f3", "f4"}, - N <- 4, - T <- 1, - ValidValues <- { "v0", "v1" }, - InvalidValues <- {"v2"}, - MaxRound <- 5, - MaxTimestamp <- 10, - MinTimestamp <- 2, - Delay <- 2, - Precision <- 2 - -\* run Apalache with --cinit=CInit -CInit == \* the proposer is arbitrary -- works for safety - Proposer \in [Rounds -> AllProcs] - -============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla index a2ee26d64..edba89c79 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla @@ -870,8 +870,8 @@ IsFirstProposedInRound(prop, src, r) == TimeLiveness == \A r \in Rounds \ {MaxRound}, v \in ValidValues: LET p == Proposer[r] IN - /\ p \in Corr \* Correct process is proposer in round r - /\ + p \in Corr \* Correct process is proposer in round r + => \E t \in Timestamps: LET prop == Proposal(v,t,r) IN ( diff --git a/spec/consensus/proposer-based-timestamp/tla/runApalache.sh b/spec/consensus/proposer-based-timestamp/tla/runApalache.sh new file mode 100755 index 000000000..4e8418a8c --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/runApalache.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash + +# Works in all cases except running from jar on Windows +EXE=$APALACHE_HOME/bin/apalache-mc + +CMD=${1:-typecheck} +N=${2:-10} +MC=${3:-true} +DD=${4:-false} + +SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) +CFG=$SCRIPT_DIR/.apalache.cfg + + +if [[ $1 == "check" ]]; then + FLAGS="--length=$N --inv=Inv --cinit=CInit --discard-disabled=$DD" +else + FLAGS="" +fi + +if ! [[ -f "$CFG" ]]; then + echo "out-dir: \"$SCRIPT_DIR/_apalache-out\"" >> $CFG + echo "write-intermediate: true" >> $CFG +fi + +if [[ MC ]]; then + # Run 3c1f + $EXE $CMD $FLAGS MC_PBT_3C_1F.tla +else + # Run 2c2f + $EXE $CMD $FLAGS MC_PBT_2C_2F.tla +fi + + +