From 5cb056daf510f51b6f074d8aff0210a67760c51c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 26 May 2019 16:24:17 +0100 Subject: [PATCH] Add ModelGenerator interface for explicit model storage (ModelModelGenerator). This allows, for example, simulation of imported models: `prism dice.pm -exportmodel dice.all` `prism -importmodel dice.all -ex -sim -pf 'R=?[F s=7]'` `prism -importmodel dice.all -ex -simpath 10,rewards=true stdout` --- prism/src/explicit/ModelModelGenerator.java | 185 ++++++++++++++++++ .../prism/ExplicitFilesRewardGenerator.java | 28 ++- prism/src/prism/Prism.java | 7 +- 3 files changed, 217 insertions(+), 3 deletions(-) create mode 100644 prism/src/explicit/ModelModelGenerator.java diff --git a/prism/src/explicit/ModelModelGenerator.java b/prism/src/explicit/ModelModelGenerator.java new file mode 100644 index 00000000..50970600 --- /dev/null +++ b/prism/src/explicit/ModelModelGenerator.java @@ -0,0 +1,185 @@ +//============================================================================== +// +// Copyright (c) 2019- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// 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.ArrayList; +import java.util.Iterator; +import java.util.List; +import java.util.Map; + +import parser.State; +import parser.VarList; +import parser.type.Type; +import prism.ModelGenerator; +import prism.ModelInfo; +import prism.ModelType; +import prism.PrismException; +import prism.PrismNotSupportedException; + +/** + * Class that implements the ModelGenerator interface using an explicit model. + * Allows e.g. simulation of a built model. + */ +public class ModelModelGenerator implements ModelGenerator +{ + // Explicit model + info + private Model model; + private ModelInfo modelInfo; + + /** Index of the state current being explored */ + private int sExplore = -1; + + // Temporary storage of transitions for a state + + private class Transitions + { + Object action; + List succs; + List probs; + + public Transitions() + { + action = null; + succs = new ArrayList<>(); + probs = new ArrayList<>(); + } + } + + private List trans = new ArrayList<>(); + + public ModelModelGenerator(Model model, ModelInfo modelInfo) + { + this.model = model; + this.modelInfo = modelInfo; + } + + @Override + public ModelType getModelType() + { + return model.getModelType(); + } + + @Override + public List getVarNames() + { + return modelInfo.getVarNames(); + } + + @Override + public List getVarTypes() + { + return modelInfo.getVarTypes(); + } + + @Override + public VarList createVarList() throws PrismException + { + return modelInfo.createVarList(); + } + + @Override + public State getInitialState() throws PrismException + { + int sInitial = model.getFirstInitialState(); + return model.getStatesList().get(sInitial); + } + + @Override + public void exploreState(State exploreState) throws PrismException + { + // Look up index of state to explore + sExplore = model.getStatesList().indexOf(exploreState); + // Extract transitions and store + trans.clear(); + switch (model.getModelType()) { + case CTMC: + storeTransitions(null, ((CTMC) model).getTransitionsIterator(sExplore)); + break; + case DTMC: + storeTransitions(null, ((DTMC) model).getTransitionsIterator(sExplore)); + break; + case MDP: + int numChoices = ((MDP) model).getNumChoices(sExplore); + for (int i = 0; i < numChoices; i++) { + Object action = ((MDP) model).getAction(sExplore, i); + storeTransitions(action, ((MDP) model).getTransitionsIterator(sExplore, i)); + } + break; + case CTMDP: + case LTS: + case PTA: + case SMG: + default: + throw new PrismNotSupportedException("Model generation not supported for " + model.getModelType() + "s"); + } + } + + /** + * Store the transitions extracted from an action and Model-provided iterator. + */ + private void storeTransitions(Object action, Iterator> transitionsIterator) + { + Transitions t = new Transitions(); + t.action = action; + while (transitionsIterator.hasNext()) { + Map.Entry e = transitionsIterator.next(); + t.succs.add(e.getKey()); + t.probs.add(e.getValue()); + } + trans.add(t); + } + + @Override + public int getNumChoices() throws PrismException + { + return trans.size(); + } + + @Override + public int getNumTransitions(int i) throws PrismException + { + return trans.get(i).succs.size(); + } + + @Override + public Object getTransitionAction(int i, int offset) throws PrismException + { + return trans.get(i).action; + } + + @Override + public double getTransitionProbability(int i, int offset) throws PrismException + { + return trans.get(i).probs.get(offset); + } + + @Override + public State computeTransitionTarget(int i, int offset) throws PrismException + { + return model.getStatesList().get(trans.get(i).succs.get(offset)); + } +} diff --git a/prism/src/prism/ExplicitFilesRewardGenerator.java b/prism/src/prism/ExplicitFilesRewardGenerator.java index 5475b26d..78ba8c86 100644 --- a/prism/src/prism/ExplicitFilesRewardGenerator.java +++ b/prism/src/prism/ExplicitFilesRewardGenerator.java @@ -33,12 +33,16 @@ import java.io.IOException; import java.util.Collections; import java.util.List; +import parser.State; + public class ExplicitFilesRewardGenerator extends PrismComponent implements RewardGenerator { // File(s) to read in rewards from private File stateRewardsFile; // Model info private int numStates; + // State list (optionally) + private List statesList = null; // Local storage of rewards private boolean stateRewardsLoaded = false; private double[] stateRewards; @@ -61,6 +65,15 @@ public class ExplicitFilesRewardGenerator extends PrismComponent implements Rewa this.numStates = numStates; } + /** + * Optionally, provide a list of model states, + * so that rewards can be looked up by State object, as well as state index. + */ + public void setStatesList(List statesList) + { + this.statesList = statesList; + } + /** * Extract the state rewards from the file and store locally. */ @@ -120,7 +133,20 @@ public class ExplicitFilesRewardGenerator extends PrismComponent implements Rewa @Override public boolean isRewardLookupSupported(RewardLookup lookup) { - return lookup == RewardLookup.BY_STATE_INDEX; + return (lookup == RewardLookup.BY_STATE_INDEX) || (lookup == RewardLookup.BY_STATE && statesList != null); + } + + @Override + public double getStateReward(int r, State state) throws PrismException + { + if (statesList == null) { + throw new PrismException("Reward lookup by State not possible since state list is missing"); + } + int s = statesList.indexOf(state); + if (s == -1) { + throw new PrismException("Unknown state " + state); + } + return getStateReward(r, s); } @Override diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 4ec3980f..5f646b05 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -42,6 +42,7 @@ import explicit.DTMCModelChecker; import explicit.ExplicitFiles2Model; import explicit.FastAdaptiveUniformisation; import explicit.FastAdaptiveUniformisationModelChecker; +import explicit.ModelModelGenerator; import hybrid.PrismHybrid; import jdd.JDD; import jdd.JDDNode; @@ -2123,8 +2124,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener currentModelInfo, explicitFilesNumStates); } else { currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModelInfo, explicitFilesNumStates); - currentModelGenerator = null; - currentRewardGenerator = new ExplicitFilesRewardGenerator(this, explicitFilesStateRewardsFile, explicitFilesNumStates); + currentModelGenerator = new ModelModelGenerator(currentModelExpl, currentModelInfo); + ExplicitFilesRewardGenerator efrg = new ExplicitFilesRewardGenerator(this, explicitFilesStateRewardsFile, explicitFilesNumStates); + efrg.setStatesList(currentModelExpl.getStatesList()); + currentRewardGenerator = efrg; } break; default: