From 95f46fcf1aef999877d1855337eaef7ddd1883b8 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 14 Jan 2011 08:14:11 +0000
Subject: [PATCH] Bugfix: digital clocks from GUI throws errors when it should
 not.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2383 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/PrismCL.java                  | 54 +++++++++----------
 .../properties/GUIExperiment.java             |  2 +-
 .../computation/ModelCheckThread.java         |  2 +-
 3 files changed, 28 insertions(+), 30 deletions(-)

diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index ec84f6d5..dddcf706 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -645,34 +645,32 @@ public class PrismCL
 
 		// check for deadlocks
 		states = model.getDeadlockStates();
-		if (states != null) {
-			if (states.size() > 0) {
-				// for pta models (via digital clocks)
-				if (digital) {
-					// by construction, these can only occur from timelocks
-					throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
-				}
-				// if requested, remove them
-				else if (fixdl) {
-					mainLog.print("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
-					model.fixDeadlocks();
-				}
-				// otherwise print error and bail out
-				else {
-					mainLog.println();
-					model.printTransInfo(mainLog, prism.getExtraDDInfo());
-					mainLog.print("\nError: Model contains " + states.size() + " deadlock states");
-					if (!verbose && states.size() > 10) {
-						mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n");
-						states.print(mainLog, 10);
-					} else {
-						mainLog.print(":\n");
-						states.print(mainLog);
-					}
-					mainLog.print("\nTip: Use the -fixdl switch to automatically add self-loops in deadlock states.\n");
-					model.clear();
-					exit();
-				}
+		if (states != null && states.size() > 0) {
+			// for pta models (via digital clocks)
+			if (digital) {
+				// by construction, these can only occur from timelocks
+				throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
+			}
+			// if requested, remove them
+			else if (fixdl) {
+				mainLog.print("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
+				model.fixDeadlocks();
+			}
+			// otherwise print error and bail out
+			else {
+				mainLog.println();
+				model.printTransInfo(mainLog, prism.getExtraDDInfo());
+				mainLog.print("\nError: Model contains " + states.size() + " deadlock states");
+				if (!verbose && states.size() > 10) {
+					mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n");
+					states.print(mainLog, 10);
+				} else {
+					mainLog.print(":\n");
+					states.print(mainLog);
+				}
+				mainLog.print("\nTip: Use the -fixdl switch to automatically add self-loops in deadlock states.\n");
+				model.clear();
+				exit();
 			}
 		}
 
diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java
index e3ab7711..b90733d8 100644
--- a/prism/src/userinterface/properties/GUIExperiment.java
+++ b/prism/src/userinterface/properties/GUIExperiment.java
@@ -411,7 +411,7 @@ public class GUIExperiment
 									clear = false;
 									// by construction, deadlocks can only occur from timelocks
 									StateList states = model.getDeadlockStates();
-									if (states != null) {
+									if (states != null && states.size() > 0) {
 										throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
 									}
 									// print some model info
diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java
index e3259bcb..8af8e58d 100644
--- a/prism/src/userinterface/properties/computation/ModelCheckThread.java
+++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java
@@ -147,7 +147,7 @@ public class ModelCheckThread extends GUIComputationThread
 					clear = false;
 					// by construction, deadlocks can only occur from timelocks
 					StateList states = model.getDeadlockStates();
-					if (states != null) {
+					if (states != null && states.size() > 0) {
 						throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
 					}
 					// print some model info