diff --git a/spec/consensus/proposer-based-timestamp/tla/HowToRun.md b/spec/consensus/proposer-based-timestamp/tla/readme.md
similarity index 92%
rename from spec/consensus/proposer-based-timestamp/tla/HowToRun.md
rename to spec/consensus/proposer-based-timestamp/tla/readme.md
index ba1352c09..ba897207e 100644
--- a/spec/consensus/proposer-based-timestamp/tla/HowToRun.md
+++ b/spec/consensus/proposer-based-timestamp/tla/readme.md
@@ -2,7 +2,7 @@
 
 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. Get Apalache, by following [these](https://apalache.informal.systems/docs/apalache/installation/index.html) instructions. Summarized:
 
     1. `git clone https://github.com/informalsystems/apalache.git`
     2. `make package`
diff --git a/spec/consensus/proposer-based-timestamp/tla/runApalache.sh b/spec/consensus/proposer-based-timestamp/tla/runApalache.sh
index 4e8418a8c..dfd0a8f07 100755
--- a/spec/consensus/proposer-based-timestamp/tla/runApalache.sh
+++ b/spec/consensus/proposer-based-timestamp/tla/runApalache.sh
@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+set -euo pipefail
+
 # Works in all cases except running from jar on Windows 
 EXE=$APALACHE_HOME/bin/apalache-mc
 
@@ -23,12 +25,12 @@ if ! [[ -f "$CFG" ]]; then
   echo "write-intermediate: true" >> $CFG
 fi
 
-if [[ MC ]]; then
-  # Run 3c1f
-  $EXE $CMD $FLAGS MC_PBT_3C_1F.tla  
-else
+if [[ "$MC" = false ]]; then
   # Run 2c2f
   $EXE $CMD $FLAGS MC_PBT_2C_2F.tla  
+else
+  # Run 3c1f
+  $EXE $CMD $FLAGS MC_PBT_3C_1F.tla  
 fi