From 2b816d8f6d462f27ae36a7a17a1f831809f80b23 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 20 Mar 2012 21:05:01 +0000
Subject: [PATCH] Add some currently commented-out code for digital clocks
 debugging.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4915 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index ec71a6ef..078fd2f5 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -1772,6 +1772,24 @@ public class Prism implements PrismSettingsListener
 				throw new PrismException("Timelock in PTA, e.g. in state " + dls);
 			}
 		}
+				
+		/*// Create new model checker object and do model checking
+		PropertiesFile pf = parsePropertiesString(currentModulesFile, "filter(exists,!\"invariants\"); E[F!\"invariants\"]");
+		if (!getExplicit()) {
+			ModelChecker mc = new NondetModelChecker(this, currentModel, pf);
+			if (((Boolean) mc.check(pf.getProperty(0)).getResult()).booleanValue()) {
+				mainLog.println(mc.check(pf.getProperty(1)).getCounterexample());
+			}
+			//sv.pr
+			//mainLog.println("XX" + res.getResult());
+		} else {
+			explicit.StateModelChecker mc = new MDPModelChecker();
+			mc.setLog(mainLog);
+			mc.setSettings(settings);
+			mc.setModulesFileAndPropertiesFile(currentModulesFile, pf);
+			explicit.StateValues sv = mc.checkExpression(currentModelExpl, pf.getProperty(0));
+			sv.print(mainLog, 1);
+		}*/
 	}
 	
 	/**