diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index f83b7c9b..57bc7820 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -125,7 +125,7 @@ public class ConstructModel // Model info ModelType modelType; // State storage - IndexedSet states; + StateStorage states; LinkedList explore; State state, stateNew; // Explicit model storage diff --git a/prism/src/explicit/IndexedSet.java b/prism/src/explicit/IndexedSet.java index 5b4be9da..b2a0f0e3 100644 --- a/prism/src/explicit/IndexedSet.java +++ b/prism/src/explicit/IndexedSet.java @@ -28,13 +28,11 @@ package explicit; import java.util.*; -import parser.State; - /** * Class storing an indexed set of objects of type T. * Typically used for storing state space during reachability. */ -public class IndexedSet +public class IndexedSet implements StateStorage { private Map set; private int indexOfLastAdd; @@ -50,11 +48,13 @@ public class IndexedSet indexOfLastAdd = -1; } + @Override public void clear() { set.clear(); } + @Override public boolean add(T state) { Integer i = set.get(state); @@ -68,16 +68,19 @@ public class IndexedSet } } + @Override public boolean contains(T state) { return set.get(state) != null; } + @Override public int getIndexOfLastAdd() { return indexOfLastAdd; } + @Override public boolean isEmpty() { return set.isEmpty(); @@ -86,6 +89,7 @@ public class IndexedSet /** * Get the number of objects stored in the set. */ + @Override public int size() { return set.size(); @@ -94,6 +98,7 @@ public class IndexedSet /** * Get access to the underlying set of map entries. */ + @Override public Set> getEntrySet() { return set.entrySet(); @@ -102,6 +107,7 @@ public class IndexedSet /** * Create an ArrayList of the states, ordered by index. */ + @Override public ArrayList toArrayList() { ArrayList list = new ArrayList(set.size()); @@ -113,6 +119,7 @@ public class IndexedSet * Create an ArrayList of the states, ordered by index, storing in the passed in list. * @param list An empty ArrayList in which to store the result. */ + @Override public void toArrayList(ArrayList list) { int i, n; @@ -130,6 +137,7 @@ public class IndexedSet * Index in new list is permut[old_index]. * @param permut Permutation to apply */ + @Override public ArrayList toPermutedArrayList(int permut[]) { ArrayList list = new ArrayList(set.size()); @@ -143,6 +151,7 @@ public class IndexedSet * @param permut Permutation to apply * @param list An empty ArrayList in which to store the result. */ + @Override public void toPermutedArrayList(int permut[], ArrayList list) { int i, n; @@ -160,6 +169,7 @@ public class IndexedSet * this returns a permutation (integer array) mapping current indices * to new indices under the sorting order. */ + @Override public int[] buildSortingPermutation() { int i, n; @@ -181,6 +191,7 @@ public class IndexedSet return set.toString(); } + @Override public int get(T t) { return set.get(t); diff --git a/prism/src/explicit/StateStorage.java b/prism/src/explicit/StateStorage.java new file mode 100644 index 00000000..c92c5565 --- /dev/null +++ b/prism/src/explicit/StateStorage.java @@ -0,0 +1,94 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// * Mateusz Ujma (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.*; + +/** + * Interface for storing an set of objects of type T. + * Typically used for storing state space during reachability. + */ +public interface StateStorage +{ + public int get(T t); + + public boolean add(T state); + + public void clear(); + + public boolean contains(T state); + + public int getIndexOfLastAdd(); + + public boolean isEmpty(); + + /** + * Get the number of objects stored in the set. + */ + public int size(); + + /** + * Get access to the underlying set of map entries. + */ + public Set> getEntrySet(); + + /** + * Create an ArrayList of the states, ordered by index. + */ + public ArrayList toArrayList(); + + /** + * Create an ArrayList of the states, ordered by index, storing in the passed in list. + * @param list An empty ArrayList in which to store the result. + */ + public void toArrayList(ArrayList list); + + /** + * Create an ArrayList of the states, ordered by permuted index. + * Index in new list is permut[old_index]. + * @param permut Permutation to apply + */ + public ArrayList toPermutedArrayList(int permut[]); + + /** + * Create an ArrayList of the states, ordered by permuted index, storing in the passed in list. + * Index in new list is permut[old_index]. + * @param permut Permutation to apply + * @param list An empty ArrayList in which to store the result. + */ + public void toPermutedArrayList(int permut[], ArrayList list); + + /** + * Build sort permutation. Assuming this was built as a sorted set, + * this returns a permutation (integer array) mapping current indices + * to new indices under the sorting order. + */ + public int[] buildSortingPermutation(); + +} diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 0beffa9a..e31dcd27 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -41,6 +41,7 @@ import prism.PrismException; import prism.PrismLog; import prism.PrismSettings; import explicit.IndexedSet; +import explicit.StateStorage; /** * Class to construct a parametric Markov model. @@ -233,7 +234,7 @@ public final class ModelBuilder { * @param states list of states to be filled by this method * @throws PrismException thrown if problems in underlying methods occur */ - private void reserveMemoryAndExploreStates(ModulesFile modulesFile, ParamModel model, ModelType modelType, SymbolicEngine engine, IndexedSet states) + private void reserveMemoryAndExploreStates(ModulesFile modulesFile, ParamModel model, ModelType modelType, SymbolicEngine engine, StateStorage states) throws PrismException { boolean isNonDet = modelType == ModelType.MDP; @@ -311,7 +312,7 @@ public final class ModelBuilder { } boolean isNonDet = modelType == ModelType.MDP; - IndexedSet states = new IndexedSet(true); + StateStorage states = new IndexedSet(true); reserveMemoryAndExploreStates(modulesFile, model, modelType, engine, states); int[] permut = states.buildSortingPermutation(); List statesList = states.toPermutedArrayList(permut); diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index 89790632..b0ae2edd 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -89,7 +89,7 @@ public class ForwardsReach { LocZone init, lz, lz2; LinkedList X; - IndexedSet Yset; + StateStorage Yset; //LocZoneSetOld Zset; ReachabilityGraph graph; int src, dest, count, dests[]; @@ -272,7 +272,7 @@ public class ForwardsReach Zone z; LocZone init, lz, lz2; LinkedList Y; - IndexedSet Zset; + StateStorage Zset; //LocZoneSetOld Zset; ReachabilityGraph graph; int cMax; diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index 83128942..572cf4c5 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/prism/src/pta/Modules2PTA.java @@ -29,6 +29,7 @@ package pta; import java.util.*; import explicit.IndexedSet; +import explicit.StateStorage; import parser.*; import parser.ast.*; @@ -504,7 +505,7 @@ public class Modules2PTA extends PrismComponent int numUpdates, numCommands, numElements; // Stuff needed to do local reachability search int src, dest; - IndexedSet states; + StateStorage states; LinkedList explore; State state, stateNew; int[] varMap; diff --git a/prism/src/pta/PTAParallel.java b/prism/src/pta/PTAParallel.java index ad30d9ad..65bd5070 100644 --- a/prism/src/pta/PTAParallel.java +++ b/prism/src/pta/PTAParallel.java @@ -30,6 +30,7 @@ import java.util.*; import prism.PrismException; import explicit.IndexedSet; +import explicit.StateStorage; /** * Class to perform the parallel composition of PTAs. @@ -37,7 +38,7 @@ import explicit.IndexedSet; public class PTAParallel { // All states - private IndexedSet states; + private StateStorage states; // States to be explored private LinkedList explore; // Component PTAs