From a4b2b0416281a15f023ff5c23197a9f1b27e974e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Dec 2008 13:09:28 +0000 Subject: [PATCH] Tweaked symmetry reduction info output. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@856 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Modules2MTBDD.java | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index c157621f..3f1db25d 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -2042,22 +2042,25 @@ public class Modules2MTBDD //ODDNode odd = ODDUtils.BuildODD(reach, allDDRowVars); //try {sparse.PrismSparse.NondetExport(trans, allDDRowVars, allDDColVars, allDDNondetVars, odd, Prism.EXPORT_PLAIN, "trans-full.tra"); } catch (FileNotFoundException e) {} + mainLog.println("\nNumber of states before before symmetry reduction: " + model.getNumStatesString()); + mainLog.println("DD sizes before symmetry reduction:"); + // trans - rows - mainLog.print("trans (full): "); + mainLog.print("trans: "); mainLog.println(JDD.GetInfoString(trans, (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); JDD.Ref(symm); trans = JDD.Apply(JDD.TIMES, trans, symm); - mainLog.print("trans (symm): "); - mainLog.println(JDD.GetInfoString(trans, (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); + //mainLog.print("trans (symm): "); + //mainLog.println(JDD.GetInfoString(trans, (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); // trans rewards - rows for (k = 0; k < numRewardStructs; k++) { - mainLog.print("transrew["+k+"] (full): "); + mainLog.print("transrew["+k+"]: "); mainLog.println(JDD.GetInfoString(transRewards[k], (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); JDD.Ref(symm); transRewards[k] = JDD.Apply(JDD.TIMES, transRewards[k], symm); - mainLog.print("transrew["+k+"] (symm): "); - mainLog.println(JDD.GetInfoString(transRewards[k], (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); + //mainLog.print("transrew["+k+"] (symm): "); + //mainLog.println(JDD.GetInfoString(transRewards[k], (type==ModulesFile.NONDETERMINISTIC)?(allDDRowVars.n()*2+allDDNondetVars.n()):(allDDRowVars.n()*2))); } mainLog.println("Starting quicksort...");