From b81b80e87772d421706f42d2b4b04ad9a38f5e01 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 15 Dec 2010 19:50:35 +0000
Subject: [PATCH] Deadlocks reported as timelocks for PTAs model checked with
 digital clocks.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2332 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/PrismCL.java                      | 15 +++++++++++----
 .../userinterface/properties/GUIExperiment.java   |  7 ++-----
 .../properties/computation/ModelCheckThread.java  |  7 ++-----
 3 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 6c60eb26..41cd8861 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -244,7 +244,7 @@ public class PrismCL
 			if (doBuild) {
 				// build model
 				try {
-					buildModel(modulesFile);
+					buildModel(modulesFile, false);
 				} catch (PrismException e) {
 					// in case of error, report it, store as result for any properties, and go on to the next model
 					error(e.getMessage());
@@ -361,7 +361,7 @@ public class PrismCL
 								modulesFileToCheck = dc.getNewModulesFile();
 								modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues());
 								doPrismLangExports(modulesFileToCheck);
-								buildModel(modulesFileToCheck);
+								buildModel(modulesFileToCheck, true);
 							} else {
 								modulesFileToCheck = modulesFile;
 							}
@@ -613,8 +613,10 @@ public class PrismCL
 	 * Build a model, usually from the passed in modulesFileToBuild. However, if importtrans=true,
 	 * then explicit model import is done and modulesFileToBuild can be null.
 	 * This method also displays model info and checks/fixes deadlocks.
+	 * If flag 'digital' is true, then this (MDP) model was constructed
+	 * from digital clocks semantics of a PTA - might need for error reporting.
 	 */
-	private void buildModel(ModulesFile modulesFileToBuild) throws PrismException
+	private void buildModel(ModulesFile modulesFileToBuild, boolean digital) throws PrismException
 	{
 		StateList states;
 		int i;
@@ -645,8 +647,13 @@ public class PrismCL
 		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
-				if (fixdl) {
+				else if (fixdl) {
 					mainLog.print("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
 					model.fixDeadlocks();
 				}
diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java
index 3d85e331..e3ab7711 100644
--- a/prism/src/userinterface/properties/GUIExperiment.java
+++ b/prism/src/userinterface/properties/GUIExperiment.java
@@ -409,13 +409,10 @@ public class GUIExperiment
 									logln("\n-------------------------------------------");
 									model = prism.buildModel(modulesFileToCheck);
 									clear = false;
-									// remove any deadlocks (don't prompt - probably should)
+									// by construction, deadlocks can only occur from timelocks
 									StateList states = model.getDeadlockStates();
 									if (states != null) {
-										if (states.size() > 0) {
-											guiProp.log("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
-											model.fixDeadlocks();
-										}
+										throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
 									}
 									// print some model info
 									guiProp.log("\n");
diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java
index 72bbbbf4..e3259bcb 100644
--- a/prism/src/userinterface/properties/computation/ModelCheckThread.java
+++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java
@@ -145,13 +145,10 @@ public class ModelCheckThread extends GUIComputationThread
 					logln("\n-------------------------------------------");
 					model = prism.buildModel(modulesFileToCheck);
 					clear = false;
-					// remove any deadlocks (don't prompt - probably should)
+					// by construction, deadlocks can only occur from timelocks
 					StateList states = model.getDeadlockStates();
 					if (states != null) {
-						if (states.size() > 0) {
-							log("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
-							model.fixDeadlocks();
-						}
+						throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")");
 					}
 					// print some model info
 					log("\n");