From 1b87d356a80d32e40b77f21470e6f25bd84cbae6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 12 Feb 2012 21:09:11 +0000
Subject: [PATCH] Move explicitBuildTest code into PRISM, but currently
 unfinished/unused.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4602 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java   | 48 +++++++++++++++++++++++++++---------
 prism/src/prism/PrismCL.java | 47 -----------------------------------
 2 files changed, 36 insertions(+), 59 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 392cf340..a72c3210 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -1034,18 +1034,7 @@ public class Prism implements PrismSettingsListener
 	 */
 	public static List<String> getListOfKeyords()
 	{
-		try {
-			// obtain exclusive access to the prism parser
-			// (don't forget to release it afterwards)
-			try {
-				return getPrismParser().getListOfKeywords();
-			} finally {
-				// release prism parser
-				releasePrismParser();
-			}
-		} catch (InterruptedException ie) {
-			return null;
-		}
+		return PrismParser.getListOfKeywords();
 	}
 
 	//------------------------------------------------------------------------------
@@ -2679,6 +2668,41 @@ public class Prism implements PrismSettingsListener
 			tmpLog.close();
 	}
 
+	public void explicitBuildTest() throws PrismException
+	{
+		/* old code...
+		String tmpFile = "";
+		try {
+			explicit.ConstructModel constructModel = new explicit.ConstructModel(getSimulator(), mainLog);
+			mainLog.println("\nConstructing model explicitly...");
+			explicit.Model modelExplicit = constructModel.constructModel(currentModulesFile);
+			tmpFile = File.createTempFile("explicitbuildtest", ".tra").getAbsolutePath();
+			tmpFile = "explicitbuildtest.tra";
+			mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "1\"...");
+			modelExplicit.exportToPrismExplicitTra(tmpFile + "1");
+			mainLog.println("\nExporting (normal) model to \"" + tmpFile + "2\"...");
+			exportTransToFile(true, Prism.EXPORT_PLAIN, new File(tmpFile + "2"));
+			explicit.ModelSimple modelExplicit2 = null;
+			switch (currentModelType) {
+			case DTMC:
+				modelExplicit2 = new explicit.DTMCSimple();
+				break;
+			case CTMC:
+				modelExplicit2 = new explicit.CTMCSimple();
+				break;
+			case MDP:
+				modelExplicit2 = new explicit.MDPSimple();
+				break;
+			}
+			modelExplicit2.buildFromPrismExplicit(tmpFile + "2");
+			if (!modelExplicit.equals(modelExplicit2)) {
+				throw new PrismException("Explicit models differ");
+			}
+		} catch (IOException e) {
+			throw new PrismException("Could not create temporary file \"" + tmpFile + "\"");
+		}*/
+	}
+	
 	/**
 	 * Clear the built model if needed (free/deallocate memory etc)
 	 */
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 03109099..271ba850 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -553,53 +553,6 @@ public class PrismCL implements PrismModelListener
 		}
 	}
 
-	/**
-	 * 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, boolean digital) throws PrismException
-	{
-		// TODO
-		/*
-		StateList states;
-		// If enabled, also construct model explicitly and compare (for testing purposes)
-		if (explicitbuildtest) {
-			String tmpFile = "'";
-			try {
-				explicit.ConstructModel constructModel = new explicit.ConstructModel(prism.getSimulator(), mainLog);
-				mainLog.println("\nConstructing model explicitly...");
-				explicit.Model modelExplicit = constructModel.constructModel(modulesFileToBuild);
-				tmpFile = File.createTempFile("explicitbuildtest", ".tra").getAbsolutePath();
-				tmpFile = "explicitbuildtest.tra";
-				mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "1\"...");
-				modelExplicit.exportToPrismExplicitTra(tmpFile + "1");
-				mainLog.println("\nExporting (normal) model to \"" + tmpFile + "2\"...");
-				prism.exportTransToFile(model, true, Prism.EXPORT_PLAIN, new File(tmpFile + "2"));
-				explicit.ModelSimple modelExplicit2 = null;
-				switch (model.getModelType()) {
-				case DTMC:
-					modelExplicit2 = new explicit.DTMCSimple();
-					break;
-				case CTMC:
-					modelExplicit2 = new explicit.CTMCSimple();
-					break;
-				case MDP:
-					modelExplicit2 = new explicit.MDPSimple();
-					break;
-				}
-				modelExplicit2.buildFromPrismExplicit(tmpFile + "2");
-				if (!modelExplicit.equals(modelExplicit2)) {
-					throw new PrismException("Explicit models differ");
-				}
-			} catch (IOException e) {
-				throw new PrismException("Could not create temporary file \"" + tmpFile + "\"");
-			}
-		}*/
-	}
-
 	// do any exporting requested
 
 	private void doExports()