From e37ab2634b7184c0e1cb3930d92bcd661a9af440 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Sat, 8 Oct 2022 15:58:16 +0200 Subject: [PATCH] add aba_asyn_byz_counters run config --- examples/bcastByz/MC10.tla | 8 ++++++++ examples/bcastByz/MC13.tla | 8 ++++++++ examples/bcastByz/MC16.tla | 8 ++++++++ examples/bcastByz/MC19.tla | 8 ++++++++ examples/bcastByz/MC4.tla | 8 ++++++++ examples/bcastByz/MC7.tla | 8 ++++++++ examples/bcastByz/bcastByz.tla | 2 +- examples/build.sbt | 31 ++++++++++++++++++++++++++++++- 8 files changed, 79 insertions(+), 2 deletions(-) create mode 100644 examples/bcastByz/MC10.tla create mode 100644 examples/bcastByz/MC13.tla create mode 100644 examples/bcastByz/MC16.tla create mode 100644 examples/bcastByz/MC19.tla create mode 100644 examples/bcastByz/MC4.tla create mode 100644 examples/bcastByz/MC7.tla diff --git a/examples/bcastByz/MC10.tla b/examples/bcastByz/MC10.tla new file mode 100644 index 0000000..87472f8 --- /dev/null +++ b/examples/bcastByz/MC10.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC10 ------------------------------------- + +N == 10 +T == 3 +F == 3 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/MC13.tla b/examples/bcastByz/MC13.tla new file mode 100644 index 0000000..c625e11 --- /dev/null +++ b/examples/bcastByz/MC13.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC13 ------------------------------------- + +N == 13 +T == 4 +F == 4 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/MC16.tla b/examples/bcastByz/MC16.tla new file mode 100644 index 0000000..453f4fa --- /dev/null +++ b/examples/bcastByz/MC16.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC16 ------------------------------------- + +N == 16 +T == 5 +F == 5 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/MC19.tla b/examples/bcastByz/MC19.tla new file mode 100644 index 0000000..53db914 --- /dev/null +++ b/examples/bcastByz/MC19.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC19 ------------------------------------- + +N == 19 +T == 6 +F == 6 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/MC4.tla b/examples/bcastByz/MC4.tla new file mode 100644 index 0000000..df14e53 --- /dev/null +++ b/examples/bcastByz/MC4.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC4 ------------------------------------- + +N == 4 +T == 1 +F == 1 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/MC7.tla b/examples/bcastByz/MC7.tla new file mode 100644 index 0000000..d29ca4c --- /dev/null +++ b/examples/bcastByz/MC7.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MC7 ------------------------------------- + +N == 7 +T == 2 +F == 2 + +INSTANCE bcastByz +=============================================================================== \ No newline at end of file diff --git a/examples/bcastByz/bcastByz.tla b/examples/bcastByz/bcastByz.tla index 828fc94..0b4600e 100644 --- a/examples/bcastByz/bcastByz.tla +++ b/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 diff --git a/examples/build.sbt b/examples/build.sbt index 014256b..e6313c9 100644 --- a/examples/build.sbt +++ b/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(