From d760b2e61aa50adcdfd1fa2c48147345a399a4fa Mon Sep 17 00:00:00 2001
From: Chris Novakovic <c.novakovic@cs.bham.ac.uk>
Date: Fri, 23 Feb 2018 16:35:02 +0000
Subject: [PATCH] explicit: don't re-explore states when not using labels

In attachLabels(), avoid unnecessarily exploring the state space again
when the ModelGenerator indicates that labels aren't used (i.e. when
getNumLabels() == 0).
---
 prism/src/explicit/ConstructModel.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java
index 9e0086fa..f3cc8934 100644
--- a/prism/src/explicit/ConstructModel.java
+++ b/prism/src/explicit/ConstructModel.java
@@ -374,6 +374,8 @@ public class ConstructModel extends PrismComponent
 		int numStates = statesList.size();
 		// Create storage for labels
 		int numLabels = modelGen.getNumLabels();
+		// No need to continue unless this ModelGenerator uses labels
+		if (numLabels == 0) return;
 		BitSet bitsets[] = new BitSet[numLabels];
 		for (int j = 0; j < numLabels; j++) {
 			bitsets[j] = new BitSet();