From 5ba9926e7dc3f0f938661b61c56209d961094205 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 7 Mar 2006 20:42:11 +0000 Subject: [PATCH] Added output of MTBDD stats for diagonals/embedded MC to StochModelChecker. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@14 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StochModelChecker.java | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index c9320086..b30af650 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -1026,6 +1026,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // compute probabilities of reaching each bscc... for (i = 0; i < n; i++) { @@ -1140,6 +1143,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // compute probabilities probs = computeNextProbs(emb, b); @@ -1227,6 +1233,8 @@ public class StochModelChecker implements ModelChecker JDD.Ref(trans); JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); // compute probs probs = computeUntilProbs(emb, trans01, b1, b1); JDD.Deref(diags); @@ -1240,6 +1248,8 @@ public class StochModelChecker implements ModelChecker JDD.Ref(trans); JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); // compute unbounded until probs tmpProbs = computeUntilProbs(emb, trans01, b1, b2); JDD.Deref(diags); @@ -1314,6 +1324,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // compute probabilities try { probs = computeUntilProbs(emb, trans01, b1, b2); @@ -1437,6 +1450,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // convert rewards JDD.Ref(stateRewards); JDD.Ref(diags); @@ -1577,6 +1593,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // compute probabilities of reaching each bscc... for (i = 0; i < n; i++) { @@ -1764,6 +1783,9 @@ public class StochModelChecker implements ModelChecker JDD.Ref(diags); emb = JDD.Apply(JDD.DIVIDE, trans, diags); + mainLog.print("\nDiagonals vector: ");JDD.PrintInfo(diags, allDDRowVars.n()); + mainLog.print("Embedded Markov chain: ");JDD.PrintInfo(emb, allDDRowVars.n()*2); + // compute prob of reaching each bscc from initial state probBSCCs = new double[n]; for (i = 0; i < n; i++) {