From 146dbe8adef7d87dcccd8eb88130096db6399727 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 1 Jun 2016 12:02:01 +0000 Subject: [PATCH] DebugJDD: main() to run small test cases git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11384 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/DebugJDD.java | 203 ++++++++++++++++++++++++++++++++++++ 1 file changed, 203 insertions(+) diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index 5d5d9250..5eebe395 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/prism/src/jdd/DebugJDD.java @@ -37,6 +37,11 @@ import java.util.Map; import java.util.Map.Entry; import java.util.TreeMap; +import prism.Prism; +import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLog; + /** * Framework for debugging JDDNode and CUDD reference counting. @@ -598,4 +603,202 @@ public class DebugJDD } } + /* --------------------- TESTING -------------------------------------------- + * + * The methods below provide simple test cases that can be executed from + * the command line to study the behaviour of the debugging functionality + * and of the tracing mechanism. + */ + + private static void test_1() + { + // test case: missing dereference + JDDNode const2 = JDD.Constant(2.0); + } + + private static void test_2() + { + // test case: additional dereference + JDDNode const2 = JDD.Constant(2.0); + JDD.Deref(const2); + JDD.Deref(const2); + } + + private static void test_3() + { + // test case: use of a JDDNode with 0 references + JDDNode const2 = JDD.Constant(2.0); + JDD.Deref(const2); + JDDNode t = JDD.ITE(JDD.Constant(1), const2, JDD.Constant(0)); + JDD.Deref(t); + } + + private static void test_4() + { + // test case: use of a JDDNode with 0 references, but which has other + // Java references + JDDNode const2 = JDD.Constant(2.0); + JDDNode copy = const2.copy(); + JDD.Deref(const2); + JDDNode t = JDD.ITE(JDD.Constant(1), const2, JDD.Constant(0)); + JDD.Deref(t); + } + + private static void test_5() + { + // test case: more complex example with no problems + // can be used with -ddtraceall to look at tracing + JDDNode v = JDD.Var(0); + JDDVars vars = new JDDVars(); + vars.addVar(v); + + JDDNode t = JDD.ITE(v.copy(), JDD.Constant(2.0), JDD.Constant(1.0)); + JDDNode c = JDD.Constant(2.0); + + t = JDD.Times(t, c); + t = JDD.SumAbstract(t, vars); + + JDD.Deref(t); + vars.derefAll(); + } + + private static void usage() + { + System.out.println("\nUsage: PRISM_MAINCLASS=jdd.DebugJDD prism [arguments] [test cases]"); + System.out.println("\nExample: PRISM_MAINCLASS=jdd.DebugJDD prism -dddebug 1 4"); + System.out.println(" Run test cases 1 and 4, with debugging enabled"); + System.out.println("\nArguments:"); + System.out.println(" -dddebug Enabled JDD debugging"); + System.out.println(" -ddtraceall Trace all JDD nodes"); + System.out.println(" -ddtracefollowcopies Trace copies of traced JDD nodes as well"); + System.out.println(" -dddebugwarnfatal Treat warnings as errors"); + System.out.println(" -dddebugwarnoff Turn off warnings"); + System.out.println(" -ddtrace n Trace JDDNode with ID=n"); + System.out.println("\nFor the test cases, look at the source code in jdd/DebugJDD.java"); + } + + private static void errorAndExit(String error) + { + System.out.println(error); + usage(); + System.exit(1); + } + + /** Command-line entry point */ + public static void main(String[] args) + { + System.out.println("PRISM [jdd.DebugJDD test bed / demonstrator]"); + System.out.println("============================================\n"); + + ArrayList testCases = new ArrayList(); + + // Parse the arguments + for (int i = 0; i < args.length; i++) { + + // if is a switch... + if (args[i].length() > 0 && args[i].charAt(0) == '-') { + + // Remove "-" + String sw = args[i].substring(1); + if (sw.length() == 0) { + errorAndExit("Invalid empty switch"); + } + // Remove optional second "-" (i.e. we allow switches of the form --sw too) + if (sw.charAt(0) == '-') + sw = sw.substring(1); + + // DD Debugging options + if (sw.equals("dddebug")) { + jdd.DebugJDD.enable(); + } + else if (sw.equals("ddtraceall")) { + jdd.DebugJDD.traceAll = true; + } + else if (sw.equals("ddtracefollowcopies")) { + jdd.DebugJDD.traceFollowCopies = true; + } + else if (sw.equals("dddebugwarnfatal")) { + jdd.DebugJDD.warningsAreFatal = true; + } + else if (sw.equals("dddebugwarnoff")) { + jdd.DebugJDD.warningsOff = true; + } + else if (sw.equals("ddtrace")) { + if (i < args.length - 1) { + String idString = args[++i]; + try { + int id = Integer.parseInt(idString); + jdd.DebugJDD.enableTracingForID(id); + } catch (NumberFormatException e) { + errorAndExit("The -" + sw + " switch requires an integer argument (JDDNode ID)"); + } + } else { + errorAndExit("The -" + sw + " switch requires an additional argument (JDDNode ID)"); + } + } + else { + errorAndExit("Unknown switch: -" + sw); + } + } else { + // not a switch, assume is a test case + testCases.add(args[i]); + } + } + + try { + // initialise Prism/CUDD + PrismLog mainLog = new PrismFileLog("stdout"); + + mainLog.println("\n[Initializing PRISM]\n"); + + // create prism object(s) + Prism prism = new Prism(mainLog); + + prism.initialise(); + + int i = 1; + for (String testCase : testCases) { + mainLog.print("\n[Running test case " + testCase); + if (testCases.size() > 1) { + mainLog.print(" (" + i + "/" + testCases.size() + ")"); + } + mainLog.println("]\n"); + i++; + + switch (testCase) { + case "1": + test_1(); + break; + case "2": + test_2(); + break; + case "3": + test_3(); + break; + case "4": + test_4(); + break; + case "5": + test_5(); + break; + + default: + errorAndExit("Unknown test case: " + testCase); + } + } + + mainLog.println("\n[Closing down PRISM/CUDD]\n"); + + // clear up and close down + prism.closeDown(true); + + mainLog.println(); + // Close logs (in case they are files) + mainLog.close(); + } catch (PrismException e) { + e.printStackTrace(); + System.exit(1); + } + } + }