From 7e6f8e8cf65522a7ccf28c7ef9ac66b69c80e28c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 28 Jan 2015 14:56:28 +0000 Subject: [PATCH] Revert recent DFA optimizations to allow for acceptance type refactoring. Functionality will be later readded using AcceptanceReach. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9575 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 16 +++------ prism/src/explicit/LTLModelChecker.java | 27 --------------- prism/src/explicit/MDPModelChecker.java | 16 +++------ prism/src/prism/DRA.java | 43 ------------------------ prism/src/prism/LTLModelChecker.java | 21 ------------ prism/src/prism/NondetModelChecker.java | 14 ++------ prism/src/prism/ProbModelChecker.java | 14 ++------ 7 files changed, 14 insertions(+), 137 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 8c08ec10..ed04b719 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -105,21 +105,13 @@ public class DTMCModelChecker extends ProbModelChecker int invMap[] = pair.second; mainLog.print("\n" + modelProduct.infoStringTable()); - // Find accepting states + compute reachability probabilities - BitSet acc = null; - if (dra.isDFA()) { - // For a DFA, just collect the accept states - mainLog.println("\nSkipping BSCC detection since DRA is a DFA..."); - acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, invMap); - } else { - // Usually, we have to detect BSCCs in the product - mainLog.println("\nFinding accepting BSCCs..."); - acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap); - } + // Find accepting BSCCs + compute reachability probabilities + mainLog.println("\nFinding accepting BSCCs..."); + BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(this); mcProduct.inheritSettings(this); - probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acc).soln, modelProduct); + probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct); // Mapping probabilities in the original model double[] probsProductDbl = probsProduct.getDoubleArray(); diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 57a8402d..339f571d 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -314,33 +314,6 @@ public class LTLModelChecker extends PrismComponent return new Pair(prodModel, invMap); } - /** - * Find the set of states in a model corresponding to the "target" part of a Rabin acceptance condition, - * i.e. just the union of the K_i parts of the (L_i,K_i) pairs. - * @param dra The DRA - * @param model The model - * @param invMap The map returned by the constructProduct method(s) - * @return - */ - public BitSet findTargetStatesForRabin(DRA dra, Model model, int invMap[]) - { - // Get union of K_i sets - BitSet unionK = new BitSet(); - int numAcceptancePairs = dra.getNumAcceptancePairs(); - for (int acceptancePair = 0; acceptancePair < numAcceptancePairs; acceptancePair++) { - unionK.or(dra.getAcceptanceK(acceptancePair)); - } - // Collate all model states with a K_i component - int draSize = dra.size(); - int numStates = (int) model.getNumStates(); - BitSet result = new BitSet(); - for (int state = 0; state < numStates; state++) { - int draState = invMap[state] % draSize; - result.set(state, unionK.get(draState)); - } - return result; - } - /** * Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition. * @param dra The DRA diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 78034e4c..1d2a0518 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -112,21 +112,13 @@ public class MDPModelChecker extends ProbModelChecker modelProduct = pair.first; int invMap[] = pair.second; - // Find accepting states + compute reachability probabilities - BitSet acc = null; - if (dra.isDFA()) { - // For a DFA, just collect the accept states - mainLog.println("\nSkipping MEC detection since DRA is a DFA..."); - acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, invMap); - } else { - // Usually, we have to detect MECs in the product - mainLog.println("\nFinding accepting MECs..."); - acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap); - } + // Find accepting MECs + compute reachability probabilities + mainLog.println("\nFinding accepting MECs..."); + BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new MDPModelChecker(this); mcProduct.inheritSettings(this); - probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acc, false).soln, modelProduct); + probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct); // Subtract from 1 if we're model checking a negated formula for regular Pmin if (minMax.isMin()) { diff --git a/prism/src/prism/DRA.java b/prism/src/prism/DRA.java index 92f4ea49..5a65fa75 100644 --- a/prism/src/prism/DRA.java +++ b/prism/src/prism/DRA.java @@ -196,49 +196,6 @@ public class DRA return acceptanceK.get(i); } - /** - * Is this Rabin automaton actually a Buchi automaton? This check is done syntactically: - * it returns true if L_i is empty for any acceptance pairs (L_i,K_i). - */ - public boolean isDBA() - { - int n = getNumAcceptancePairs(); - for (int i = 0; i < n; i++) { - if (!getAcceptanceL(i).isEmpty()) - return false; - } - return true; - } - - /** - * Is this Rabin automaton actually a finite automaton? This check is done syntactically: - * it returns true if every transition from a K_i state goes to another K_i state. - * We also require that there are no L_i states overlapping with any K_j states. - */ - public boolean isDFA() - { - // Compute union of all K_i sets - BitSet acc = new BitSet(); - int n = getNumAcceptancePairs(); - for (int i = 0; i < n; i++) { - acc.or(getAcceptanceK(i)); - } - // Make sure there are no L_i states in any K_j states - for (int i = 0; i < n; i++) { - if (acc.intersects(getAcceptanceL(i))) - return false; - } - // Check if every transition from a K_i state goes to another K_i state. - for (int i = acc.nextSetBit(0); i >= 0; i = acc.nextSetBit(i + 1)) { - int m = getNumEdges(i); - for (int j = 0; j < m; j++) { - if (!acc.get(getEdgeDest(i, j))) - return false; - } - } - return true; - } - /** * Print DRA in DOT format to an output stream. */ diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 9d2b9714..a2189d20 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -664,27 +664,6 @@ public class LTLModelChecker extends PrismComponent return statesKi; } - /** - * Find the set of states in a model corresponding to the "target" part of a Rabin acceptance condition, - * i.e. just the union of the K_i parts of the (L_i,K_i) pairs. - * @param dra The DRA storing the Rabin acceptance condition - * @param model The model - * @param draDDRowVars BDD row variables for the DRA part of the model - * @param draDDColVars BDD column variables for the DRA part of the model - * @return - */ - public JDDNode findTargetStatesForRabin(DRA dra, Model model, JDDVars draDDRowVars, JDDVars draDDColVars) - { - JDDNode acceptingStates = JDD.Constant(0); - for (int i = 0; i < dra.getNumAcceptancePairs(); i++) { - JDDNode tmpK = buildKStatesForRabinPair(draDDRowVars, dra, i); - acceptingStates = JDD.Or(acceptingStates, tmpK); - } - JDD.Ref(model.getReach()); - acceptingStates = JDD.And(model.getReach(), acceptingStates); - return acceptingStates; - } - /** * Find the set of accepting BSCCs in a model wrt a Rabin acceptance condition. * @param dra The DRA storing the Rabin acceptance condition diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 1aad841c..f356b1b4 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1013,17 +1013,9 @@ public class NondetModelChecker extends NonProbModelChecker out.close(); } - // Find accepting states + compute reachability probabilities - JDDNode acc = null; - if (dra.isDFA()) { - // For a DFA, just collect the accept states - mainLog.println("\nSkipping end component detection since DRA is a DFA..."); - acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars); - } else { - // Usually, we have to detect end components in the product - mainLog.println("\nFinding accepting end components..."); - acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness); - } + // Find accepting MECs + compute reachability probabilities + mainLog.println("\nFinding accepting end components..."); + JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new NondetModelChecker(prism, modelProduct, null); probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index a0f097ff..a001fc53 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -552,17 +552,9 @@ public class ProbModelChecker extends NonProbModelChecker out.close(); } - // Find accepting states + compute reachability probabilities - JDDNode acc = null; - if (dra.isDFA()) { - // For a DFA, just collect the accept states - mainLog.println("\nSkipping BSCC detection since DRA is a DFA..."); - acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars); - } else { - // Usually, we have to detect BSCCs in the product - mainLog.println("\nFinding accepting BSCCs..."); - acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars); - } + // Find accepting BSCCs + compute reachability probabilities + mainLog.println("\nFinding accepting BSCCs..."); + JDDNode acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars); mainLog.println("\nComputing reachability probabilities..."); mcProduct = createNewModelChecker(prism, modelProduct, null); probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual);