diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index a8ebddf2..1ac54a85 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -408,7 +408,7 @@ public final class FastAdaptiveUniformisation extends PrismComponent } /** model exploration component to generate new states */ - private ModelExplorer modelExplorer; + private ModelGenerator modelGen; /** probability allowed to drop birth process */ private double epsilon; /** probability threshold when to drop states in discrete-time process */ @@ -463,11 +463,11 @@ public final class FastAdaptiveUniformisation extends PrismComponent /** * Constructor. */ - public FastAdaptiveUniformisation(PrismComponent parent, ModelExplorer modelExplorer) throws PrismException + public FastAdaptiveUniformisation(PrismComponent parent, ModelGenerator modelGen) throws PrismException { super(parent); - this.modelExplorer = modelExplorer; + this.modelGen = modelGen; maxNumStates = 0; epsilon = settings.getDouble(PrismSettings.PRISM_FAU_EPSILON); @@ -562,8 +562,8 @@ public final class FastAdaptiveUniformisation extends PrismComponent for (Map.Entry statePair : states.entrySet()) { State state = statePair.getKey(); StateProp prop = statePair.getValue(); - modelExplorer.queryState(state); - specialLabels.setLabel(0, modelExplorer.getNumTransitions() == 0 ? Expression.True() : Expression.False()); + modelGen.exploreState(state); + specialLabels.setLabel(0, modelGen.getNumTransitions() == 0 ? Expression.True() : Expression.False()); specialLabels.setLabel(1, initStates.contains(state) ? Expression.True() : Expression.False()); Expression evSink = sink.deepCopy(); evSink = (Expression) evSink.expandLabels(specialLabels); @@ -666,6 +666,9 @@ public final class FastAdaptiveUniformisation extends PrismComponent */ public StateValues doTransient(double time, StateValues initDist) throws PrismException { + if (!modelGen.hasSingleInitialState()) + throw new PrismException("Fast adaptive uniformisation does not yet support models with multiple initial states"); + mainLog.println("\nComputing probabilities (fast adaptive uniformisation)..."); if (initDist == null) { @@ -675,7 +678,7 @@ public final class FastAdaptiveUniformisation extends PrismComponent initDist.valuesD = new double[1]; initDist.statesList = new ArrayList(); initDist.valuesD[0] = 1.0; - initDist.statesList.add(modelExplorer.getDefaultInitialState()); + initDist.statesList.add(modelGen.getInitialState()); } /* prepare fast adaptive uniformisation */ @@ -773,8 +776,8 @@ public final class FastAdaptiveUniformisation extends PrismComponent for (Map.Entry statePair : states.entrySet()) { State state = statePair.getKey(); StateProp prop = statePair.getValue(); - modelExplorer.queryState(state); - specialLabels.setLabel(0, modelExplorer.getNumTransitions() == 0 ? Expression.True() : Expression.False()); + modelGen.exploreState(state); + specialLabels.setLabel(0, modelGen.getNumTransitions() == 0 ? Expression.True() : Expression.False()); specialLabels.setLabel(1, initStates.contains(state) ? Expression.True() : Expression.False()); Expression evTarget = target.deepCopy(); evTarget = (Expression) evTarget.expandLabels(specialLabels); @@ -1079,7 +1082,7 @@ public final class FastAdaptiveUniformisation extends PrismComponent private void prepareInitialDistribution() throws PrismException { initStates = new HashSet(); - State initState = modelExplorer.getDefaultInitialState(); + State initState = modelGen.getInitialState(); initStates.add(initState); addToModel(initState); computeStateRatesAndRewards(initState); @@ -1121,8 +1124,8 @@ public final class FastAdaptiveUniformisation extends PrismComponent for (Map.Entry statePair : states.entrySet()) { State state = statePair.getKey(); StateProp prop = statePair.getValue(); - modelExplorer.queryState(state); - specialLabels.setLabel(0, modelExplorer.getNumTransitions() == 0 ? Expression.True() : Expression.False()); + modelGen.exploreState(state); + specialLabels.setLabel(0, modelGen.getNumTransitions() == 0 ? Expression.True() : Expression.False()); specialLabels.setLabel(1, initStates.contains(state) ? Expression.True() : Expression.False()); Expression evSink = sink.deepCopy(); evSink = (Expression) evSink.expandLabels(specialLabels); @@ -1161,8 +1164,8 @@ public final class FastAdaptiveUniformisation extends PrismComponent { double[] succRates; StateProp[] succStates; - modelExplorer.queryState(state); - specialLabels.setLabel(0, modelExplorer.getNumTransitions() == 0 ? Expression.True() : Expression.False()); + modelGen.exploreState(state); + specialLabels.setLabel(0, modelGen.getNumTransitions() == 0 ? Expression.True() : Expression.False()); specialLabels.setLabel(1, initStates.contains(state) ? Expression.True() : Expression.False()); Expression evSink = sink.deepCopy(); evSink = (Expression) evSink.expandLabels(specialLabels); @@ -1172,21 +1175,24 @@ public final class FastAdaptiveUniformisation extends PrismComponent succRates[0] = 1.0; succStates[0] = states.get(state); } else { - int nt = modelExplorer.getNumTransitions(); - succRates = new double[nt]; - succStates = new StateProp[nt]; - for (int i = 0; i < nt; i++) { - State succState = modelExplorer.computeTransitionTarget(i); - StateProp succProp = states.get(succState); - if (null == succProp) { - addToModel(succState); - modelExplorer.queryState(state); - succProp = states.get(succState); + int nc = modelGen.getNumChoices(); + succRates = new double[nc]; + succStates = new StateProp[nc]; + for (int i = 0; i < nc; i++) { + int nt = modelGen.getNumTransitions(i); + for (int j = 0; j < nt; j++) { + State succState = modelGen.computeTransitionTarget(i, j); + StateProp succProp = states.get(succState); + if (null == succProp) { + addToModel(succState); + modelGen.exploreState(state); + succProp = states.get(succState); + } + succRates[i] = modelGen.getTransitionProbability(i, j); + succStates[i] = succProp; } - succRates[i] = modelExplorer.getTransitionProbability(i); - succStates[i] = succProp; } - if (nt == 0) { + if (nc == 0) { succRates = new double[1]; succStates = new StateProp[1]; succRates[0] = 1.0; @@ -1248,10 +1254,10 @@ public final class FastAdaptiveUniformisation extends PrismComponent if (!isRewardAnalysis()) { return 0.0; } - int numTransitions = 0; + int numChoices = 0; if (AnalysisType.REW_CUMUL == analysisType) { - modelExplorer.queryState(state); - numTransitions = modelExplorer.getNumTransitions(); + modelGen.exploreState(state); + numChoices = modelGen.getNumChoices(); } double sumReward = 0.0; int numStateItems = rewStruct.getNumItems(); @@ -1262,13 +1268,16 @@ public final class FastAdaptiveUniformisation extends PrismComponent String action = rewStruct.getSynch(i); if (action != null) { if (AnalysisType.REW_CUMUL == analysisType) { - for (int j = 0; j < numTransitions; j++) { - String tAction = modelExplorer.getTransitionAction(j); - if (tAction == null) { - tAction = ""; - } - if (tAction.equals(action)) { - sumReward += reward * modelExplorer.getTransitionProbability(j); + for (int j = 0; j < numChoices; j++) { + int numTransitions = modelGen.getNumTransitions(j); + for (int k = 0; k < numTransitions; k++) { + String tAction = modelGen.getTransitionAction(j, k).toString(); + if (tAction == null) { + tAction = ""; + } + if (tAction.equals(action)) { + sumReward += reward * modelGen.getTransitionProbability(j, k); + } } } } diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java index cc63656c..ffd3b5e1 100644 --- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java +++ b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java @@ -40,8 +40,7 @@ import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; import prism.Result; -import simulator.PrismModelExplorer; -import simulator.SimulatorEngine; +import simulator.ModulesFileModelGenerator; /** * CTMC model checker based on fast adaptive uniformisation. @@ -52,8 +51,6 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent private ModulesFile modulesFile; // Properties file private PropertiesFile propertiesFile; - // Simulator engine - private SimulatorEngine engine; // Constants from model private Values constantValues; // Labels from the model @@ -64,12 +61,11 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent /** * Constructor. */ - public FastAdaptiveUniformisationModelChecker(PrismComponent parent, ModulesFile modulesFile, PropertiesFile propertiesFile, SimulatorEngine engine) throws PrismException + public FastAdaptiveUniformisationModelChecker(PrismComponent parent, ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismException { super(parent); this.modulesFile = modulesFile; this.propertiesFile = propertiesFile; - this.engine = engine; // Get combined constant values from model/properties constantValues = new Values(); @@ -160,8 +156,8 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent } mainLog.println("Starting transient probability computation using fast adaptive uniformisation..."); - PrismModelExplorer modelExplorer = new PrismModelExplorer(engine, modulesFile); - FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); + ModulesFileModelGenerator prismModelGen = new ModulesFileModelGenerator(modulesFile, this); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, prismModelGen); fau.setConstantValues(constantValues); Expression op1 = exprTemp.getOperand1(); @@ -228,8 +224,8 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent private Result checkExpressionReward(ExpressionReward expr) throws PrismException { mainLog.println("Starting transient probability computation using fast adaptive uniformisation..."); - PrismModelExplorer modelExplorer = new PrismModelExplorer(engine, modulesFile); - FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); + ModulesFileModelGenerator prismModelGen = new ModulesFileModelGenerator(modulesFile, this); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, prismModelGen); ExpressionTemporal temporal = (ExpressionTemporal) expr.getExpression(); switch (temporal.getOperator()) { case ExpressionTemporal.R_I: diff --git a/prism/src/explicit/ModelExplorer.java b/prism/src/explicit/ModelExplorer.java deleted file mode 100644 index 28ae099e..00000000 --- a/prism/src/explicit/ModelExplorer.java +++ /dev/null @@ -1,99 +0,0 @@ -//============================================================================== -// -// Authors: -// * Dave Parker (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 parser.State; -import prism.PrismException; - -public interface ModelExplorer -{ - public State getDefaultInitialState() throws PrismException; - - public void queryState(State state) throws PrismException; - - public void queryState(State state, double time) throws PrismException; - - /** - * Returns the current number of available choices. - * @throws PrismException - */ - public int getNumChoices() throws PrismException; - - /** - * Returns the current (total) number of available transitions. - * @throws PrismException - */ - public int getNumTransitions() throws PrismException; - - /** - * Returns the current number of available transitions in choice i. - * @throws PrismException - */ - public int getNumTransitions(int i) throws PrismException; - - /** - * Get the probability/rate of a transition within a choice, specified by its index/offset. - */ - public double getTransitionProbability(int i, int offset) throws PrismException; - - /** - * Get the action label of a transition as a string, specified by its index/offset. - * (null for asynchronous/independent transitions) - * (see also {@link #getTransitionModuleOrAction(int, int)} and {@link #getTransitionModuleOrActionIndex(int, int)}) - * TODO: change return type to Object? - * @throws PrismException - */ - public String getTransitionAction(int i, int offset) throws PrismException; - - /** - * Get the action label of a transition as a string, specified by its index. - * (null for asynchronous/independent transitions) - * (see also {@link #getTransitionModuleOrAction(int)} and {@link #getTransitionModuleOrActionIndex(int)}) - * TODO: change return type to Object? - * @throws PrismException - */ - public String getTransitionAction(int index) throws PrismException; - - /** - * Get the probability/rate of a transition, specified by its index. - */ - public double getTransitionProbability(int i) throws PrismException; - - /** - * Get the sum of probabilities/rates for transitions. - */ -// public double getTransitionProbabilitySum() throws PrismException; - - /** - * Get the target (as a new State object) of a transition within a choice, specified by its index/offset. - */ - public State computeTransitionTarget(int i, int offset) throws PrismException; - - /** - * Get the target of a transition (as a new State object), specified by its index. - */ - public State computeTransitionTarget(int i) throws PrismException; -} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 772cd469..b842df05 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -60,7 +60,6 @@ import pta.DigitalClocks; import pta.PTAModelChecker; import simulator.GenerateSimulationPath; import simulator.ModulesFileModelGenerator; -import simulator.PrismModelExplorer; import simulator.SimulatorEngine; import simulator.method.SimulationMethod; import sparse.PrismSparse; @@ -2762,7 +2761,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // For fast adaptive uniformisation if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) { FastAdaptiveUniformisationModelChecker fauMC; - fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile, getSimulator()); + fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile); return fauMC.check(prop.getExpression()); } // Auto-switch engine if required @@ -3305,8 +3304,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener // FAU if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) { - PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile); - FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); + ModulesFileModelGenerator prismModelGen = new ModulesFileModelGenerator(currentModulesFile, this); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, prismModelGen); fau.setConstantValues(currentModulesFile.getConstantValues()); probsExpl = fau.doTransient(time, fileIn, currentModel); } @@ -3412,8 +3411,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener // FAU if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) { - PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile); - FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); + ModulesFileModelGenerator prismModelGen = new ModulesFileModelGenerator(currentModulesFile, this); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, prismModelGen); fau.setConstantValues(currentModulesFile.getConstantValues()); if (i == 0) { probsExpl = fau.doTransient(timeDouble, fileIn, currentModel); diff --git a/prism/src/simulator/PrismModelExplorer.java b/prism/src/simulator/PrismModelExplorer.java deleted file mode 100644 index 4e1ba1c3..00000000 --- a/prism/src/simulator/PrismModelExplorer.java +++ /dev/null @@ -1,125 +0,0 @@ -//============================================================================== -// -// Authors: -// * Dave Parker (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 simulator; - -import parser.State; -import parser.ast.ModulesFile; -import prism.PrismException; -import explicit.ModelExplorer; - -public class PrismModelExplorer implements ModelExplorer -{ - private SimulatorEngine simEngine; - private ModulesFile modulesFile; - - public PrismModelExplorer(SimulatorEngine simEngine, ModulesFile modulesFile) throws PrismException - { - this.simEngine = simEngine; - this.modulesFile = modulesFile; - simEngine.createNewOnTheFlyPath(modulesFile); - - } - - @Override - public State getDefaultInitialState() throws PrismException - { - return modulesFile.getDefaultInitialState(); - } - - @Override - public void queryState(State state) throws PrismException - { - simEngine.initialisePath(state); - } - - @Override - public void queryState(State state, double time) throws PrismException - { - queryState(state); - } - - @Override - public int getNumChoices() throws PrismException - { - return simEngine.getNumChoices(); - } - - @Override - public int getNumTransitions() throws PrismException - { - return simEngine.getNumTransitions(); - } - - @Override - public int getNumTransitions(int i) throws PrismException - { - return simEngine.getNumTransitions(i); - } - - @Override - public String getTransitionAction(int i, int offset) throws PrismException - { - return simEngine.getTransitionAction(i, offset); - } - - @Override - public String getTransitionAction(int i) throws PrismException - { - return simEngine.getTransitionAction(i); - } - - @Override - public double getTransitionProbability(int i, int offset) throws PrismException - { - return simEngine.getTransitionProbability(i, offset); - } - - @Override - public double getTransitionProbability(int i) throws PrismException - { - return simEngine.getTransitionProbability(i); - } - - /* - @Override - public double getTransitionProbabilitySum() throws PrismException - { - return simEngine.getTransitionProbabilitySum(); - } - */ - - @Override - public State computeTransitionTarget(int i, int offset) throws PrismException - { - return simEngine.computeTransitionTarget(i, offset); - } - - @Override - public State computeTransitionTarget(int i) throws PrismException - { - return simEngine.computeTransitionTarget(i); - } -}