diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index bd9a1e15..5f7b4d43 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1451,7 +1451,7 @@ public class Prism implements PrismSettingsListener public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, Expression propertyToCheck, Values initialState, int noIterations, int pathLength) throws PrismException, InterruptedException { - getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, noIterations); + getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, new State(initialState), pathLength, noIterations); } // generate a random path through the model using the simulator diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index 2fcda764..cdd65778 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/prism/src/simulator/GenerateSimulationPath.java @@ -29,9 +29,9 @@ package simulator; import java.io.File; import java.util.ArrayList; -import parser.Values; -import parser.ast.ModulesFile; import prism.*; +import parser.*; +import parser.ast.*; public class GenerateSimulationPath { @@ -220,7 +220,7 @@ public class GenerateSimulationPath // generate path engine.createNewPath(modulesFile); for (j = 0; j < simPathRepeat; j++) { - engine.initialisePath(initialState); + engine.initialisePath(new State(initialState)); i = 0; t = 0.0; done = false; diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1beda04c..8ca9d724 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -268,16 +268,6 @@ public class SimulatorEngine onTheFly = true; } - /** - * Initialise (or re-initialise) the simulation path, starting with a specific (or random) initial state. - * @param initialState Initial state (if null, is selected randomly) - */ - public void initialisePath(Values initialState) throws PrismException - { - // TODO: need this method? - initialisePath(new State(initialState)); - } - /** * Initialise (or re-initialise) the simulation path, starting with a specific (or random) initial state. * @param initialState Initial state (if null, is selected randomly) @@ -290,8 +280,6 @@ public class SimulatorEngine } // Or pick a random one else { - // TODO - //currentState... throw new PrismException("Random initial start state not yet supported"); } updater.calculateStateRewards(currentState, currentStateRewards); @@ -1377,7 +1365,7 @@ public class SimulatorEngine * if something goes wrong with the sampling algorithm */ public void modelCheckExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, - ResultsCollection resultsCollection, Expression propertyToCheck, Values initialState, int maxPathLength, int noIterations) throws PrismException, + ResultsCollection resultsCollection, Expression propertyToCheck, State initialState, int maxPathLength, int noIterations) throws PrismException, InterruptedException, PrismException { int n; diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index a45bfee7..001894e3 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -360,7 +360,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect engine.createNewPath(parsedModel); pathActive = true; repopulateFormulae(pf); - engine.initialisePath(initialState); + engine.initialisePath(new State(initialState)); totalTimeLabel.setText(formatDouble(engine.getTotalTimeForPath())); pathLengthLabel.setText("" + engine.getPathSize());