diff --git a/specifications/Disruptor/Disruptor_MPMC.tla b/specifications/Disruptor/Disruptor_MPMC.tla
index e72fc522..34432378 100644
--- 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
index 273116a3..cf252f3d 100644
--- 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
index 76efa574..e59788bd 100644
--- 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