From 5072898b17b4e567be1b8a490099a9d063ee6301 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 16:56:10 +0000 Subject: [PATCH] symbolic ECComputerDefault: remove the two numeric methods in EC computations findMaximalStableSetOld has not been in use since 2013 (replaced by findMaximalStableset), maxStableSetTrans is replaced by getStableTransReln. Methods were private, so we just remove instead of marking as deprecated. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12029 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ECComputerDefault.java | 64 -------------------------- 1 file changed, 64 deletions(-) diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java index 583a14bd..3e2d10b4 100644 --- a/prism/src/prism/ECComputerDefault.java +++ b/prism/src/prism/ECComputerDefault.java @@ -147,68 +147,4 @@ public class ECComputerDefault extends ECComputer return mecs; } - /** - * Returns the maximal stable set of states contained in {@code candidateStates}, - * i.e. the maximal subset of states which have a choice whose transitions remain in the subset. - * @param candidateStates BDD for a set of states (over allDDRowVars) (dereferenced after calling this function) - * @return A referenced BDD with the maximal stable set in c - * - * Old version of the code (uses probability sum, which shouldn't be needed). - */ - private JDDNode findMaximalStableSetOld(JDDNode candidateStates) - { - JDDNode old = JDD.Constant(0); - JDDNode current = candidateStates; - - while (!current.equals(old)) { - JDD.Deref(old); - JDD.Ref(current); - old = current; - - JDD.Ref(current); - JDD.Ref(trans); - // Select transitions starting in current - JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, current); - // Select transitions starting in current and ending in current - JDDNode tmp = JDD.PermuteVariables(current, allDDRowVars, allDDColVars); - tmp = JDD.Apply(JDD.TIMES, currTrans, tmp); - // Sum all successor probabilities for each (state, action) tuple - tmp = JDD.SumAbstract(tmp, allDDColVars); - // If the sum for a (state,action) tuple is 1, - // there is an action that remains in the stable set with prob 1 - tmp = JDD.GreaterThan(tmp, 1 - sumRoundOff); - // Without fairness, we just need one action per state - current = JDD.ThereExists(tmp, allDDNondetVars); - } - JDD.Deref(old); - return current; - } - - /** - * Returns the transition relation of a stable set - * - * @param b BDD of a stable set (dereferenced after calling this function) - * @return referenced BDD of the transition relation restricted to the stable set - */ - private JDDNode maxStableSetTrans(JDDNode b) - { - - JDD.Ref(b); - JDD.Ref(trans); - // Select transitions starting in b - JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b); - JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars); - // Select transitions starting in current and ending in current - mask = JDD.Apply(JDD.TIMES, currTrans, mask); - // Sum all successor probabilities for each (state, action) tuple - mask = JDD.SumAbstract(mask, allDDColVars); - // If the sum for a (state,action) tuple is 1, - // there is an action that remains in the stable set with prob 1 - mask = JDD.GreaterThan(mask, 1 - sumRoundOff); - // select the transitions starting in these tuples - JDD.Ref(trans01); - JDDNode stableTrans01 = JDD.And(trans01, mask); - // Abstract over actions - return JDD.ThereExists(stableTrans01, allDDNondetVars); - } }