From 1fba1a5e414caf02d91a0d0ef435bbdf8be80ff0 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 7 Jan 2010 10:39:51 +0000
Subject: [PATCH] Test program for (explicit) STPG model checking.

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

diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java
index 25059557..fb8e4cb8 100644
--- a/prism/src/explicit/STPGModelChecker.java
+++ b/prism/src/explicit/STPGModelChecker.java
@@ -662,4 +662,50 @@ public class STPGModelChecker extends ModelChecker
 			ubSoln2 = soln2;
 		}
 	}*/
+
+
+	/**
+	 * Simple test program.
+	 */
+	public static void main(String args[])
+	{
+		STPGModelChecker mc;
+		STPG stpg;
+		ModelCheckerResult res;
+		BitSet target;
+		Map<String, BitSet> labels;
+		boolean min1 = true, min2 = true;
+		try {
+			mc = new STPGModelChecker();
+			stpg = new STPG();
+			stpg.buildFromPrismExplicit(args[0]);
+			//System.out.println(stpg);
+			labels = mc.loadLabelsFile(args[1]);
+			//System.out.println(labels);
+			target = labels.get(args[2]);
+			if (target == null)
+				throw new PrismException("Unknown label \"" + args[2] + "\"");
+			for (int i  =3; i < args.length; i++) {
+				if (args[i].equals("-minmin")) {
+					min1 =true;
+					min2 = true;
+				} else if (args[i].equals("-maxmin")) {
+					min1 =false;
+					min2 = true;
+				} else if (args[i].equals("-minmax")) {
+					min1 =true;
+					min2 = false;
+				} else if (args[i].equals("-maxmax")) {
+					min1 =false;
+					min2 = false;
+				}
+			}
+			//stpg.exportToDotFile("stpg.dot", target);
+			//stpg.exportToPrismExplicit("stpg");
+			res = mc.probReach(stpg, target, min1, min2);
+			System.out.println(res.soln[0]);
+		} catch (PrismException e) {
+			System.out.println(e);
+		}
+	}
 }