Add check to avoid empty set of running consumers

cosmos · Jan 22, 2024 · 36b5d92 · 36b5d92
1 parent 36a7041
commit 36b5d92
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt
@@ -663,7 +663,8 @@ module ccv_model {
         }
 
     action nondetKeyAssignment = 
-        any {
+        all {
+            runningConsumers.size() > 0,
             nondet node = oneOf(nodes)
             nondet consumerAddr = oneOf(consumerAddresses)
             nondet consumer = oneOf(runningConsumers)