From 4ae35b1bebcb4aa9637d5ed03c4574c771cc465d Mon Sep 17 00:00:00 2001 From: Ernst Moritz Hahn Date: Tue, 26 Mar 2013 18:32:27 +0000 Subject: [PATCH] began modifying for storing actions git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6621 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, 496 insertions(+), 31 deletions(-) create mode 100644 prism/src/explicit/StateAction.java create mode 100644 prism/src/explicit/StateActionDistribution.java diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java index 9731d2ef..b871b3e9 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; - Distribution distr; + StateActionDistribution 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(), e.getValue() / d); + for (Map.Entry e : distr) { + dtmc.setProbability(i, e.getKey().getState(), e.getKey().getAction(), e.getValue() / d); } } } @@ -161,7 +161,7 @@ public class CTMCSimple extends DTMCSimple implements CTMC @Override public void uniformise(double q) { - Distribution distr; + StateActionDistribution 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; - Distribution distr; + StateActionDistribution 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(), e.getValue() / q); + for (Map.Entry e : distr) { + dtmc.setProbability(i, e.getKey().getState(), e.getKey().getAction(), 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 46c53e0e..22c9e3d4 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -46,6 +46,11 @@ 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 86b5985a..9e067283 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -205,6 +205,12 @@ 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 a8996db5..e6dcd943 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -185,6 +185,12 @@ 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 ec92d2b2..4f03c3fd 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 Distribution(dtmc.trans.get(i))); + trans.set(i, new StateActionDistribution(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 Distribution(dtmc.trans.get(i), permut)); + trans.set(permut[i], new StateActionDistribution(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 Distribution()); + trans.add(new StateActionDistribution()); } } @@ -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 Distribution()); + trans.add(new StateActionDistribution()); numStates++; } } @@ -185,7 +185,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple */ public void setProbability(int i, int j, double prob) { - Distribution distr = trans.get(i); + StateActionDistribution distr = trans.get(i); if (distr.get(i) != 0.0) numTransitions--; if (prob != 0.0) @@ -193,6 +193,19 @@ 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. */ @@ -204,6 +217,17 @@ 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 @@ -217,7 +241,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { return trans.get(s).getSupport().iterator(); } - + @Override public boolean isSuccessor(int s1, int s2) { @@ -275,14 +299,20 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple @Override public Iterator> getTransitionsIterator(int s) { - return trans.get(s).iterator(); + 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; - Distribution distr; + StateActionDistribution distr; for (i = 0; i < numStates; i++) { if (subset.get(i)) { distr = trans.get(i); @@ -295,7 +325,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result) { int i; - Distribution distr; + StateActionDistribution distr; for (i = 0; i < numStates; i++) { if (subset.get(i)) { distr = trans.get(i); @@ -309,12 +339,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double d, prob; - Distribution distr; + StateActionDistribution distr; distr = trans.get(s); d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey().getState(); prob = (Double) e.getValue(); d += prob * vect[k]; } @@ -327,13 +357,13 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double diag, d, prob; - Distribution distr; + StateActionDistribution distr; distr = trans.get(s); diag = 1.0; d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey().getState(); prob = (Double) e.getValue(); if (k != s) { d += prob * vect[k]; @@ -352,12 +382,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int k; double d, prob; - Distribution distr; + StateActionDistribution distr; distr = trans.get(s); d = mcRewards.getStateReward(s); - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); + for (Map.Entry e : distr) { + k = (Integer) e.getKey().getState(); prob = (Double) e.getValue(); d += prob * vect[k]; } @@ -370,7 +400,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple { int i, j; double prob; - Distribution distr; + StateActionDistribution distr; // Initialise result to 0 for (j = 0; j < numStates; j++) { @@ -379,8 +409,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(); + for (Map.Entry e : distr) { + j = (Integer) e.getKey().getState(); prob = (Double) e.getValue(); result[j] += prob * vect[i]; } @@ -395,7 +425,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple */ public Distribution getTransitions(int s) { - return trans.get(s); + return trans.get(s).toDistribution(); } // Standard methods diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 488377ea..53b27366 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -209,6 +209,12 @@ 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 new file mode 100644 index 00000000..cc9a028d --- /dev/null +++ b/prism/src/explicit/StateAction.java @@ -0,0 +1,83 @@ +//============================================================================== +// +// 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 new file mode 100644 index 00000000..c9c67331 --- /dev/null +++ b/prism/src/explicit/StateActionDistribution.java @@ -0,0 +1,329 @@ +//============================================================================== +// +// 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; + } +}