diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index ac03bf62..fe75b32b 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -620,11 +620,14 @@ public class LTLModelChecker extends PrismComponent } /** - * Computes sets of accepting states in a DTMC/CTMC for each Rabin acceptance pair - * - * @returns a referenced BDD of the union of all the accepting sets + * Find the set of accepting BSCCs in a model wrt a Rabin acceptance condition. + * @param dra The DRA storing the Rabin acceptance condition + * @param draDDRowVars BDD row variables for the DRA part of the model + * @param draDDColVars BDD column variables for the DRA part of the model + * @param model The model + * @returns A referenced BDD for the union of all states in accepting BSCCs */ - public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model) throws PrismException + public JDDNode findAcceptingBSCCsForRabin(DRA dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException { SCCComputer sccComputer; JDDNode acceptingStates, allAcceptingStates; @@ -689,11 +692,15 @@ public class LTLModelChecker extends PrismComponent } /** - * Computes sets of accepting states in an MDP for each Rabin acceptance pair - * - * @returns a referenced BDD of the union of all the accepting sets + * Find the set of states in accepting MEC in a nondeterministic model wrt a Rabin acceptance condition. + * @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 + * @param fairness Consider fairness? + * @returns A referenced BDD for the union of all states in accepting MECs */ - public JDDNode findAcceptingStates(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) throws PrismException + public JDDNode findAcceptingMECStatesForRabin(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) throws PrismException { JDDNode acceptingStates = null, allAcceptingStates, acceptanceVector_H, acceptanceVector_L, candidateStates; int i, j; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 5220bff9..d35e01d0 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1365,7 +1365,7 @@ public class NondetModelChecker extends NonProbModelChecker // Find accepting MECs + compute reachability probabilities mainLog.println("\nFinding accepting end components..."); - JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, draDDRowVars, draDDColVars, fairness); + JDDNode acc = mcLtl.findAcceptingMECStatesForRabin(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 51b62973..6c2e501f 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -612,7 +612,7 @@ public class ProbModelChecker extends NonProbModelChecker // Find accepting BSCCs + compute reachability probabilities mainLog.println("\nFinding accepting BSCCs..."); - JDDNode acc = mcLtl.findAcceptingBSCCs(dra, draDDRowVars, draDDColVars, modelProduct); + 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);