add aba_asyn_byz_counters run config

examples/bcastByz/MC10.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC10 -------------------------------------
+
+N == 10
+T == 3
+F == 3
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/MC13.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC13 -------------------------------------
+
+N == 13
+T == 4
+F == 4
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/MC16.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC16 -------------------------------------
+
+N == 16
+T == 5
+F == 5
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/MC19.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC19 -------------------------------------
+
+N == 19
+T == 6
+F == 6
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/MC4.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC4 -------------------------------------
+
+N == 4
+T == 1
+F == 1
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/MC7.tla

@@ -0,0 +1,8 @@
+----------------------------- MODULE MC7 -------------------------------------
+
+N == 7
+T == 2
+F == 2
+
+INSTANCE bcastByz
+===============================================================================

examples/bcastByz/bcastByz.tla

@@ -127,7 +127,7 @@ UnforgLtl == (\A i \in Corr: pc[i] = "V0") => [](\A i \in Corr: pc[i] /= "AC")
 (* The special case of the unforgeability property. When our algorithms start with InitNoBcast,
    we can rewrite UnforgLtl as a first-order formula.     
  *)          
-Unforg == (\A i \in Proc: i \in Corr => (pc[i] /= "AC")) 
+Unforg == (\A i \in Corr: (pc[i] /= "AC"))
 
 IndInv_Unforg_NoBcast ==  
   /\ TypeOK

examples/build.sbt

@@ -35,7 +35,6 @@ lazy val testAba = Seq( // not related to a certain Swedish band
   Spec("aba_asyn_byz_sets", "MC13.tla", length = 11, init = "Init", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_sets", "MC16.tla", length = 13, init = "Init", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_sets", "MC19.tla", length = 15, init = "Init", inv = Some("NoDecide")),
-   */
   Spec("aba_asyn_byz_fns", "MC4.tla", length = 5, init = "Init0", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_fns", "MC7.tla", length = 7, init = "Init0", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_fns", "MC10.tla", length = 9, init = "Init0", inv = Some("NoDecide")),
@@ -48,6 +47,36 @@ lazy val testAba = Seq( // not related to a certain Swedish band
   Spec("aba_asyn_byz_fns", "MC13.tla", length = 11, init = "Init", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_fns", "MC16.tla", length = 13, init = "Init", inv = Some("NoDecide")),
   Spec("aba_asyn_byz_fns", "MC19.tla", length = 15, init = "Init", inv = Some("NoDecide")),
+   */
+  Spec("aba_asyn_byz_counters", "MC4.tla", length = 5, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC7.tla", length = 7, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC10.tla", length = 9, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC13.tla", length = 11, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC16.tla", length = 13, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC19.tla", length = 15, init = "Init0", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC4.tla", length = 5, init = "Init", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC7.tla", length = 7, init = "Init", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC10.tla", length = 9, init = "Init", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC13.tla", length = 11, init = "Init", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC16.tla", length = 13, init = "Init", inv = Some("NoDecide")),
+  Spec("aba_asyn_byz_counters", "MC19.tla", length = 15, init = "Init", inv = Some("NoDecide")),
+)
+
+lazy val testOther = Seq(
+  // length is 2T+3, with N > 3T; N is the number on the MC files
+  // inv holds for Init0 and does not hold for Init
+  Spec("bcastByz", "MC4.tla", length = 5, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC7.tla", length = 7, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC10.tla", length = 9, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC13.tla", length = 11, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC16.tla", length = 13, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC19.tla", length = 15, init = "InitNoBcast", inv = Some("Unforg")),
+  Spec("bcastByz", "MC4.tla", length = 5, init = "Init", inv = Some("Unforg")),
+  Spec("bcastByz", "MC7.tla", length = 7, init = "Init", inv = Some("Unforg")),
+  Spec("bcastByz", "MC10.tla", length = 9, init = "Init", inv = Some("Unforg")),
+  Spec("bcastByz", "MC13.tla", length = 11, init = "Init", inv = Some("Unforg")),
+  Spec("bcastByz", "MC16.tla", length = 13, init = "Init", inv = Some("Unforg")),
+  Spec("bcastByz", "MC19.tla", length = 15, init = "Init", inv = Some("Unforg")),
 )
 
 lazy val testTendermint = Seq(