From 19ec2f0a76b8f0d0f4359d34b57469b23d08da98 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 8 Sep 2016 22:35:35 +0000 Subject: [PATCH] Refactor parametric model construction to use an extension of ModelGenerator instead of reading specifically from a ModulesFile. Needs further refactoring. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11793 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/FunctionFactory.java | 2 +- prism/src/param/ModelBuilder.java | 102 ++-- prism/src/param/TransitionList.java | 10 + prism/src/prism/ModelGeneratorSymbolic.java | 173 +++++++ prism/src/prism/Prism.java | 5 +- .../ModulesFileModelGeneratorSymbolic.java | 465 ++++++++++++++++++ 6 files changed, 698 insertions(+), 59 deletions(-) create mode 100644 prism/src/prism/ModelGeneratorSymbolic.java create mode 100644 prism/src/simulator/ModulesFileModelGeneratorSymbolic.java diff --git a/prism/src/param/FunctionFactory.java b/prism/src/param/FunctionFactory.java index c711e7c4..c40afabb 100644 --- a/prism/src/param/FunctionFactory.java +++ b/prism/src/param/FunctionFactory.java @@ -34,7 +34,7 @@ import java.util.HashMap; * @see Function * @author Ernst Moritz Hahn (University of Oxford) */ -abstract class FunctionFactory { +public abstract class FunctionFactory { /** names of parameters */ protected String[] parameterNames; /** lower bounds of parameters */ diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index a378a252..de0272ae 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -42,11 +42,13 @@ import parser.ast.ExpressionLiteral; import parser.ast.ExpressionUnaryOp; import parser.ast.ModulesFile; import parser.visitor.ASTTraverseModify; +import prism.ModelGeneratorSymbolic; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; import prism.PrismLangException; import prism.PrismSettings; +import simulator.ModulesFileModelGenerator; import prism.PrismNotSupportedException; import explicit.IndexedSet; import explicit.StateStorage; @@ -59,9 +61,9 @@ import explicit.StateStorage; */ public final class ModelBuilder extends PrismComponent { - /** {@code ModulesFile} to be transformed to a {@code ParamModel} */ - private ModulesFile modulesFile; - /** parametric model constructed from {@code modulesFile} */ + /** the ModelGeneratorSymbolic interface providing the model to be transformed to a {@code ParamModel} */ + private ModelGeneratorSymbolic modelGenSym; + /** parametric model constructed */ private ParamModel model; /** function factory used in the constructed parametric model */ private FunctionFactory functionFactory; @@ -104,7 +106,7 @@ public final class ModelBuilder extends PrismComponent * @return rational function representing the given PRISM expression * @throws PrismException thrown if {@code expr} cannot be represented as rational function */ - Function expr2function(FunctionFactory factory, Expression expr) throws PrismException + public Function expr2function(FunctionFactory factory, Expression expr) throws PrismException { if (expr instanceof ExpressionLiteral) { String exprString = ((ExpressionLiteral) expr).getString(); @@ -114,16 +116,15 @@ public final class ModelBuilder extends PrismComponent return factory.fromBigRational(new BigRational(exprString)); } else if (expr instanceof ExpressionConstant) { String exprString = ((ExpressionConstant) expr).getName(); - int index = modulesFile.getConstantList().getConstantIndex(exprString); - if (index != -1) { - Expression constExpr = modulesFile.getConstantList().getConstant(index); - if (constExpr != null) { - return expr2function(factory, constExpr); - } else { - return factory.getVar(exprString); - } + if (modelGenSym.getConstantValues().contains(exprString)) { + Object val = modelGenSym.getConstantValues().getValueOf(exprString); + return factory.fromBigRational(new BigRational(val.toString())); + } + Expression constExpr = modelGenSym.getUnknownConstantDefinition(exprString); + if (constExpr == null) { + return factory.getVar(exprString); } else { - throw new PrismException("Invalid parametric constant definition used"); + return expr2function(factory, constExpr); } } else if (expr instanceof ExpressionBinaryOp) { ExpressionBinaryOp binExpr = ((ExpressionBinaryOp) expr); @@ -195,13 +196,11 @@ public final class ModelBuilder extends PrismComponent // setters and getters /** - * Set modules file to be transformed to parametric Markov model. - * - * @param modulesFile modules file to be transformed to parametric Markov model + * Set generator of model to be transformed to parametric Markov model. */ - public void setModulesFile(ModulesFile modulesFile) + public void setModelGenerator(ModelGeneratorSymbolic modelGenSym) throws PrismException { - this.modulesFile = modulesFile; + this.modelGenSym = modelGenSym; } /** @@ -252,7 +251,9 @@ public final class ModelBuilder extends PrismComponent } long time; - if (modulesFile.getModelType() == ModelType.PTA) { + modelGenSym.setSymbolic(this, functionFactory); + + if (modelGenSym.getModelType() == ModelType.PTA) { throw new PrismNotSupportedException("You cannot build a PTA model explicitly, only perform model checking"); } @@ -264,7 +265,7 @@ public final class ModelBuilder extends PrismComponent // (but do this *symbolically* - partly because some constants are parameters and therefore unknown, // but also to keep values like 1/3 as expressions rather than being converted to doubles, // resulting in a loss of precision) - ConstantList constantList = modulesFile.getConstantList(); + /*ConstantList constantList = modulesFile.getConstantList(); constExprs = constantList.evaluateConstantsPartially(modulesFile.getUndefinedConstantValues(), null); modulesFile = (ModulesFile) modulesFile.deepCopy(); modulesFile = (ModulesFile) modulesFile.accept(new ASTTraverseModify() @@ -274,8 +275,8 @@ public final class ModelBuilder extends PrismComponent Expression expr = constExprs.get(e.getName()); return (expr != null) ? expr.deepCopy() : e; } - }); - ParamModel modelExpl = constructModel(modulesFile); + });*/ + ParamModel modelExpl = constructModel(modelGenSym); time = System.currentTimeMillis() - time; mainLog.print("\n"+modelExpl.infoStringTable()); @@ -305,35 +306,34 @@ public final class ModelBuilder extends PrismComponent * @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, StateStorage states) - throws PrismException + private void reserveMemoryAndExploreStates(ModelGeneratorSymbolic modelGenSym, ParamModel model, StateStorage states) throws PrismException { - boolean isNonDet = modelType == ModelType.MDP; + boolean isNonDet = modelGenSym.getModelType().nondeterministic(); int numStates = 0; int numTotalChoices = 0; int numTotalSuccessors = 0; LinkedList explore = new LinkedList(); - State state = modulesFile.getDefaultInitialState(); + State state = modelGenSym.getInitialState(); states.add(state); explore.add(state); numStates++; while (!explore.isEmpty()) { state = explore.removeFirst(); - TransitionList tranlist = engine.calculateTransitions(state, true); // Suppress warnings - int numChoices = tranlist.getNumChoices(); + modelGenSym.exploreState(state); + int numChoices = modelGenSym.getNumChoices(); if (isNonDet) { numTotalChoices += numChoices; } else { numTotalChoices += 1; } for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { - int numSuccessors = tranlist.getChoice(choiceNr).size(); + int numSuccessors = modelGenSym.getNumTransitions(choiceNr); numTotalSuccessors += numSuccessors; for (int succNr = 0; succNr < numSuccessors; succNr++) { - State stateNew = tranlist.getChoice(choiceNr).computeTarget(succNr, state); + State stateNew = modelGenSym.computeTransitionTarget(choiceNr, succNr); if (states.add(stateNew)) { numStates++; explore.add(stateNew); @@ -359,11 +359,11 @@ public final class ModelBuilder extends PrismComponent * @return parametric model constructed * @throws PrismException thrown if model cannot be constructed */ - private ParamModel constructModel(ModulesFile modulesFile) throws PrismException + private ParamModel constructModel(ModelGeneratorSymbolic modelGenSym) throws PrismException { ModelType modelType; - if (modulesFile.getInitialStates() != null) { + if (!modelGenSym.hasSingleInitialState()) { throw new PrismNotSupportedException("Cannot do explicit-state reachability if there are multiple initial states"); } @@ -372,45 +372,38 @@ public final class ModelBuilder extends PrismComponent mainLog.print("\nComputing reachable states..."); mainLog.flush(); long timer = System.currentTimeMillis(); - modelType = modulesFile.getModelType(); + modelType = modelGenSym.getModelType(); ParamModel model = new ParamModel(); model.setModelType(modelType); if (modelType != ModelType.DTMC && modelType != ModelType.CTMC && modelType != ModelType.MDP) { throw new PrismNotSupportedException("Unsupported model type: " + modelType); } - SymbolicEngine engine = new SymbolicEngine(modulesFile, this, functionFactory); - - if (modulesFile.getInitialStates() != null) { - throw new PrismNotSupportedException("Explicit model construction does not support multiple initial states"); - } + // need? SymbolicEngine engine = new SymbolicEngine(modulesFile, this, functionFactory); boolean isNonDet = modelType == ModelType.MDP; boolean isContinuous = modelType == ModelType.CTMC; StateStorage states = new IndexedSet(true); - reserveMemoryAndExploreStates(modulesFile, model, modelType, engine, states); + reserveMemoryAndExploreStates(modelGenSym, model, states); int[] permut = states.buildSortingPermutation(); List statesList = states.toPermutedArrayList(permut); model.setStatesList(statesList); model.addInitialState(permut[0]); int stateNr = 0; for (State state : statesList) { - TransitionList tranlist = engine.calculateTransitions(state, false); - int numChoices = tranlist.getNumChoices(); - + modelGenSym.exploreState(state); + int numChoices = modelGenSym.getNumChoices(); boolean computeSumOut = !isNonDet; boolean checkChoiceSumEqualsOne = doProbChecks && model.getModelType().choicesSumToOne(); // sumOut = the sum over all outgoing choices from this state Function sumOut = functionFactory.getZero(); for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { - ChoiceListFlexi choice = tranlist.getChoice(choiceNr); - int numSuccessors = choice.size(); + int numSuccessors = modelGenSym.getNumTransitions(choiceNr); // sumOutForChoice = the sum over all outgoing transitions for this choice Function sumOutForChoice = functionFactory.getZero(); for (int succNr = 0; succNr < numSuccessors; succNr++) { - ChoiceListFlexi succ = tranlist.getChoice(choiceNr); - Function probFunc = succ.getProbability(succNr); + Function probFunc = modelGenSym.getTransitionProbabilityFunction(choiceNr, succNr); if (computeSumOut) sumOut = sumOut.add(probFunc); if (checkChoiceSumEqualsOne) @@ -421,9 +414,9 @@ public final class ModelBuilder extends PrismComponent if (sumOutForChoice.isConstant()) { // as the sum is constant, we know that it is really not 1 throw new PrismLangException("Probabilities sum to " + sumOutForChoice.asBigRational() + " instead of 1 in state " - + state.toString(modulesFile) + " for some command"); + + state.toString(modelGenSym) + " for some command"); } else { - throw new PrismLangException("In state " + state.toString(modulesFile) + " the probabilities sum to " + throw new PrismLangException("In state " + state.toString(modelGenSym) + " the probabilities sum to " + sumOutForChoice + " for some command, which can not be determined to be equal to 1 (to ignore, use -noprobchecks option)"); } } @@ -435,20 +428,17 @@ public final class ModelBuilder extends PrismComponent sumOut = functionFactory.getOne(); } for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { - ChoiceListFlexi choice = tranlist.getChoice(choiceNr); - int a = tranlist.getTransitionModuleOrActionIndex(tranlist.getTotalIndexOfTransition(choiceNr, 0)); - String action = a < 0 ? null : modulesFile.getSynch(a - 1); - int numSuccessors = choice.size(); + Object action = modelGenSym.getChoiceAction(choiceNr); + int numSuccessors = modelGenSym.getNumTransitions(choiceNr); for (int succNr = 0; succNr < numSuccessors; succNr++) { - ChoiceListFlexi succ = tranlist.getChoice(choiceNr); - State stateNew = succ.computeTarget(succNr, state); - Function probFn = succ.getProbability(succNr); + State stateNew = modelGenSym.computeTransitionTarget(choiceNr, succNr); + Function probFn = modelGenSym.getTransitionProbabilityFunction(choiceNr, succNr); // divide by sumOut // for DTMC, this normalises over the choices // for CTMC this builds the embedded DTMC // for MDP this does nothing (sumOut is set to 1) probFn = probFn.divide(sumOut); - model.addTransition(permut[states.get(stateNew)], probFn, action); + model.addTransition(permut[states.get(stateNew)], probFn, action == null ? "" : action.toString()); } if (isNonDet) { model.setSumLeaving(isContinuous ? sumOut : functionFactory.getOne()); diff --git a/prism/src/param/TransitionList.java b/prism/src/param/TransitionList.java index d2bc90e0..60b1556a 100644 --- a/prism/src/param/TransitionList.java +++ b/prism/src/param/TransitionList.java @@ -199,6 +199,16 @@ public class TransitionList return getChoiceOfTransition(index).getModuleOrActionIndex(); } + /** + * Get the index of the action/module of a choice, specified by its index. + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ + public int getChoiceModuleOrActionIndex(int index) + { + return getChoice(index).getModuleOrActionIndex(); + } + /** * Get the probability/rate of a transition, specified by its index. */ diff --git a/prism/src/prism/ModelGeneratorSymbolic.java b/prism/src/prism/ModelGeneratorSymbolic.java new file mode 100644 index 00000000..85d45cc7 --- /dev/null +++ b/prism/src/prism/ModelGeneratorSymbolic.java @@ -0,0 +1,173 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Nishan Kamaleson (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 prism; + +import java.util.List; + +import param.Function; +import param.FunctionFactory; +import param.ModelBuilder; +import parser.State; +import parser.ast.Expression; + +/** + * Interface for classes that generate a probabilistic model: + * given a particular model state (represented as a State object), + * they provide information about the outgoing transitions from that state. + */ +public interface ModelGeneratorSymbolic extends ModelInfo +{ + /** + * Does the model have a single initial state? + */ + public boolean hasSingleInitialState() throws PrismException; + + /** + * Get the initial states of the model. + * The returned list should contain fresh State objects that can be kept/modified. + */ + public List getInitialStates() throws PrismException; + + /** + * Get the initial state of the model, if there is just one, + * or the first of the initial states if there are more than one. + * The returned State object should be fresh, i.e. can be kept/modified. + */ + public State getInitialState() throws PrismException; + + /** + * Explore a given state of the model. After a call to this method, + * the class should be able to respond to the various methods that are + * available to query the outgoing transitions from the current state. + * @param exploreState State to explore (generate transition information for) + */ + public void exploreState(State exploreState) throws PrismException; + + /** + * Get the state that is currently being explored, i.e. the last one for which + * {@link #exploreState(State)} was called. Can return null if there is no such state. + */ + public State getExploreState(); + + /** + * Get the number of nondeterministic choices in the current state. + */ + public int getNumChoices() throws PrismException; + + /** + * Get the total number of transitions in the current state. + */ + public int getNumTransitions() throws PrismException; + + /** + * Get the number of transitions in the {@code i}th nondeterministic choice. + * @param i Index of the nondeterministic choice + */ + public int getNumTransitions(int i) throws PrismException; + + /** + * Get the action label of a transition, specified by its index. + * The label can be any Object, but will often be treated as a string, so it should at least + * have a meaningful toString() method implemented. Absence of an action label is denoted by null. + * Note: For most types of models, the action label will be the same for all transitions within + * the same nondeterministic choice, so it is better to query the action by choice, not transition. + */ + public Object getTransitionAction(int i) throws PrismException; + + /** + * Get the action label of a transition within a choice, specified by its index/offset. + * The label can be any Object, but will often be treated as a string, so it should at least + * have a meaningful toString() method implemented. Absence of an action label is denoted by null. + * Note: For most types of models, the action label will be the same for all transitions within + * the same nondeterministic choice (i.e. for each different value of {@code offset}), + * but for Markov chains this may not necessarily be the case. + */ + public Object getTransitionAction(int i, int offset) throws PrismException; + + /** + * Get the action label of a choice, specified by its index. + * The label can be any Object, but will often be treated as a string, so it should at least + * have a meaningful toString() method implemented. Absence of an action label is denoted by null. + * Note: If the model has different actions for different transitions within a choice + * (as can be the case for Markov chains), this method returns the action for the first transition. + * So, this method is essentially equivalent to {@code getTransitionAction(i, 0)}. + */ + public Object getChoiceAction(int i) throws PrismException; + + /** + * Get the probability/rate of a transition within a choice, specified by its index/offset. + * @param i Index of the nondeterministic choice + * @param offset Index of the transition within the choice + */ + public double getTransitionProbability(int i, int offset) throws PrismException; + + /** + * Get the target (as a new State object) of a transition within a choice, specified by its index/offset. + * @param i Index of the nondeterministic choice + * @param offset Index of the transition within the choice + */ + public State computeTransitionTarget(int i, int offset) throws PrismException; + + /** + * Is label {@code label} true in the state currently being explored? + * @param label The name of the label to check + */ + public boolean isLabelTrue(String label) throws PrismException; + + /** + * Is the {@code i}th label of the model true in the state currently being explored? + * @param i The index of the label to check + */ + public boolean isLabelTrue(int i) throws PrismException; + + /** + * Get the state reward of the {@code r}th reward structure for state {@code state}. + * @param r The index of the reward structure to use + * @param state The state in which to evaluate the rewards + */ + public double getStateReward(int r, State state) throws PrismException; + + /** + * Get the state-action reward of the {@code r}th reward structure for state {@code state} + * and action {@code action{. + * @param r The index of the reward structure to use + * @param state The state in which to evaluate the rewards + * @param action The outgoing action label + */ + public double getStateActionReward(int r, State state, Object action) throws PrismException; + + // Extra methods for symbolic interface (bit of a hack for now: + // we assume some methods do not need to be implemented, e.g. getTransitionProbability, + // and and some new ones to replace them, e.g. getTransitionProbabilityFunction + + public void setSymbolic(ModelBuilder modelBuilder, FunctionFactory functionFactory); + + public Expression getUnknownConstantDefinition(String name) throws PrismException; + + public Function getTransitionProbabilityFunction(int i, int offset) throws PrismException; +} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 95a5bd70..ea4427ed 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -65,6 +65,7 @@ import pta.DigitalClocks; import pta.PTAModelChecker; import simulator.GenerateSimulationPath; import simulator.ModulesFileModelGenerator; +import simulator.ModulesFileModelGeneratorSymbolic; import simulator.SimulatorEngine; import simulator.method.SimulationMethod; import sparse.PrismSparse; @@ -3092,7 +3093,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener String[] paramUpperBounds = new String[] { "1" }; // And execute parameteric model checking param.ModelBuilder builder = new ModelBuilder(this); - builder.setModulesFile(currentModulesFile); + builder.setModelGenerator(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this)); builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds); builder.build(); explicit.Model modelExpl = builder.getModel(); @@ -3151,7 +3152,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener mainLog.println("Property constants: " + definedPFConstants); param.ModelBuilder builder = new ModelBuilder(this); - builder.setModulesFile(currentModulesFile); + builder.setModelGenerator(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this)); builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds); builder.build(); explicit.Model modelExpl = builder.getModel(); diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java new file mode 100644 index 00000000..dd620b0d --- /dev/null +++ b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java @@ -0,0 +1,465 @@ +package simulator; + +import java.util.ArrayList; +import java.util.List; + +import param.Function; +import param.FunctionFactory; +import param.ModelBuilder; +import param.SymbolicEngine; +import parser.State; +import parser.Values; +import parser.VarList; +import parser.ast.ConstantList; +import parser.ast.Expression; +import parser.ast.LabelList; +import parser.ast.ModulesFile; +import parser.ast.RewardStruct; +import parser.type.Type; +import prism.DefaultModelGenerator; +import prism.ModelGeneratorSymbolic; +import prism.ModelType; +import prism.PrismComponent; +import prism.PrismException; +import prism.PrismLangException; + +public class ModulesFileModelGeneratorSymbolic extends DefaultModelGenerator implements ModelGeneratorSymbolic +{ + // Parent PrismComponent (logs, settings etc.) + protected PrismComponent parent; + + // PRISM model info + /** The original modules file (might have unresolved constants) */ + private ModulesFile originalModulesFile; + /** The modules file used for generating (has no unresolved constants after {@code initialise}) */ + private ModulesFile modulesFile; + private ModelType modelType; + private Values mfConstants; + private VarList varList; + private LabelList labelList; + private List labelNames; + + // Model exploration info + + // State currently being explored + private State exploreState; + // Updater object for model + //protected Updater updater; + protected SymbolicEngine engine; + // List of currently available transitions + protected param.TransitionList transitionList; + // Has the transition list been built? + protected boolean transitionListBuilt; + + // Symbolic stuff + boolean symbolic = false; + protected ModelBuilder modelBuilder; + protected FunctionFactory functionFactory; + + /** + * Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance. + * @param modulesFile The PRISM model + */ + public ModulesFileModelGeneratorSymbolic(ModulesFile modulesFile) throws PrismException + { + this(modulesFile, null); + } + + /** + * Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance. + * @param modulesFile The PRISM model + */ + public ModulesFileModelGeneratorSymbolic(ModulesFile modulesFile, PrismComponent parent) throws PrismException + { + this.parent = parent; + + // No support for PTAs yet + if (modulesFile.getModelType() == ModelType.PTA) { + throw new PrismException("Sorry - the simulator does not currently support PTAs"); + } + // No support for system...endsystem yet + if (modulesFile.getSystemDefn() != null) { + throw new PrismException("Sorry - the simulator does not currently handle the system...endsystem construct"); + } + + // Store basic model info + this.modulesFile = modulesFile; + this.originalModulesFile = modulesFile; + modelType = modulesFile.getModelType(); + + // If there are no constants to define, go ahead and initialise; + // Otherwise, setSomeUndefinedConstants needs to be called when the values are available + mfConstants = modulesFile.getConstantValues(); + if (mfConstants != null) { + initialise(); + } + } + + /** + * (Re-)Initialise the class ready for model exploration + * (can only be done once any constants needed have been provided) + */ + private void initialise() throws PrismLangException + { + // Evaluate constants on (a copy) of the modules file, insert constant values + // Note that we don't optimise expressions since this can create some round-off issues + modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants); + + // Get info + varList = modulesFile.createVarList(); + labelList = modulesFile.getLabelList(); + labelNames = labelList.getLabelNames(); + + // Create data structures for exploring model + //updater = new Updater(modulesFile, varList, parent); + //transitionList = new TransitionList(); + engine = new SymbolicEngine(modulesFile, modelBuilder, functionFactory); + transitionListBuilt = false; + } + + @Override + public void setSymbolic(ModelBuilder modelBuilder, FunctionFactory functionFactory) + { + symbolic = true; + this.modelBuilder = modelBuilder; + this.functionFactory = functionFactory; + //updater.setSymbolic(modelBuilder, functionFactory); + // TODO: created twice + engine = new SymbolicEngine(modulesFile, modelBuilder, functionFactory); + } + + // Methods for ModelInfo interface + + @Override + public ModelType getModelType() + { + return modelType; + } + + @Override + public void setSomeUndefinedConstants(Values someValues) throws PrismException + { + // We start again with a copy of the original modules file + // and set the constants in the copy. + // As {@code initialise()} can replace references to constants + // with the concrete values in modulesFile, this ensures that we + // start again at a place where references to constants have not + // yet been replaced. + modulesFile = (ModulesFile) originalModulesFile.deepCopy(); + modulesFile.setSomeUndefinedConstants(someValues); + mfConstants = modulesFile.getConstantValues(); + initialise(); + } + + @Override + public Values getConstantValues() + { + return mfConstants; + } + + @Override + public boolean containsUnboundedVariables() + { + return modulesFile.containsUnboundedVariables(); + } + + @Override + public int getNumVars() + { + return modulesFile.getNumVars(); + } + + @Override + public List getVarNames() + { + return modulesFile.getVarNames(); + } + + @Override + public List getVarTypes() + { + return modulesFile.getVarTypes(); + } + + @Override + public int getNumLabels() + { + return labelList.size(); + } + + @Override + public List getLabelNames() + { + return labelNames; + } + + @Override + public String getLabelName(int i) throws PrismException + { + return labelList.getLabelName(i); + } + + @Override + public int getLabelIndex(String label) + { + return labelList.getLabelIndex(label); + } + + @Override + public int getNumRewardStructs() + { + return modulesFile.getNumRewardStructs(); + } + + @Override + public List getRewardStructNames() + { + return modulesFile.getRewardStructNames(); + } + + @Override + public int getRewardStructIndex(String name) + { + return modulesFile.getRewardStructIndex(name); + } + + @Override + public RewardStruct getRewardStruct(int i) + { + return modulesFile.getRewardStruct(i); + } + + // Methods for ModelGenerator interface + + @Override + public boolean hasSingleInitialState() throws PrismException + { + return modulesFile.getInitialStates() == null; + } + + @Override + public State getInitialState() throws PrismException + { + if (modulesFile.getInitialStates() == null) { + return modulesFile.getDefaultInitialState(); + } else { + // Inefficient but probably won't be called + return getInitialStates().get(0); + } + } + + @Override + public List getInitialStates() throws PrismException + { + List initStates = new ArrayList(); + // Easy (normal) case: just one initial state + if (modulesFile.getInitialStates() == null) { + State state = modulesFile.getDefaultInitialState(); + initStates.add(state); + } + // Otherwise, there may be multiple initial states + // For now, we handle this is in a very inefficient way + else { + Expression init = modulesFile.getInitialStates(); + List allPossStates = varList.getAllStates(); + for (State possState : allPossStates) { + if (init.evaluateBoolean(modulesFile.getConstantValues(), possState)) { + initStates.add(possState); + } + } + } + return initStates; + } + + @Override + public void exploreState(State exploreState) throws PrismException + { + this.exploreState = exploreState; + transitionListBuilt = false; + } + + @Override + public State getExploreState() + { + return exploreState; + } + + @Override + public int getNumChoices() throws PrismException + { + return getTransitionList().getNumChoices(); + } + + @Override + public int getNumTransitions() throws PrismException + { + return getTransitionList().getNumTransitions(); + } + + @Override + public int getNumTransitions(int index) throws PrismException + { + return getTransitionList().getChoice(index).size(); + } + + @Override + public String getTransitionAction(int index) throws PrismException + { + int a = getTransitionList().getTransitionModuleOrActionIndex(index); + return a < 0 ? null : modulesFile.getSynch(a - 1); + } + + @Override + public String getTransitionAction(int index, int offset) throws PrismException + { + param.TransitionList transitions = getTransitionList(); + int a = transitions.getTransitionModuleOrActionIndex(transitions.getTotalIndexOfTransition(index, offset)); + return a < 0 ? null : modulesFile.getSynch(a - 1); + } + + @Override + public String getChoiceAction(int index) throws PrismException + { + param.TransitionList transitions = getTransitionList(); + int a = transitions.getChoiceModuleOrActionIndex(index); + return a < 0 ? null : modulesFile.getSynch(a - 1); + } + + @Override + public double getTransitionProbability(int index, int offset) throws PrismException + { + throw new UnsupportedOperationException(); + /*param.TransitionList transitions = getTransitionList(); + return transitions.getChoice(index).getProbability(offset);*/ + } + + //@Override + public double getTransitionProbability(int index) throws PrismException + { + throw new UnsupportedOperationException(); + /*param.TransitionList transitions = getTransitionList(); + return transitions.getTransitionProbability(index);*/ + } + + @Override + public Function getTransitionProbabilityFunction(int index, int offset) throws PrismException + { + param.TransitionList transitions = getTransitionList(); + return transitions.getChoice(index).getProbability(offset); + } + + @Override + public State computeTransitionTarget(int index, int offset) throws PrismException + { + return getTransitionList().getChoice(index).computeTarget(offset, exploreState); + } + + //@Override + public State computeTransitionTarget(int index) throws PrismException + { + return getTransitionList().computeTransitionTarget(index, exploreState); + } + + @Override + public boolean isLabelTrue(int i) throws PrismException + { + Expression expr = labelList.getLabel(i); + return expr.evaluateBoolean(exploreState); + } + + @Override + public double getStateReward(int r, State state) throws PrismException + { + RewardStruct rewStr = modulesFile.getRewardStruct(r); + int n = rewStr.getNumItems(); + double d = 0; + for (int i = 0; i < n; i++) { + if (!rewStr.getRewardStructItem(i).isTransitionReward()) { + Expression guard = rewStr.getStates(i); + if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { + double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); + d += rew; + } + } + } + return d; + } + + @Override + public double getStateActionReward(int r, State state, Object action) throws PrismException + { + RewardStruct rewStr = modulesFile.getRewardStruct(r); + int n = rewStr.getNumItems(); + double d = 0; + for (int i = 0; i < n; i++) { + if (rewStr.getRewardStructItem(i).isTransitionReward()) { + Expression guard = rewStr.getStates(i); + String cmdAction = rewStr.getSynch(i); + if (action == null ? (cmdAction.isEmpty()) : action.equals(cmdAction)) { + if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { + double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); + d += rew; + } + } + } + } + return d; + } + + //@Override + public void calculateStateRewards(State state, double[] store) throws PrismLangException + { + // TODO updater.calculateStateRewards(state, store); + } + + @Override + public VarList createVarList() + { + return varList; + } + + // Miscellaneous (unused?) methods + + //@Override + public void getRandomInitialState(RandomNumberGenerator rng, State initialState) throws PrismException + { + if (modulesFile.getInitialStates() == null) { + initialState.copy(modulesFile.getDefaultInitialState()); + } else { + throw new PrismException("Random choice of multiple initial states not yet supported"); + } + } + + // Local utility methods + + /** + * Returns the current list of available transitions, generating it first if this has not yet been done. + */ + private param.TransitionList getTransitionList() throws PrismException + { + // Compute the current transition list, if required + if (!transitionListBuilt) { + //updater.calculateTransitions(exploreState, transitionList); + transitionList = engine.calculateTransitions(exploreState, true); + transitionListBuilt = true; + } + return transitionList; + } + + // ModelGeneratorSymbolic + + @Override + public Expression getUnknownConstantDefinition(String name) throws PrismException + { + ConstantList constantList = modulesFile.getConstantList(); + int i = constantList.getConstantIndex(name); + if (i == -1) { + throw new PrismException("Unknown constant " + name); + } + return constantList.getConstant(i); + } +}