From 36b5d924eb3d15a6c02c520d0e6fbaacf04b14f7 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt
Date: Mon, 22 Jan 2024 17:36:34 +0100
Subject: [PATCH] Add check to avoid empty set of running consumers
---
tests/mbt/model/ccv_model.qnt | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt
index 9727a56475..12eca0fa8c 100644
--- 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)