From 710d5b15b54991db59e1384e8eb750b1dffd141a Mon Sep 17 00:00:00 2001 From: Mateusz Ujma Date: Sun, 21 Jul 2013 15:43:07 +0000 Subject: [PATCH] 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 --- prism/src/explicit/SubNondetModel.java | 388 +++++++++++++++++++++++++ 1 file changed, 388 insertions(+) create mode 100644 prism/src/explicit/SubNondetModel.java diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java new file mode 100644 index 00000000..295bb9ec --- /dev/null +++ b/prism/src/explicit/SubNondetModel.java @@ -0,0 +1,388 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/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.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 actions = null; + private BitSet initialStates = null; + private List statesList = null; + private Map stateLookupTable = new HashMap(); + private Map> actionLookupTable = new HashMap>(); + private Map inverseStateLookupTable = new HashMap(); + + private int numTransitions = 0; + private int maxNumChoices = 0; + private int numChoices = 0; + + public SubNondetModel(NondetModel model, BitSet states, Map 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 getInitialStates() { + List is = new ArrayList(); + 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 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 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 generateSubStateList(BitSet states) { + List statesList = new ArrayList(); + for(int i=0;i getSuccessorsIterator(int s) { + s = translateState(s); + + List succ = new ArrayList(); + for(int i=0;i> 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> it = model.getTransitionsIterator(state, i); + while(it.hasNext()) { + it.next(); + transitions += 1; + } + } + return transitions; + } + + @Override + public Iterator> getTransitionsIterator(int s, int i) { + s = translateState(s); + i = translateAction(s, i); + + Map distrs = new HashMap(); + Iterator> it = model.getTransitionsIterator(s, i); + while(it.hasNext()) { + Entry e = it.next(); + int succ = inverseTranslateState(e.getKey()); + distrs.put(succ, e.getValue()); + } + return distrs.entrySet().iterator(); + } + + private void generateLookupTable(BitSet states, Map actions) { + for(int i=0;i < model.getNumStates();i++) { + if(states.get(i)) { + inverseStateLookupTable.put(i, stateLookupTable.size()); + stateLookupTable.put(stateLookupTable.size(),i); + Map r = new HashMap(); + for(int j=0;j