Add property MonotonicByzCommittedIndexdProp

Signed-off-by: Markus Alexander Kuppe <[email protected]>
heidihoward · Dec 7, 2024 · d2e727d · d2e727d
1 parent 483eabe
commit d2e727d
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 0 deletions.
diff --git a/MCpirateship.cfg b/MCpirateship.cfg
@@ -29,6 +29,7 @@ INVARIANT
 PROPERTIES 
     CommittedLogAppendOnlyProp
     ByzCommittedLogAppendOnlyProp
+    MonotonicByzCommittedIndexdProp
 
 CHECK_DEADLOCK 
     FALSE

diff --git a/MCpirateshipCrash.cfg b/MCpirateshipCrash.cfg
@@ -35,6 +35,7 @@ INVARIANT
 PROPERTIES 
     CommittedLogAppendOnlyProp
     ByzCommittedLogAppendOnlyProp
+    MonotonicByzCommittedIndexdProp
 
 CHECK_DEADLOCK 
     FALSE

diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg
@@ -28,6 +28,7 @@ INVARIANT
 PROPERTIES 
     CommittedLogAppendOnlyProp
     ByzCommittedLogAppendOnlyProp
+    MonotonicByzCommittedIndexdProp
 
 CONSTRAINTS
     CrashCommitIndexAt1

diff --git a/SIMpirateshipCrash.cfg b/SIMpirateshipCrash.cfg
@@ -28,6 +28,7 @@ INVARIANT
 PROPERTIES 
     CommittedLogAppendOnlyProp
     ByzCommittedLogAppendOnlyProp
+    MonotonicByzCommittedIndexdProp
 
 CONSTRAINTS
     CrashCommitIndexAt1

diff --git a/pirateship.tla b/pirateship.tla
@@ -598,6 +598,10 @@ CommittedLogAppendOnlyProp ==
         \A i \in R :
         IsPrefixWithoutEmpty(Committed(i), Committed(i)')]_vars
 
+MonotonicByzCommittedIndexdProp ==
+    [][\A i \in CR :
+        byzCommitIndex[i] <= byzCommitIndex'[i]]_vars
+
 \* Each correct replica only appends to its byzantine committed log
 ByzCommittedLogAppendOnlyProp ==
     [][\A i \in CR :