run script/docs

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`

spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla

@@ -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: <<ROUND,PROCESS>> -> 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]
-
-=============================================================================    

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
       (

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
+
+
+