Add ASSUME statements on Writers and Readers.

tlaplus · Sep 16, 2024 · ff64e51 · ff64e51
1 parent faf4046
commit ff64e51
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 0 deletions.
diff --git a/specifications/Disruptor/Disruptor_MPMC.tla b/specifications/Disruptor/Disruptor_MPMC.tla
@@ -20,6 +20,8 @@ CONSTANTS
   Size,             (* Ringbuffer size.                                     *)
   NULL
 
+ASSUME Writers /= {}
+ASSUME Readers /= {}
 ASSUME Size \in Nat \ {0}
 
 VARIABLES

diff --git a/specifications/Disruptor/Disruptor_SPMC.tla b/specifications/Disruptor/Disruptor_SPMC.tla
@@ -22,6 +22,8 @@ CONSTANTS
   Size,         (* Ringbuffer size.                                  *)
   NULL
 
+ASSUME Writers /= {}
+ASSUME Readers /= {}
 ASSUME Size \in Nat \ {0}
 
 VARIABLES

diff --git a/specifications/Disruptor/RingBuffer.tla b/specifications/Disruptor/RingBuffer.tla
@@ -22,6 +22,8 @@ CONSTANTS
   NULL
 
 ASSUME Size \in Nat \ {0}
+ASSUME Writers /= {}
+ASSUME Readers /= {}
 ASSUME NULL \notin Values
 
 VARIABLE ringbuffer