From 24ea13790dc605bc93d2e40ba3bfbd6545d37e59 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Tue, 31 May 2022 15:45:54 +0200 Subject: [PATCH] PR comments --- .../tla/{HowToRun.md => readme.md} | 2 +- .../proposer-based-timestamp/tla/runApalache.sh | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) rename spec/consensus/proposer-based-timestamp/tla/{HowToRun.md => readme.md} (92%) 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