From e0e967aa1c00e3fee947db7a39168a93cea0c51f Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 24 Oct 2024 10:47:08 +0200
Subject: [PATCH 01/15] introduce initial conditions with InitAccountableSafety

---
 spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla |  7 +++--
 spec4b-optimizations/MC_ffg_b3_ffg5_v12.tla | 29 ++++++++++++++++-----
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla b/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
index efd9344..6a618c1 100644
--- a/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
+++ b/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
@@ -59,7 +59,6 @@ IndInit ==
         /\ fork_number \in -MAX_BLOCK_BODY..0
         /\ chain2_fork_block_number = fork_number
     /\ justified_checkpoints = Gen(5)
-    /\ InitAccountableSafety
     /\ IndInv
 
 IndInit_C1 ==
@@ -82,8 +81,12 @@ IndInit_C1 ==
       /\ ffg_votes = Gen(5) \* must be >= 4 to observe disagreement
       /\ votes = Gen(12)    \* must be >= 12 to observe disagreement
       /\ justified_checkpoints = Gen(5)
-      /\ InitAccountableSafety
       /\ VotesInv
       /\ CheckpointsInv
 
+\* restrict the initial condition to have accountable safety
+IndInit_C1_AS ==
+    /\ IndInit_C1
+    /\ InitAccountableSafety
+
 =============================================================================
diff --git a/spec4b-optimizations/MC_ffg_b3_ffg5_v12.tla b/spec4b-optimizations/MC_ffg_b3_ffg5_v12.tla
index 7135372..a91da8d 100644
--- a/spec4b-optimizations/MC_ffg_b3_ffg5_v12.tla
+++ b/spec4b-optimizations/MC_ffg_b3_ffg5_v12.tla
@@ -68,11 +68,16 @@ IndInit_C1 ==
       /\ ffg_votes = Gen(5) \* must be >= 4 to observe disagreement
       /\ votes = Gen(12)    \* must be >= 12 to observe disagreement
       /\ justified_checkpoints = Gen(5)
-      \*/\ InitAccountableSafety
       /\ VotesInv
-      /\ CheckpointsApproxInv
-      \*/\ CheckpointsInv
+      /\ CheckpointsInv
+      \*/\ CheckpointsApproxInv
 
+\* restrict the initial condition to have accountable safety
+IndInit_C1_AS ==
+    /\ IndInit_C1
+    /\ InitAccountableSafety
+
+\* a very restricted initial condition
 IndInit_C1_1_2_3_4 ==
     (*
            / [+1] - [+2]
@@ -121,10 +126,14 @@ IndInit_C2 ==
       /\ ffg_votes = Gen(5) \* must be >= 4 to observe disagreement
       /\ votes = Gen(12)    \* must be >= 12 to observe disagreement
       /\ justified_checkpoints = Gen(5)
-      /\ InitAccountableSafety
       /\ VotesInv
       /\ CheckpointsInv
 
+\* restrict the initial condition to have accountable safety
+IndInit_C2_AS ==
+    /\ IndInit_C2
+    /\ InitAccountableSafety
+
 IndInit_C3 ==
     (*
                   / [+2]
@@ -147,10 +156,14 @@ IndInit_C3 ==
       /\ ffg_votes = Gen(5) \* must be >= 4 to observe disagreement
       /\ votes = Gen(12)    \* must be >= 12 to observe disagreement
       /\ justified_checkpoints = Gen(5)
-      /\ InitAccountableSafety
       /\ VotesInv
       /\ CheckpointsInv
 
+\* restrict the initial condition to have accountable safety
+IndInit_C3_AS ==
+    /\ IndInit_C3
+    /\ InitAccountableSafety
+
 IndInit_C4 ==
     (*
            / [+1] - [+2]
@@ -173,8 +186,12 @@ IndInit_C4 ==
       /\ ffg_votes = Gen(5) \* must be >= 4 to observe disagreement
       /\ votes = Gen(12)    \* must be >= 12 to observe disagreement
       /\ justified_checkpoints = Gen(5)
-      /\ InitAccountableSafety
       /\ VotesInv
       /\ CheckpointsInv
 
+\* restrict the initial condition to have accountable safety
+IndInit_C4_AS ==
+    /\ IndInit_C4
+    /\ InitAccountableSafety
+
 =============================================================================
\ No newline at end of file

From 0239d74e38a3b047bc0bf6f9075409177aa9ba19 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 24 Oct 2024 10:53:48 +0200
Subject: [PATCH 02/15] add a script to run them all

---
 spec4b-optimizations/exp.csv            | 10 ++++++++++
 spec4b-optimizations/run-experiments.sh |  5 +++++
 2 files changed, 15 insertions(+)
 create mode 100644 spec4b-optimizations/exp.csv
 create mode 100755 spec4b-optimizations/run-experiments.sh

diff --git a/spec4b-optimizations/exp.csv b/spec4b-optimizations/exp.csv
new file mode 100644
index 0000000..10e6936
--- /dev/null
+++ b/spec4b-optimizations/exp.csv
@@ -0,0 +1,10 @@
+MC_ffg_b1_ffg5_v12.tla,IndInit_C1_SA,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C1_SA,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C2_SA,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C3_SA,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4_SA,AccountableSafety
+MC_ffg_b1_ffg5_v12.tla,IndInit_C1,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C1,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C2,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C3,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4,AccountableSafety
\ No newline at end of file
diff --git a/spec4b-optimizations/run-experiments.sh b/spec4b-optimizations/run-experiments.sh
new file mode 100755
index 0000000..2638929
--- /dev/null
+++ b/spec4b-optimizations/run-experiments.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+parallel --joblog joblog.txt --results out/ --colsep ',' \
+    -a exp.csv \
+    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" apalache-mc check --init={2} --inv={3} {1}
\ No newline at end of file

From 327aa9a4fe0eb63d790b826b910b9f75c2ccd4bc Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 24 Oct 2024 08:59:50 +0000
Subject: [PATCH 03/15] fix the experiments script

---
 spec4b-optimizations/run-experiments.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/spec4b-optimizations/run-experiments.sh b/spec4b-optimizations/run-experiments.sh
index 2638929..1466a74 100755
--- a/spec4b-optimizations/run-experiments.sh
+++ b/spec4b-optimizations/run-experiments.sh
@@ -1,5 +1,10 @@
 #!/usr/bin/env bash
 
+if [ "$APALACHE_HOME" == "" ]; then
+    echo "set APALACHE_HOME to the Apalache installation directory"
+    exit 1
+fi
+
 parallel --joblog joblog.txt --results out/ --colsep ',' \
     -a exp.csv \
-    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" apalache-mc check --init={2} --inv={3} {1}
\ No newline at end of file
+    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" ${APALACHE_HOME}/bin/apalache-mc check --init={2} --inv={3} {1}

From 2c9073a562e35e7c9504ee76d58125f602cb1761 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 24 Oct 2024 09:00:14 +0000
Subject: [PATCH 04/15] fix the experiments names

---
 spec4b-optimizations/exp.csv | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/spec4b-optimizations/exp.csv b/spec4b-optimizations/exp.csv
index 10e6936..fa9c90b 100644
--- a/spec4b-optimizations/exp.csv
+++ b/spec4b-optimizations/exp.csv
@@ -1,10 +1,10 @@
-MC_ffg_b1_ffg5_v12.tla,IndInit_C1_SA,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C1_SA,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C2_SA,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C3_SA,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C4_SA,AccountableSafety
+MC_ffg_b1_ffg5_v12.tla,IndInit_C1_AS,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C1_AS,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C2_AS,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C3_AS,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4_AS,AccountableSafety
 MC_ffg_b1_ffg5_v12.tla,IndInit_C1,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C1,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C2,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C3,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C4,AccountableSafety
\ No newline at end of file
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4,AccountableSafety

From 7d161b6d75da0c00dc59719776cb0fcc91553cc0 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 12:26:20 +0200
Subject: [PATCH 05/15] add experiments to check inductiveness

---
 ...n-experiments.sh => check-accountable-safety.sh} |  4 +++-
 spec4b-optimizations/check-inductive.sh             | 13 +++++++++++++
 .../{exp.csv => experiments-accountable-safety.csv} |  2 +-
 spec4b-optimizations/experiments-inductive.csv      |  7 +++++++
 4 files changed, 24 insertions(+), 2 deletions(-)
 rename spec4b-optimizations/{run-experiments.sh => check-accountable-safety.sh} (76%)
 create mode 100755 spec4b-optimizations/check-inductive.sh
 rename spec4b-optimizations/{exp.csv => experiments-accountable-safety.csv} (90%)
 create mode 100644 spec4b-optimizations/experiments-inductive.csv

diff --git a/spec4b-optimizations/run-experiments.sh b/spec4b-optimizations/check-accountable-safety.sh
similarity index 76%
rename from spec4b-optimizations/run-experiments.sh
rename to spec4b-optimizations/check-accountable-safety.sh
index 1466a74..afcb224 100755
--- a/spec4b-optimizations/run-experiments.sh
+++ b/spec4b-optimizations/check-accountable-safety.sh
@@ -1,4 +1,6 @@
 #!/usr/bin/env bash
+#
+# Run the experiments to check accountable safety.
 
 if [ "$APALACHE_HOME" == "" ]; then
     echo "set APALACHE_HOME to the Apalache installation directory"
@@ -6,5 +8,5 @@ if [ "$APALACHE_HOME" == "" ]; then
 fi
 
 parallel --joblog joblog.txt --results out/ --colsep ',' \
-    -a exp.csv \
+    -a experiments-accountable-safety.csv \
     /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" ${APALACHE_HOME}/bin/apalache-mc check --init={2} --inv={3} {1}
diff --git a/spec4b-optimizations/check-inductive.sh b/spec4b-optimizations/check-inductive.sh
new file mode 100755
index 0000000..54cd325
--- /dev/null
+++ b/spec4b-optimizations/check-inductive.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+#
+# Run the experiments to check inductiveness.
+
+if [ "$APALACHE_HOME" == "" ]; then
+    echo "set APALACHE_HOME to the Apalache installation directory"
+    exit 1
+fi
+
+parallel --joblog joblog.txt --results out/ --colsep ',' \
+    -a experiments-inductive.csv \
+    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" \
+    ${APALACHE_HOME}/bin/apalache-mc check --init={2} --length={3} --inv={4} {1}
diff --git a/spec4b-optimizations/exp.csv b/spec4b-optimizations/experiments-accountable-safety.csv
similarity index 90%
rename from spec4b-optimizations/exp.csv
rename to spec4b-optimizations/experiments-accountable-safety.csv
index fa9c90b..6a76f5a 100644
--- a/spec4b-optimizations/exp.csv
+++ b/spec4b-optimizations/experiments-accountable-safety.csv
@@ -7,4 +7,4 @@ MC_ffg_b1_ffg5_v12.tla,IndInit_C1,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C1,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C2,AccountableSafety
 MC_ffg_b3_ffg5_v12.tla,IndInit_C3,AccountableSafety
-MC_ffg_b3_ffg5_v12.tla,IndInit_C4,AccountableSafety
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4,AccountableSafety
\ No newline at end of file
diff --git a/spec4b-optimizations/experiments-inductive.csv b/spec4b-optimizations/experiments-inductive.csv
new file mode 100644
index 0000000..7b1ae17
--- /dev/null
+++ b/spec4b-optimizations/experiments-inductive.csv
@@ -0,0 +1,7 @@
+MC_ffg_b1_ffg5_v12.tla,IndInit_C1,1,IndInv
+MC_ffg_b1_ffg5_v12.tla,Init,0,IndInv
+MC_ffg_b3_ffg5_v12.tla,IndInit_C1,1,IndInv
+MC_ffg_b3_ffg5_v12.tla,IndInit_C2,1,IndInv
+MC_ffg_b3_ffg5_v12.tla,IndInit_C3,1,IndInv
+MC_ffg_b3_ffg5_v12.tla,IndInit_C4,1,IndInv
+MC_ffg_b3_ffg5_v12.tla,Init,0,IndInv
\ No newline at end of file

From 47ebeebef2b70c4428f7bbfb73047c340a27f4ff Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 12:27:07 +0200
Subject: [PATCH 06/15] add length=0

---
 spec4b-optimizations/check-accountable-safety.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/spec4b-optimizations/check-accountable-safety.sh b/spec4b-optimizations/check-accountable-safety.sh
index afcb224..f3609de 100755
--- a/spec4b-optimizations/check-accountable-safety.sh
+++ b/spec4b-optimizations/check-accountable-safety.sh
@@ -9,4 +9,5 @@ fi
 
 parallel --joblog joblog.txt --results out/ --colsep ',' \
     -a experiments-accountable-safety.csv \
-    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" ${APALACHE_HOME}/bin/apalache-mc check --init={2} --inv={3} {1}
+    /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" \
+    ${APALACHE_HOME}/bin/apalache-mc check --length=0 --init={2} --inv={3} {1}

From 4337fbcccdfd12b69ea2807b09cc19d87e95568c Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 12:28:26 +0200
Subject: [PATCH 07/15] fix joblog

---
 spec4b-optimizations/check-accountable-safety.sh | 2 +-
 spec4b-optimizations/check-inductive.sh          | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec4b-optimizations/check-accountable-safety.sh b/spec4b-optimizations/check-accountable-safety.sh
index f3609de..5d3d586 100755
--- a/spec4b-optimizations/check-accountable-safety.sh
+++ b/spec4b-optimizations/check-accountable-safety.sh
@@ -7,7 +7,7 @@ if [ "$APALACHE_HOME" == "" ]; then
     exit 1
 fi
 
-parallel --joblog joblog.txt --results out/ --colsep ',' \
+parallel --joblog joblog-as.txt --results out/ --colsep ',' \
     -a experiments-accountable-safety.csv \
     /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" \
     ${APALACHE_HOME}/bin/apalache-mc check --length=0 --init={2} --inv={3} {1}
diff --git a/spec4b-optimizations/check-inductive.sh b/spec4b-optimizations/check-inductive.sh
index 54cd325..c87cf4f 100755
--- a/spec4b-optimizations/check-inductive.sh
+++ b/spec4b-optimizations/check-inductive.sh
@@ -7,7 +7,7 @@ if [ "$APALACHE_HOME" == "" ]; then
     exit 1
 fi
 
-parallel --joblog joblog.txt --results out/ --colsep ',' \
+parallel --joblog joblog-inductive.txt --results out/ --colsep ',' \
     -a experiments-inductive.csv \
     /usr/bin/time -f "'%Uuser %Ssystem %elapsed %Mmaxk'" \
     ${APALACHE_HOME}/bin/apalache-mc check --init={2} --length={3} --inv={4} {1}

From 25f69295c9964491a0607112192cc85695bd4ded Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 12:33:42 +0200
Subject: [PATCH 08/15] update the init predicate

---
 spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla | 1 +
 1 file changed, 1 insertion(+)

diff --git a/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla b/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
index 6a618c1..d543750 100644
--- a/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
+++ b/spec4b-optimizations/MC_ffg_b1_ffg5_v12.tla
@@ -71,6 +71,7 @@ IndInit_C1 ==
       LET b1 == [ body |-> 1, slot |-> i ]
           b2 == [ body |-> -1, slot |-> j ]
       IN
+      /\ 0 < i /\ 0 < j
       /\ all_blocks = { GenesisBlock, b1, b2 }
       /\ chain1 = { GenesisBlock, b1 }
       /\ chain1_tip = b1

From af0f938754efe93d5a606c13c1c1b95ee90cbbad Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 12:39:08 +0200
Subject: [PATCH 09/15] refer to the scripts

---
 EXPERIMENTS.md | 47 +++++------------------------------------------
 1 file changed, 5 insertions(+), 42 deletions(-)

diff --git a/EXPERIMENTS.md b/EXPERIMENTS.md
index 51f5013..707800c 100644
--- a/EXPERIMENTS.md
+++ b/EXPERIMENTS.md
@@ -397,50 +397,13 @@ This experiment took 19 hours 48 min 29 sec.
 
 ## 7. Induction checking with Spec 4b
 
-### 7.1. Checking Accountable Safety for M3
+We ran the experiments using the following scripts:
 
-```sh
-$ apalache-mc check --length=0 --init=IndInit_C1 \
-  --inv=AccountableSafety MC_ffg_b1_ffg5_v12.tla
-```
-
-This experiment took XXX sec.
-
-### 7.2. Checking Accountable Safety for M4a
-
-```sh
-$ apalache-mc check --length=0 --init=IndInit_C4 \
-  --inv=AccountableSafety MC_ffg_b3_ffg5_v12.tla
-```
-
-This experiment took XXX sec.
-
-### 7.3. Checking Accountable Safety for M4b
-
-```sh
-$ apalache-mc check --length=0 --init=IndInit_C2 \
-  --inv=AccountableSafety MC_ffg_b3_ffg5_v12.tla
-```
-
-This experiment took XXX sec.
-
-### 7.4. Checking Accountable Safety for M5a
-
-```sh
-$ apalache-mc check --length=0 --init=IndInit_C1 \
-  --inv=AccountableSafety MC_ffg_b3_ffg5_v12.tla
-```
-
-This experiment took XXX sec.
-
-### 7.5. Checking Accountable Safety for M5b
-
-```sh
-$ apalache-mc check --length=0 --init=IndInit_C3 \
-  --inv=AccountableSafety MC_ffg_b3_ffg5_v12.tla
-```
+ - [check-inductive.sh](./spec4b-optimizations/check-inductive.sh)
+   to check inductiveness of our invariants.
 
-This experiment took XXX sec.
+ - [check-accountable-safety.sh](./spec4b-optimizations/check-accountable-safety.sh)
+   to check accountable safety against the inductive invariant.
 
 
 [Apalache]: https://apalache-mc.org/

From 9088211b8b3d159a7c38804a6a8501f32a2e8760 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 13:34:39 +0200
Subject: [PATCH 10/15] updating the experimental results

---
 EXPERIMENTS.md     | 11 +++++++
 reports/spec3.tex  | 15 ++++-----
 reports/spec4.tex  |  2 +-
 reports/spec4b.tex | 77 +++++++++++++++++++++++++++++++++++++++++-----
 4 files changed, 89 insertions(+), 16 deletions(-)

diff --git a/EXPERIMENTS.md b/EXPERIMENTS.md
index 707800c..8d5e38c 100644
--- a/EXPERIMENTS.md
+++ b/EXPERIMENTS.md
@@ -405,6 +405,17 @@ We ran the experiments using the following scripts:
  - [check-accountable-safety.sh](./spec4b-optimizations/check-accountable-safety.sh)
    to check accountable safety against the inductive invariant.
 
+The table below summarizes the experiments with inductiveness checking.
+
+| Instance               | Init     | Invariant | Memory | Time       |
+|------------------------|----------|-----------|--------|------------|
+| MC_ffg_b1_ffg5_v12     | Init     | IndInv    | 580 MB | 7s         |
+| MC_ffg_b3_ffg5_v12     | Init     | IndInv    | 700 MB | 7s         |
+| MC_ffg_b1_ffg5_v12     | Init_C1  | IndInv    | 1.4 GB | 2min 8s    |
+| MC_ffg_b3_ffg5_v12     | Init_C1  | IndInv    | 1.8 GB | 19min 10s  |
+| MC_ffg_b3_ffg5_v12     | Init_C2  | IndInv    | 1.6 GB | 13min 16s  |
+| MC_ffg_b3_ffg5_v12     | Init_C3  | IndInv    | 1.6 GB | 17min 39s  |
+| MC_ffg_b3_ffg5_v12     | Init_C4  | IndInv    | 1.6 GB | 16min 23s  |
 
 [Apalache]: https://apalache-mc.org/
 [Apalache installation]: https://apalache-mc.org/docs/apalache/installation/index.html
diff --git a/reports/spec3.tex b/reports/spec3.tex
index 4253915..33319a3 100644
--- a/reports/spec3.tex
+++ b/reports/spec3.tex
@@ -2,10 +2,10 @@
 
 \section{\SpecThree{}: Adding a state machine}\label{sec:spec3}
 
-In the course of writing \texttt{Spec 2}, we realized
+In the course of writing~\SpecTwo{}, we realized
 that the executable Python specification is essentially sequential. In other
 words, even though the 3SF algorithm is distributed, its Python
-specification as well as \texttt{Spec 1} and \texttt{Spec 2} are encoding
+specification as well as~\SpecOne{} and~\SpecTwo{} are encoding
 all possible protocol states in a single specification state.
 
 \subsection{State machines in \tlap{}}
@@ -32,7 +32,7 @@ \subsection{State machines in \tlap{}}
 
 \subsection{Introducing a state machine}
 
-Having the observations above in mind, we introduce \texttt{Spec 3} in which we
+Having the observations above in mind, we introduce~\SpecThree{} in which we
 specify a state machine that incrementally builds possible protocol states by
 constructing the following data structures:
 
@@ -77,7 +77,7 @@ \subsection{Introducing a state machine}
 \begin{figure}
     \centering
     \includegraphics[width=\textwidth]{images/abstract-ffg-next.pdf}  % Include the PDF file
-    \caption{The transition predicate of Spec 3}\label{fig:abstract-ffg-next}
+    \caption{The transition predicate of~\SpecThree{}}\label{fig:abstract-ffg-next}
 \end{figure}
 
 \subsection{Model checking experiments}
@@ -113,8 +113,8 @@ \subsection{Model checking experiments}
             \\ \midrule
         \texttt{check}
             & $\textit{ExistTwoFinalizedConflictingBlocks}$
-            & N
-            & 1h 27min
+            & 6
+            & 52min
             \\ \midrule
         \texttt{simulate}
             & $\textit{AccountableSafety}$
@@ -127,6 +127,7 @@ \subsection{Model checking experiments}
             & N
             \\ \bottomrule
     \end{tabular}
-    \caption{Model checking experiments with Spec 3}\label{tab:abstract-ffg-mc}
+    \caption{Model checking experiments
+             with~\SpecThree{}}\label{tab:abstract-ffg-mc}
 \end{table}
 
diff --git a/reports/spec4.tex b/reports/spec4.tex
index 781c077..787a0cd 100644
--- a/reports/spec4.tex
+++ b/reports/spec4.tex
@@ -92,7 +92,7 @@ \subsection{Model checking experiments}
             \bottomrule
     \end{tabular}
     \caption{Model checking experiments
-        with~\SpecFourB{} on the instance~\texttt{MC\_ffg\_b3\_ffg5\_v12}
+        with~\SpecFour{} on the instance~\texttt{MC\_ffg\_b3\_ffg5\_v12}
     }\label{tab:spec4-experiments}
 \end{table}
 
diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index fc5b051..3d14c22 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -94,14 +94,18 @@ \subsection{Decomposition of chain configurations}\label{sec:decomposition}
 
 \subsection{Model checking experiments}
 
-Table~\ref{tab:spec4b-experiments} summarizes our experiments with Apalache for
-various configurations. One interesting effect of the optimizations,
-especially of the ones presented in Section~\ref{sec:decomposition}, is
-a significant drop in the memory consumption of the SMT solver. In our
-experiments, Z3 required from 700~MB to 1.5~GB\@. While this is still a factor of
-20 in comparison to the Alloy experiments in Section~\ref{sec:alloy}, this is
-significantly better than our initial experiments with~\SpecTwo{}
-and~\SpecThree{}, which required up to 20~GB of RAM\@.
+Tables~\ref{tab:spec4b-experiments} and~\ref{tab:spec4b-inductiveness}
+summarizes our experiments with Apalache for various configurations. One
+interesting effect of the optimizations, especially of the ones presented in
+Section~\ref{sec:decomposition}, is a significant drop in the memory
+consumption of the SMT solver. In our experiments, Z3 required from 700~MB to
+1.5~GB\@. While this is still a factor of 20 in comparison to the Alloy
+experiments in Section~\ref{sec:alloy}, this is significantly better than our
+initial experiments with~\SpecTwo{} and~\SpecThree{}, which required up to
+20~GB of RAM\@. Interestingly, inductiveness checks in
+Table~\ref{tab:spec4b-inductiveness} take significantly longer than in the case
+of~\SpecFour{}. We conjecture that this is caused by the need to check more
+specialized graphs in conjunction with steps.
 
 We notice significant variations in the running times on different
 configurations. This is probably due to the effect of different runs of the Z3
@@ -154,3 +158,60 @@ \subsection{Model checking experiments}
              against~\SpecFourB{}}\label{tab:spec4b-experiments}
 \end{table}
 
+\begin{table}
+    \centering
+    \begin{tabular}{lllrr}
+        \tbh{Instance}
+            & \tbh{Init}
+            & \tbh{Invariant}
+            & \tbh{Memory}
+            & \tbh{Time}
+            \\ \toprule
+        \texttt{MC\_ffg\_b1\_ffg5\_v12}
+            & \texttt{Init}
+            & \texttt{IndInv}
+            & 580 MB
+            & 7s
+            \\
+        \texttt{MC\_ffg\_b3\_ffg5\_v12}
+            & \texttt{Init}
+            & \texttt{IndInv}
+            & 700 MB
+            & 7s
+            \\
+        \texttt{MC\_ffg\_b1\_ffg5\_v12}
+            & \texttt{Init\_C1}
+            & \texttt{IndInv}
+            & 1.4 GB
+            & 2min 8s
+            \\
+        \texttt{MC\_ffg\_b3\_ffg5\_v12}
+            & \texttt{Init\_C1}
+            & \texttt{IndInv}
+            & 1.8 GB
+            & 19min 10s
+            \\
+        \texttt{MC\_ffg\_b3\_ffg5\_v12}
+            & \texttt{Init\_C2}
+            & \texttt{IndInv}
+            & 1.6 GB
+            & 13min 16s
+            \\
+        \texttt{MC\_ffg\_b3\_ffg5\_v12}
+            & \texttt{Init\_C3}
+            & \texttt{IndInv}
+            &  1.6 GB
+            & 17min 39s
+            \\
+        \texttt{MC\_ffg\_b3\_ffg5\_v12}
+            & \texttt{Init\_C4}
+            & \texttt{IndInv}
+            & 1.6 GB
+            & 16min 23s
+            \\
+            \bottomrule
+    \end{tabular}
+    \caption{Checking inductiveness
+             for~\SpecFourB{}}\label{tab:spec4b-inductiveness}
+\end{table}
+

From 2f36fef42f4771933cdfb266cd4e90f1a7e6a7dc Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 26 Oct 2024 14:46:34 +0200
Subject: [PATCH 11/15] small fix

---
 reports/spec4b.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index 3d14c22..6084eb0 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -111,7 +111,7 @@ \subsection{Model checking experiments}
 configurations. This is probably due to the effect of different runs of the Z3
 SMT solve having great variety of running times, which is well-known in the
 computer-aided community. To further confirm these variations, we could run
-multiple experiments with `hyperfine`.
+multiple experiments with~\texttt{hyperfine}.
 
 \begin{table}
     \centering

From bc1684070ad92ebd9adb3e59d7a8a4be118ab2c6 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sun, 27 Oct 2024 09:07:26 +0100
Subject: [PATCH 12/15] update the figures

---
 reports/spec3.tex  | 2 +-
 reports/spec4b.tex | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/reports/spec3.tex b/reports/spec3.tex
index 33319a3..26d665a 100644
--- a/reports/spec3.tex
+++ b/reports/spec3.tex
@@ -124,7 +124,7 @@ \subsection{Model checking experiments}
         \texttt{check}
             & $\textit{AccountableSafety}$
             & 6
-            & N
+            & 16h 13min
             \\ \bottomrule
     \end{tabular}
     \caption{Model checking experiments
diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index 6084eb0..314cd66 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -109,9 +109,9 @@ \subsection{Model checking experiments}
 
 We notice significant variations in the running times on different
 configurations. This is probably due to the effect of different runs of the Z3
-SMT solve having great variety of running times, which is well-known in the
-computer-aided community. To further confirm these variations, we could run
-multiple experiments with~\texttt{hyperfine}.
+SMT solve having great variation of running times, which is well-known in the
+community of computer-aided verification. To further confirm these variations,
+we could run multiple experiments with~\texttt{hyperfine}.
 
 \begin{table}
     \centering

From f506ac91e39cd0bac67f3fd4431738a8cf42d733 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 1 Nov 2024 14:58:59 +0100
Subject: [PATCH 13/15] update the experiment figures

---
 reports/spec4.tex  |  5 +++--
 reports/spec4b.tex | 11 ++++++-----
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/reports/spec4.tex b/reports/spec4.tex
index 787a0cd..1e8fcb5 100644
--- a/reports/spec4.tex
+++ b/reports/spec4.tex
@@ -86,13 +86,14 @@ \subsection{Model checking experiments}
             & \texttt{Next}
             & \texttt{AccountableSafety}
             & 0
-            & XXX
-            & XXX
+            & 1.5 GB
+            & TO ($> 6$d)
             \\
             \bottomrule
     \end{tabular}
     \caption{Model checking experiments
         with~\SpecFour{} on the instance~\texttt{MC\_ffg\_b3\_ffg5\_v12}
+        (``TO'' means timeout)
     }\label{tab:spec4-experiments}
 \end{table}
 
diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index 314cd66..27755f8 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -131,8 +131,8 @@ \subsection{Model checking experiments}
         M4a: Fig.~\ref{fig:four-top}
             & \texttt{MC\_ffg\_b3\_ffg5\_v12}
             & \texttt{Init\_C4}
-            & XXX
-            & XXX
+            & 1.4 GB
+            & TO ($>6$d)
             \\
         M4b: Fig.~\ref{fig:four-bottom}
             & \texttt{MC\_ffg\_b3\_ffg5\_v12}
@@ -149,13 +149,14 @@ \subsection{Model checking experiments}
         M5b: Fig.~\ref{fig:five2}
             & \texttt{MC\_ffg\_b3\_ffg5\_v12}
             & \texttt{Init\_C1}
-            & XXX
-            & XXX
+            & 1.5 GB
+            & TO ($>6$d)
             \\
             \bottomrule
     \end{tabular}
     \caption{Checking accountable safety
-             against~\SpecFourB{}}\label{tab:spec4b-experiments}
+             against~\SpecFourB{} (``TO'' means timeout)}%
+             \label{tab:spec4b-experiments}
 \end{table}
 
 \begin{table}

From 91acb8d367388a9a240252d31833b357103dc7b8 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 1 Nov 2024 15:05:34 +0100
Subject: [PATCH 14/15] update the experiments

---
 EXPERIMENTS.md | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/EXPERIMENTS.md b/EXPERIMENTS.md
index 8d5e38c..bdc1b89 100644
--- a/EXPERIMENTS.md
+++ b/EXPERIMENTS.md
@@ -393,7 +393,7 @@ $ JVM_ARGS=-Xmx20G apalache-mc check \
   MC_ffg_b3_ffg5_v12.tla
 ```
 
-This experiment took 19 hours 48 min 29 sec.
+This experiment did not finish after 6 days.
 
 ## 7. Induction checking with Spec 4b
 
@@ -405,7 +405,7 @@ We ran the experiments using the following scripts:
  - [check-accountable-safety.sh](./spec4b-optimizations/check-accountable-safety.sh)
    to check accountable safety against the inductive invariant.
 
-The table below summarizes the experiments with inductiveness checking.
+The table below summarizes the experiments with inductiveness checking:
 
 | Instance               | Init     | Invariant | Memory | Time       |
 |------------------------|----------|-----------|--------|------------|
@@ -417,6 +417,16 @@ The table below summarizes the experiments with inductiveness checking.
 | MC_ffg_b3_ffg5_v12     | Init_C3  | IndInv    | 1.6 GB | 17min 39s  |
 | MC_ffg_b3_ffg5_v12     | Init_C4  | IndInv    | 1.6 GB | 16min 23s  |
 
+The table below summarizes the experiments with accountable safety:
+
+| Instance               | Init    | Invariant         | Memory | Time       |
+|------------------------|---------|-------------------|--------|------------|
+| MC_ffg-b1_ffg5_v12     | Init_C1 | AccountableSafety | 1.2 GB | 11h 31min  |
+| MC_ffg-b3_ffg5_v12     | Init_C4 | AccountableSafety | 1.4 GB | TO (> 6d)  |
+| MC_ffg-b3_ffg5_v12     | Init_C2 | AccountableSafety | 1.3 GB | 1day 6h    |
+| MC_ffg-b3_ffg5_v12     | Init_C3 | AccountableSafety | 1.2 GB | 1h 53min   |
+| MC_ffg-b3_ffg5_v12     | Init_C1 | AccountableSafety | 1.5 GB | TO (> 6d)  |
+
 [Apalache]: https://apalache-mc.org/
 [Apalache installation]: https://apalache-mc.org/docs/apalache/installation/index.html
 [Apalache releases]: https://github.com/apalache-mc/apalache/releases

From 32117235c99f29986927b05159f214c1741db063 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 1 Nov 2024 20:08:01 +0100
Subject: [PATCH 15/15] Apply suggestions from code review

Co-authored-by: Kukovec <jure.kukovec@gmail.com>
---
 reports/spec4b.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index 27755f8..eb1c0cf 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -95,7 +95,7 @@ \subsection{Decomposition of chain configurations}\label{sec:decomposition}
 \subsection{Model checking experiments}
 
 Tables~\ref{tab:spec4b-experiments} and~\ref{tab:spec4b-inductiveness}
-summarizes our experiments with Apalache for various configurations. One
+summarize our experiments with Apalache for various configurations. One
 interesting effect of the optimizations, especially of the ones presented in
 Section~\ref{sec:decomposition}, is a significant drop in the memory
 consumption of the SMT solver. In our experiments, Z3 required from 700~MB to
@@ -107,9 +107,9 @@ \subsection{Model checking experiments}
 of~\SpecFour{}. We conjecture that this is caused by the need to check more
 specialized graphs in conjunction with steps.
 
-We notice significant variations in the running times on different
-configurations. This is probably due to the effect of different runs of the Z3
-SMT solve having great variation of running times, which is well-known in the
+We observe that the run-times depend on the different
+configurations used. This is probably due to the effect of built-in variance of runs of the Z3
+SMT solver, which is well-known in the
 community of computer-aided verification. To further confirm these variations,
 we could run multiple experiments with~\texttt{hyperfine}.