Added class for handling sub-models of NondetModel's

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7108 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago · 710d5b15b5
1 changed files with 388 additions and 0 deletions
--- a/prism/src/explicit/SubNondetModel.java
+++ b/prism/src/explicit/SubNondetModel.java
@ -0,0 +1,388 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk> (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.io.File;
+import java.io.NotSerializableException;
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.NoSuchElementException;
+
+import parser.State;
+import parser.Values;
+import parser.VarList;
+import prism.ModelType;
+import prism.PrismException;
+import prism.PrismLog;
+
+/*
+ * Class for creating a sub-model of any NondetModel, please note the translate* methods
+ * used to translate between state ids for model and sub-model. Created sub-model will have new 
+ * state numbering from 0 to number of states in the sub model.
+ * 
+ */
+
+public class SubNondetModel implements NondetModel {
+
+	private NondetModel model = null;
+	private BitSet states = null;
+	private Map<Integer,BitSet> actions = null;
+	private BitSet initialStates = null;
+	private List<State> statesList = null;
+	private Map<Integer,Integer> stateLookupTable = new HashMap<Integer,Integer>();
+	private Map<Integer,Map<Integer,Integer>> actionLookupTable = new HashMap<Integer,Map<Integer,Integer>>();
+	private Map<Integer,Integer> inverseStateLookupTable = new HashMap<Integer,Integer>();
+	
+	private int numTransitions = 0;
+	private int maxNumChoices = 0;
+	private int numChoices = 0;
+	
+	public SubNondetModel(NondetModel model, BitSet states, Map<Integer,BitSet> actions, BitSet initialStates) {
+		this.model = model;
+		this.states = states;
+		this.actions = actions;
+		this.initialStates = initialStates;
+		
+		generateStatistics();
+		generateLookupTable(states, actions);
+	}
+	
+	@Override
+	public ModelType getModelType() {
+		return model.getModelType();
+	}
+
+	@Override
+	public int getNumStates() {
+		return states.cardinality();
+	}
+
+	@Override
+	public int getNumInitialStates() {
+		return initialStates.cardinality();
+	}
+
+	@Override
+	public Iterable<Integer> getInitialStates() {
+		List<Integer> is = new ArrayList<Integer>();
+		for(int i=initialStates.nextSetBit(0); i>=0; i=initialStates.nextSetBit(i+1)) { 
+			is.add(translateState(i));
+		}
+		
+		return is;
+	}
+
+	@Override
+	public int getFirstInitialState() {
+		return translateState(initialStates.nextSetBit(0));
+	}
+
+	@Override
+	public boolean isInitialState(int i) {
+		return initialStates.get(translateState(i));
+	}
+
+	@Override
+	public int getNumDeadlockStates() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Iterable<Integer> getDeadlockStates() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public StateValues getDeadlockStatesList() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public int getFirstDeadlockState() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean isDeadlockState(int i) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	
+	public List<State> getStatesList() {
+		//We use lazy generation because in many cases the state list is not 
+		//needed
+		if(statesList == null) {
+			statesList = generateSubStateList(states);
+		}
+		return statesList;
+	}
+	
+	private List<State> generateSubStateList(BitSet states) {
+		List<State> statesList = new ArrayList<State>();
+		for(int i=0;i<model.getNumStates();i++) {
+			if(states.get(i)) {
+				statesList.add(model.getStatesList().get(i));
+			}
+		}
+		return statesList;
+	}
+
+	@Override
+	public Values getConstantValues() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public int getNumTransitions() {
+		return numTransitions;
+	}
+
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(int s) {
+		s = translateState(s);
+		
+		List<Integer> succ = new ArrayList<Integer>();
+		for(int i=0;i<model.getNumChoices(s);i++) {
+			if(actions.get(s).get(i)) {
+				Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(s,i);
+				while(it.hasNext()) {
+					int succc = it.next().getKey();
+					succ.add(inverseTranslateState(succc));
+				}
+			}
+		}
+		return succ.iterator();
+	}
+		
+
+	@Override
+	public boolean isSuccessor(int s1, int s2) {
+		s1 = translateState(s1);
+		s2 = translateState(s2);
+		return model.isSuccessor(s1, s2);
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, BitSet set) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, BitSet set) {
+		throw new UnsupportedOperationException();
+	}
+	
+	@Override
+	public void findDeadlocks(boolean fix) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void checkForDeadlocks() throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void checkForDeadlocks(BitSet except) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismExplicit(String baseFilename)
+			throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(String filename) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(File file) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(PrismLog log) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToDotFile(String filename) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToDotFile(String filename, BitSet mark)
+			throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismLanguage(String filename) throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportStates(int exportType, VarList varList, PrismLog log)
+			throws PrismException {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public String infoString() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public String infoStringTable() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public int getNumChoices(int s) {
+		s = translateState(s);
+		return actions.get(s).cardinality();
+	}
+
+	@Override
+	public int getMaxNumChoices() {
+		return maxNumChoices;
+	}
+
+	@Override
+	public int getNumChoices() {
+		return numChoices;
+	}
+
+	@Override
+	public Object getAction(int s, int i) {
+		s = translateState(s);
+		i = translateAction(s, i);
+		
+		return model.getAction(s, i);
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, int i, BitSet set) {
+		s = translateState(s);
+		i = translateAction(s, i);
+		set = translateSet(set);
+
+		return model.allSuccessorsInSet(s, i, set);
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set) {
+		s = translateState(s);
+		i = translateAction(s, i);
+		set = translateSet(set);
+
+		return model.someSuccessorsInSet(s, i, set);
+	}
+	
+	private BitSet translateSet(BitSet set) {
+		BitSet translatedBitSet = new BitSet();
+		 for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i+1)) {
+			 translatedBitSet.set(translateState(i));
+		 }
+		 return translatedBitSet;
+	}
+	
+	private void generateStatistics() {
+		for(int i=0;i<model.getNumStates();i++) {
+			if(states.get(i)) {	
+				numTransitions += getTransitions(i);
+				numChoices += actions.get(i).cardinality();
+				maxNumChoices = Math.max(maxNumChoices, model.getNumChoices(i));
+			}
+		}
+	}
+	
+	private int getTransitions(int state) {
+		int transitions = 0;
+		for(int i=0;i<model.getNumChoices(state);i++) {
+			Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(state, i);
+			while(it.hasNext()) {
+				it.next();
+				transitions += 1;
+			}
+		}
+		return transitions;
+	}
+
+	@Override
+	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i) {
+		s = translateState(s);
+		i = translateAction(s, i);
+		
+		Map<Integer,Double> distrs = new HashMap<Integer, Double>();
+		Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(s, i);
+		while(it.hasNext()) {
+			Entry<Integer, Double> e = it.next();
+			int succ = inverseTranslateState(e.getKey());
+			distrs.put(succ, e.getValue());
+		}
+		return distrs.entrySet().iterator();
+	}
+	
+	private void generateLookupTable(BitSet states, Map<Integer,BitSet> actions) {
+		for(int i=0;i < model.getNumStates();i++) {
+			if(states.get(i)) {
+				inverseStateLookupTable.put(i, stateLookupTable.size());
+				stateLookupTable.put(stateLookupTable.size(),i);
+				Map<Integer,Integer> r = new HashMap<Integer,Integer>();
+				for(int j=0;j<model.getNumChoices(i);j++) {
+					if(actions.get(i).get(j)) {
+						r.put(r.size(),j);
+					}
+				}
+				actionLookupTable.put(actionLookupTable.size(),r);
+			}
+		}
+	}
+	
+	public int translateState(int s) {
+		return stateLookupTable.get(s);
+	}
+	
+	private int inverseTranslateState(int s) {
+		return inverseStateLookupTable.get(s);
+	}
+	
+	public int translateAction(int s, int i) {
+		return actionLookupTable.get(s).get(i);
+	}
+}