diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index d9043402..9024c95c 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -104,14 +104,15 @@ public class PathFull extends Path implements PathFullInfo } @Override - public void addStep(int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList) + public void addStep(int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, + TransitionList transitionList) { addStep(1.0, choice, moduleOrActionIndex, probability, transitionRewards, newState, newStateRewards, transitionList); } @Override - public void addStep(double time, int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, - TransitionList transitionList) + public void addStep(double time, int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, + double[] newStateRewards, TransitionList transitionList) { Step stepOld, stepNew; // Add info to last existing step @@ -257,7 +258,7 @@ public class PathFull extends Path implements PathFullInfo { return steps.get(steps.size() - 2).probability; } - + @Override public double getTotalTime() { @@ -431,7 +432,7 @@ public class PathFull extends Path implements PathFullInfo { return steps.get(steps.size() - 2).probability; } - + /** * Get a transition reward associated with a given step. * @param step Step index (0 = initial state/step of path) @@ -497,7 +498,8 @@ public class PathFull extends Path implements PathFullInfo displayer.start(getState(0), getStateRewards(0)); int n = size(); for (int i = 1; i <= n; i++) { - displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getProbability(i - 1), getTransitionRewards(i), i, getState(i), getStateRewards(i)); + displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getProbability(i - 1), getTransitionRewards(i), i, getState(i), + getStateRewards(i)); } displayer.end(); } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 910d5965..1c1f8403 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -26,16 +26,34 @@ package simulator; -import java.util.*; -import java.io.*; - -import simulator.method.*; -import simulator.sampler.*; +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +import parser.State; +import parser.Values; +import parser.VarList; +import parser.ast.Expression; +import parser.ast.ExpressionFilter; +import parser.ast.ExpressionProb; +import parser.ast.ExpressionReward; +import parser.ast.ExpressionTemporal; +import parser.ast.LabelList; +import parser.ast.ModulesFile; +import parser.ast.PropertiesFile; +import parser.type.Type; +import prism.ModelType; +import prism.Prism; +import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLangException; +import prism.PrismLog; +import prism.PrismUtils; +import prism.ResultsCollection; +import prism.UndefinedConstants; +import simulator.method.SimulationMethod; +import simulator.sampler.Sampler; import userinterface.graph.Graph; -import parser.*; -import parser.ast.*; -import parser.type.*; -import prism.*; /** * A discrete event simulation engine for PRISM models. @@ -184,7 +202,7 @@ public class SimulatorEngine throw new PrismException("Sorry - the simulator does not currently handle the system...endsystem construct"); } } - + /** * Create a new path for a model. * Note: All constants in the model must have already been defined. @@ -499,7 +517,7 @@ public class SimulatorEngine state = nextState; } } - + // ------------------------------------------------------------------------------ // Methods for adding/querying labels and properties // ------------------------------------------------------------------------------ @@ -854,7 +872,7 @@ public class SimulatorEngine } return transitionList; } - + /** * Returns the current number of available choices. */ @@ -1032,7 +1050,7 @@ public class SimulatorEngine { return (Path) path; } - + /** * Get the size of the current path (number of steps; or number of states - 1). */ @@ -1089,7 +1107,7 @@ public class SimulatorEngine { return (PathFull) path; } - + /** * Get the value of a variable at a given step of the path. * (Not applicable for on-the-fly paths) @@ -1255,7 +1273,7 @@ public class SimulatorEngine } ((PathFull) path).exportToLog(log, timeCumul, colSep, vars); } - + /** * Plot the current path on a Graph. * @param graphModel Graph on which to plot path @@ -1276,7 +1294,7 @@ public class SimulatorEngine { return isPropertyOKForSimulationString(expr) == null; } - + /** * Check whether a property is suitable for approximate model checking using the simulator. * If not, an explanatory error message is thrown as an exception. @@ -1287,7 +1305,7 @@ public class SimulatorEngine if (errMsg != null) throw new PrismException(errMsg); } - + /** * Check whether a property is suitable for approximate model checking using the simulator. * If yes, return null; if not, return an explanatory error message. @@ -1312,7 +1330,7 @@ public class SimulatorEngine } // Simulator cannot handle cumulative reward properties without a time bound if (expr instanceof ExpressionReward) { - Expression exprTemp = ((ExpressionReward) expr).getExpression(); + Expression exprTemp = ((ExpressionReward) expr).getExpression(); if (exprTemp instanceof ExpressionTemporal) { if (((ExpressionTemporal) exprTemp).getOperator() == ExpressionTemporal.R_C) { if (((ExpressionTemporal) exprTemp).getUpperBound() == null) {