From 55025ee63b164aa84ef1669787c60e49e86efe05 Mon Sep 17 00:00:00 2001 From: Ernst Moritz Hahn Date: Tue, 26 Mar 2013 19:07:24 +0000 Subject: [PATCH] too slow git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6622 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCSimple.java | 14 +- prism/src/explicit/DTMC.java | 5 - prism/src/explicit/DTMCEmbeddedSimple.java | 6 - .../DTMCFromMDPMemorylessAdversary.java | 6 - prism/src/explicit/DTMCSimple.java | 78 ++--- prism/src/explicit/DTMCUniformisedSimple.java | 6 - prism/src/explicit/StateAction.java | 83 ----- .../src/explicit/StateActionDistribution.java | 329 ------------------ 8 files changed, 31 insertions(+), 496 deletions(-) delete mode 100644 prism/src/explicit/StateAction.java delete mode 100644 prism/src/explicit/StateActionDistribution.java diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java index b871b3e9..9731d2ef 100644 --- a/prism/src/explicit/CTMCSimple.java +++ b/prism/src/explicit/CTMCSimple.java @@ -137,7 +137,7 @@ public class CTMCSimple extends DTMCSimple implements CTMC public DTMCSimple buildEmbeddedDTMC() { DTMCSimple dtmc; - StateActionDistribution distr; + Distribution distr; int i; double d; dtmc = new DTMCSimple(numStates); @@ -150,8 +150,8 @@ public class CTMCSimple extends DTMCSimple implements CTMC if (d == 0) { dtmc.setProbability(i, i, 1.0); } else { - for (Map.Entry e : distr) { - dtmc.setProbability(i, e.getKey().getState(), e.getKey().getAction(), e.getValue() / d); + for (Map.Entry e : distr) { + dtmc.setProbability(i, e.getKey(), e.getValue() / d); } } } @@ -161,7 +161,7 @@ public class CTMCSimple extends DTMCSimple implements CTMC @Override public void uniformise(double q) { - StateActionDistribution distr; + Distribution distr; int i; for (i = 0; i < numStates; i++) { distr = trans.get(i); @@ -179,7 +179,7 @@ public class CTMCSimple extends DTMCSimple implements CTMC public DTMCSimple buildUniformisedDTMC(double q) { DTMCSimple dtmc; - StateActionDistribution distr; + Distribution distr; int i; double d; dtmc = new DTMCSimple(numStates); @@ -189,8 +189,8 @@ public class CTMCSimple extends DTMCSimple implements CTMC for (i = 0; i < numStates; i++) { // Add scaled off-diagonal entries distr = trans.get(i); - for (Map.Entry e : distr) { - dtmc.setProbability(i, e.getKey().getState(), e.getKey().getAction(), e.getValue() / q); + for (Map.Entry e : distr) { + dtmc.setProbability(i, e.getKey(), e.getValue() / q); } // Add diagonal, if needed d = distr.sumAllBut(i); diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 22c9e3d4..46c53e0e 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -46,11 +46,6 @@ public interface DTMC extends Model */ public Iterator> getTransitionsIterator(int s); - /** - * Get an iterator over the transitions from state s. - */ - public Iterator> getTransitionsActionIterator(int s); - /** * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset}, * set bit i of {@code result} iff there is a transition to a state in {@code u}. diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 9e067283..86b5985a 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -205,12 +205,6 @@ public class DTMCEmbeddedSimple extends DTMCExplicit throw new RuntimeException("Not implemented yet"); } - public Iterator> getTransitionsActionIterator(int s) - { - // TODO - throw new RuntimeException("Not implemented yet"); - } - public void prob0step(BitSet subset, BitSet u, BitSet result) { int i; diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index e6dcd943..a8996db5 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -185,12 +185,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit throw new RuntimeException("Not implemented yet"); } - public Iterator> getTransitionsActionIterator(int s) - { - // TODO - throw new RuntimeException("Not implemented yet"); - } - public void prob0step(BitSet subset, BitSet u, BitSet result) { // TODO diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 4f03c3fd..ec92d2b2 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -39,7 +39,7 @@ import prism.PrismException; public class DTMCSimple extends DTMCExplicit implements ModelSimple { // Transition matrix (distribution list) - protected List trans; + protected List trans; // Other statistics protected int numTransitions; @@ -70,7 +70,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple this(dtmc.numStates); copyFrom(dtmc); for (int i = 0; i < numStates; i++) { - trans.set(i, new StateActionDistribution(dtmc.trans.get(i))); + trans.set(i, new Distribution(dtmc.trans.get(i))); } numTransitions = dtmc.numTransitions; } @@ -87,7 +87,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple this(dtmc.numStates); copyFrom(dtmc, permut); for (int i = 0; i < numStates; i++) { - trans.set(permut[i], new StateActionDistribution(dtmc.trans.get(i), permut)); + trans.set(permut[i], new Distribution(dtmc.trans.get(i), permut)); } numTransitions = dtmc.numTransitions; } @@ -98,9 +98,9 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple public void initialise(int numStates) { super.initialise(numStates); - trans = new ArrayList(numStates); + trans = new ArrayList(numStates); for (int i = 0; i < numStates; i++) { - trans.add(new StateActionDistribution()); + trans.add(new Distribution()); } } @@ -126,7 +126,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple public void addStates(int numToAdd) { for (int i = 0; i < numToAdd; i++) { - trans.add(new StateActionDistribution()); + trans.add(new Distribution()); numStates++; } } @@ -185,7 +185,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple */ public void setProbability(int i, int j, double prob) { - StateActionDistribution distr = trans.get(i); + Distribution distr = trans.get(i); if (distr.get(i) != 0.0) numTransitions--; if (prob != 0.0) @@ -193,19 +193,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple distr.set(j, prob); } - /** - * Set the probability for a transition. - */ - public void setProbability(int i, int j, Object a, double prob) - { - StateActionDistribution distr = trans.get(i); - if (distr.get(i, a) != 0.0) - numTransitions--; - if (prob != 0.0) - numTransitions++; - distr.set(j, a, prob); - } - /** * Add to the probability for a transition. */ @@ -217,17 +204,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple } } - /** - * Add to the probability for a transition. - */ - public void addToProbability(int i, int j, int a, double prob) - { - if (!trans.get(i).add(j, a, prob)) { - if (prob != 0.0) - numTransitions++; - } - } - // Accessors (for Model) @Override @@ -241,7 +217,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { return trans.get(s).getSupport().iterator(); } - + @Override public boolean isSuccessor(int s1, int s2) { @@ -298,21 +274,15 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple @Override public Iterator> getTransitionsIterator(int s) - { - return trans.get(s).toDistribution().iterator(); - } - - @Override - public Iterator> getTransitionsActionIterator(int s) { return trans.get(s).iterator(); } - + @Override public void prob0step(BitSet subset, BitSet u, BitSet result) { int i; - StateActionDistribution distr; + Distribution distr; for (i = 0; i < numStates; i++) { if (subset.get(i)) { distr = trans.get(i); @@ -325,7 +295,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result) { int i; - StateActionDistribution distr; + Distribution distr; for (i = 0; i < numStates; i++) { if (subset.get(i)) { distr = trans.get(i); @@ -339,12 +309,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double d, prob; - StateActionDistribution distr; + Distribution distr; distr = trans.get(s); d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey().getState(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); prob = (Double) e.getValue(); d += prob * vect[k]; } @@ -357,13 +327,13 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double diag, d, prob; - StateActionDistribution distr; + Distribution distr; distr = trans.get(s); diag = 1.0; d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey().getState(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); prob = (Double) e.getValue(); if (k != s) { d += prob * vect[k]; @@ -382,12 +352,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double d, prob; - StateActionDistribution distr; + Distribution distr; distr = trans.get(s); d = mcRewards.getStateReward(s); - for (Map.Entry e : distr) { - k = (Integer) e.getKey().getState(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); prob = (Double) e.getValue(); d += prob * vect[k]; } @@ -400,7 +370,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int i, j; double prob; - StateActionDistribution distr; + Distribution distr; // Initialise result to 0 for (j = 0; j < numStates; j++) { @@ -409,8 +379,8 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple // Go through matrix elements (by row) for (i = 0; i < numStates; i++) { distr = trans.get(i); - for (Map.Entry e : distr) { - j = (Integer) e.getKey().getState(); + for (Map.Entry e : distr) { + j = (Integer) e.getKey(); prob = (Double) e.getValue(); result[j] += prob * vect[i]; } @@ -425,7 +395,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple */ public Distribution getTransitions(int s) { - return trans.get(s).toDistribution(); + return trans.get(s); } // Standard methods diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 53b27366..488377ea 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -209,12 +209,6 @@ public class DTMCUniformisedSimple extends DTMCExplicit throw new RuntimeException("Not implemented yet"); } - public Iterator> getTransitionsActionIterator(int s) - { - // TODO - throw new RuntimeException("Not implemented yet"); - } - public void prob0step(BitSet subset, BitSet u, BitSet result) { // TODO diff --git a/prism/src/explicit/StateAction.java b/prism/src/explicit/StateAction.java deleted file mode 100644 index cc9a028d..00000000 --- a/prism/src/explicit/StateAction.java +++ /dev/null @@ -1,83 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (University of Oxford) -// * Ernst Moritz Hahn (University of Oxford) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package explicit; - -/** - * Stores a state-action entry. - */ -public final class StateAction -{ - final int state; - final Object action; - - StateAction(int state, Object action) - { - this.state = state; - this.action = action; - } - - int getState() - { - return state; - } - - Object getAction() - { - return action; - } - - @Override - public boolean equals(Object obj) - { - if (!(obj instanceof StateAction)) { - return false; - } - - StateAction other = (StateAction) obj; - if (this.state != other.state) { - return false; - } - if ((this.action == null) != (other.action == null)) { - return false; - } - if (this.action == null) { - return true; - } - return (this.action.equals(other.action)); - } - - @Override - public int hashCode() - { - if (null != action) { - return state * 23 + action.hashCode(); - } else { - return state; - } - } -} diff --git a/prism/src/explicit/StateActionDistribution.java b/prism/src/explicit/StateActionDistribution.java deleted file mode 100644 index c9c67331..00000000 --- a/prism/src/explicit/StateActionDistribution.java +++ /dev/null @@ -1,329 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (University of Oxford) -// * Ernst Moritz Hahn (University of Oxford) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package explicit; - -import java.util.BitSet; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Map; -import java.util.Set; -import java.util.Map.Entry; - -import prism.PrismUtils; - -/** - * Stores a distributions over a state-action pairs. - */ -public class StateActionDistribution implements Iterable> -{ - private HashMap map; - - /** - * Create an empty distribution. - */ - public StateActionDistribution() - { - clear(); - } - - /** - * Copy constructor. - */ - public StateActionDistribution(StateActionDistribution distr) - { - this(); - Iterator> i = distr.iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - add(e.getKey(), e.getValue()); - } - } - - /** - * Construct a distribution from an existing one and a state index permutation, - * i.e. in which state index i becomes index permut[i]. - * Note: have to build the new distributions from scratch anyway to do this, - * so may as well provide this functionality as a constructor. - */ - public StateActionDistribution(StateActionDistribution distr, int permut[]) - { - this(); - Iterator> i = distr.iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - StateAction oldStateAction = e.getKey(); - StateAction newStateAction = new StateAction(permut[oldStateAction.getState()], oldStateAction.getAction()); - add(newStateAction, e.getValue()); - } - } - - /** - * Get probability for state state/action 0. - * - * @param state state to get probability of - * @return probability - */ - public double get(int state) - { - return get(state, null); - } - - /** - * Get the probability for state/action pair - */ - public double get(int state, Object action) - { - StateAction entry = new StateAction(state, action); - return get(entry); - } - - /** - * Get the probability for given entry - */ - public double get(StateAction entry) - { - Double d; - d = (Double) map.get(entry); - return d==null ? 0.0 : d.doubleValue(); - } - - @Override - public Iterator> iterator() - { - return map.entrySet().iterator(); - } - - /** - * Clear all entries of the distribution. - */ - public void clear() - { - map = new HashMap(); - } - - public boolean add(int state, double prob) - { - return add(state, null, prob); - } - - /** - * Add 'prob' to the probability for given state and action. - * Return boolean indicating whether or not there was already - * non-zero probability for this state (i.e. false denotes new transition). - */ - public boolean add(int state, Object action, double prob) - { - StateAction entry = new StateAction(state, action); - return add(entry, prob); - } - - public boolean add(StateAction entry, double prob) - { - Double d = (Double) map.get(entry); - if (d == null) { - map.put(entry, prob); - return false; - } else { - set(entry, d + prob); - return true; - } - } - - /** - * Set the probability for state/action to prob. - */ - public void set(int state, Object action, double prob) - { - StateAction entry = new StateAction(state, action); - set(entry, prob); - } - - public void set(int state, double prob) { - set(state, null, prob); - } - - public void set(StateAction entry, double prob) - { - if (prob == 0.0) - map.remove(entry); - else - map.put(entry, prob); - } - - /** - * Returns true if index j is in the support of the distribution. - */ - public boolean contains(int state, Object action) - { - StateAction entry = new StateAction(state, action); - return map.get(entry) != null; - } - - public boolean contains(int state) - { - return contains(state, null); - } - - /** - * Returns true if all states in the support of the distribution are in the set. - */ - public boolean isSubsetOf(BitSet set) - { - Iterator> i = iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - if (!set.get(((StateAction) e.getKey()).getState())) - return false; - } - return true; - } - - /** - * Get the support of the distribution. - */ - public Set getSupport() - { - HashSet support = new HashSet(); - for (StateAction stateAction : map.keySet()) { - support.add(stateAction.getState()); - } - return support; - } - - /** - * Returns true if the distribution is empty. - */ - public boolean isEmpty() - { - return map.isEmpty(); - } - - /** - * Get the size of the support of the distribution. - */ - public int size() - { - return map.size(); - } - - /** - * Get the sum of the probabilities in the distribution. - */ - public double sum() - { - double d = 0.0; - Iterator> i = iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - d += e.getValue(); - } - return d; - } - - /** - * Get the sum of all the probabilities in the distribution except for state j. - */ - public double sumAllBut(int j) - { - double d = 0.0; - Iterator> i = iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - if (e.getKey().getState() != j) - d += e.getValue(); - } - return d; - } - - /** - * Create a new distribution, based on a mapping from the state indices - * used in this distribution to a different set of state indices. - */ - public StateActionDistribution map(int map[]) - { - StateActionDistribution distrNew = new StateActionDistribution(); - Iterator> i = iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - StateAction oldStateAction = e.getKey(); - StateAction newStateAction = new StateAction(map[oldStateAction.getState()], oldStateAction.getAction()); - distrNew.add(newStateAction, e.getValue()); - } - return distrNew; - } - - @Override - public boolean equals(Object o) - { - Double d1, d2; - StateActionDistribution d = (StateActionDistribution) o; - if (d.size() != size()) - return false; - Iterator> i = iterator(); - while (i.hasNext()) { - Map.Entry e = i.next(); - d1 = e.getValue(); - d2 = d.map.get(e.getKey()); - if (d2 == null || !PrismUtils.doublesAreClose(d1, d2, 1e-12, false)) - return false; - } - return true; - } - - @Override - public int hashCode() - { - // Simple hash code - return map.size(); - } - - @Override - public String toString() - { - return map.toString(); - } - - public boolean containsOneOf(BitSet set) - { - for (StateAction stateAction : map.keySet()) { - if (set.get(stateAction.getState())); - } - return false; - } - - public Distribution toDistribution() - { - Distribution result = new Distribution(); - for (Entry entry : map.entrySet()) { - result.add(entry.getKey().getState(), entry.getValue()); - } - - return result; - } -}