From 6ca3e63d851068118f96cb1003ec2b07bd5842f2 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 7 Jun 2016 10:29:36 +0000
Subject: [PATCH] DebugJDD: add test cases for getThen(), getElse() and
 getValue() calls

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

diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java
index 31bd0d2f..cc7d6e92 100644
--- a/prism/src/jdd/DebugJDD.java
+++ b/prism/src/jdd/DebugJDD.java
@@ -804,6 +804,69 @@ public class DebugJDD
 		vars.derefAll();
 	}
 
+	@SuppressWarnings("unused")
+	private static void test_6()
+	{
+		// test case: getThen of a constant
+		JDDNode const2 = JDD.Constant(2);
+		JDDNode t = const2.getThen();
+	}
+
+	@SuppressWarnings("unused")
+	private static void test_7()
+	{
+		// test case: getElse of a constant
+		JDDNode const2 = JDD.Constant(2);
+		JDDNode t = const2.getElse();
+	}
+
+	@SuppressWarnings("unused")
+	private static void test_8()
+	{
+		// test case: getValue of an internal node
+		JDDNode v = JDD.Var(0);
+		double value = v.getValue();
+	}
+
+	private static void test_9()
+	{
+		// test case: use of a light-weight node as a
+		// method argument
+		JDDNode v = JDD.Var(0);
+		JDDNode result = JDD.Apply(JDD.MAX, v.getThen(), v.getElse());
+		JDD.Deref(result);
+	}
+
+	private static void test_10()
+	{
+		// test case: deref of a light-weight node as a
+		// method argument
+		JDDNode v = JDD.Var(0);
+		JDD.Deref(v.getThen());
+		JDD.Deref(v);
+	}
+
+	private static void test_11()
+	{
+		// test case: ref of a light-weight node as a
+		// method argument
+		JDDNode v = JDD.Var(0);
+		JDDNode t = v.getThen();
+		JDD.Ref(t);
+		JDD.Deref(t);
+		JDD.Deref(v);
+	}
+
+	private static void test_12()
+	{
+		// test case: proper use of a light-weight node as a
+		// method argument by using copy()
+		JDDNode v = JDD.Var(0);
+		JDDNode result = JDD.Apply(JDD.MAX, v.getThen().copy(), v.getElse().copy());
+		JDD.Deref(result);
+		JDD.Deref(v);
+	}
+
 	private static void usage()
 	{
 		System.out.println("\nUsage: PRISM_MAINCLASS=jdd.DebugJDD prism [arguments] [test cases]");
@@ -917,6 +980,27 @@ public class DebugJDD
 				case "5":
 					test_5();
 					break;
+				case "6":
+					test_6();
+					break;
+				case "7":
+					test_7();
+					break;
+				case "8":
+					test_8();
+					break;
+				case "9":
+					test_9();
+					break;
+				case "10":
+					test_10();
+					break;
+				case "11":
+					test_11();
+					break;
+				case "12":
+					test_12();
+					break;
 
 				default:
 					errorAndExit("Unknown test case: " + testCase);