From 01aaf56ca38675b4a07e237d9a0d27662d9c51fc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jul 2015 11:25:49 +0000 Subject: [PATCH] explicit.DTMCModelChecker: Implements predecessor-based versions of prob0 / prob1. [from Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10196 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 142 +++++++++++++++++++++-- 1 file changed, 133 insertions(+), 9 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 729cc80a..80324a14 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -411,6 +411,7 @@ public class DTMCModelChecker extends ProbModelChecker BitSet no, yes; int i, n, numYes, numNo; long timer, timerProb0, timerProb1; + PredecessorRelation pre = null; // Local copy of setting LinEqMethod linEqMethod = this.linEqMethod; @@ -451,17 +452,29 @@ public class DTMCModelChecker extends ProbModelChecker exportLabels(dtmc, labels, labelNames, Prism.EXPORT_PLAIN, new PrismFileLog(getExportTargetFilename())); } + if (precomp && (prob0 || prob1) && cachePre) { + pre = dtmc.getPredecessorRelation(this, true); + } + // Precomputation timerProb0 = System.currentTimeMillis(); if (precomp && prob0) { - no = prob0(dtmc, remain, target); + if (cachePre) { + no = prob0(dtmc, remain, target, pre); + } else { + no = prob0(dtmc, remain, target); + } } else { no = new BitSet(); } timerProb0 = System.currentTimeMillis() - timerProb0; timerProb1 = System.currentTimeMillis(); if (precomp && prob1) { - yes = prob1(dtmc, remain, target); + if (cachePre) { + yes = prob1(dtmc, remain, target, pre); + } else { + yes = prob1(dtmc, remain, target); + } } else { yes = (BitSet) target.clone(); } @@ -496,12 +509,56 @@ public class DTMCModelChecker extends ProbModelChecker return res; } + /** - * Prob0 precomputation algorithm. + * Prob0 precomputation algorithm (using predecessor relation), * i.e. determine the states of a DTMC which, with probability 0, - * reach a state in {@code target}, while remaining in those in @{code remain}. - * @param mdp The MDP - * @param remain Remain in these states (optional: null means "all") + * reach a state in {@code target}, while remaining in those in {@code remain}. + * @param dtmc The DTMC + * @param remain Remain in these states (optional: {@code null} means "all states") + * @param target Target states + * @param pre The predecessor relation + */ + public BitSet prob0(DTMC dtmc, BitSet remain, BitSet target, PredecessorRelation pre) + { + BitSet canReachTarget, result; + long timer; + + // Start precomputation + timer = System.currentTimeMillis(); + mainLog.println("Starting Prob0..."); + + // Special case: no target states + if (target.isEmpty()) { + BitSet soln = new BitSet(dtmc.getNumStates()); + soln.set(0, dtmc.getNumStates()); + return soln; + } + + // calculate all states that can reach 'target' + // while remaining in 'remain' in the underlying graph, + // where all the 'target' states are made absorbing + canReachTarget = pre.calculatePreStar(remain, target, target); + + // prob0 = complement of 'canReachTarget' + result = new BitSet(); + result.set(0, dtmc.getNumStates(), true); + result.andNot(canReachTarget); + + // Finished precomputation + timer = System.currentTimeMillis() - timer; + mainLog.print("Prob0"); + mainLog.println(" took " + timer / 1000.0 + " seconds."); + + return result; + } + + /** + * Prob0 precomputation algorithm (using a fixed-point computation), + * i.e. determine the states of a DTMC which, with probability 0, + * reach a state in {@code target}, while remaining in those in {@code remain}. + * @param dtmc The DTMC + * @param remain Remain in these states (optional: {@code null} means "all") * @param target Target states */ public BitSet prob0(DTMC dtmc, BitSet remain, BitSet target) @@ -564,12 +621,79 @@ public class DTMCModelChecker extends ProbModelChecker } /** - * Prob1 precomputation algorithm. + * Prob1 precomputation algorithm (using predecessor relation), * i.e. determine the states of a DTMC which, with probability 1, - * reach a state in {@code target}, while remaining in those in @{code remain}. - * @param mdp The MDP + * reach a state in {@code target}, while remaining in those in {@code remain}. + * @param dtmc The DTMC * @param remain Remain in these states (optional: null means "all") * @param target Target states + * @param pre The predecessor relation of the DTMC + */ + public BitSet prob1(DTMC dtmc, BitSet remain, BitSet target, PredecessorRelation pre) { + // Implements the constrained reachability algorithm from + // Baier, Katoen: Principles of Model Checking (Corollary 10.31 Qualitative Constrained Reachability) + long timer; + + // Start precomputation + timer = System.currentTimeMillis(); + mainLog.println("Starting Prob1..."); + + // Special case: no 'target' states + if (target.isEmpty()) { + // empty set + return new BitSet(); + } + + // mark all states in 'target' and all states not in 'remain' as absorbing + BitSet absorbing = new BitSet(); + if (remain != null) { + // complement remain + absorbing.set(0, dtmc.getNumStates(), true); + absorbing.andNot(remain); + } else { + // for remain == null, remain consists of all states + // thus, absorbing = the empty set is already the complementation of remain + } + // union with 'target' + absorbing.or(target); + + // M' = DTMC where all 'absorbing' states are considered to be absorbing + + // the set of states that satisfy E [ F target ] in M' + // Pre*(target) + BitSet canReachTarget = pre.calculatePreStar(null, target, absorbing); + + // complement canReachTarget + // S\Pre*(target) + BitSet canNotReachTarget = new BitSet(); + canNotReachTarget.set(0, dtmc.getNumStates(), true); + canNotReachTarget.andNot(canReachTarget); + + // the set of states that can reach a canNotReachTarget state in M' + // Pre*(S\Pre*(target)) + BitSet probTargetNot1 = pre.calculatePreStar(null, canNotReachTarget, absorbing); + + // complement probTargetNot1 + // S\Pre*(S\Pre*(target)) + BitSet result = new BitSet(); + result.set(0, dtmc.getNumStates(), true); + result.andNot(probTargetNot1); + + // Finished precomputation + timer = System.currentTimeMillis() - timer; + mainLog.print("Prob1"); + mainLog.println(" took " + timer / 1000.0 + " seconds."); + + return result; + } + + /** + * Prob1 precomputation algorithm (using a fixed-point computation) + * i.e. determine the states of a DTMC which, with probability 1, + * reach a state in {@code target}, while remaining in those in {@code remain}. + * @param dtmc The DTMC + * @param remain Remain in these states (optional: {@code null} means "all") + * @param target Target states */ public BitSet prob1(DTMC dtmc, BitSet remain, BitSet target) {