From 98126c125ca4adb33b33f93d485658fb994692c9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Nov 2010 22:49:23 +0000 Subject: [PATCH] Code tidy. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2255 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/SimulatorEngine.java | 91 +++++++++--------------- 1 file changed, 32 insertions(+), 59 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 4b12c3f1..093c1a25 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -116,7 +116,7 @@ public class SimulatorEngine // Temporary storage for manipulating states/rewards protected double tmpStateRewards[]; protected double tmpTransitionRewards[]; - + // Updater object for model protected Updater updater; // Random number generator @@ -837,7 +837,7 @@ public class SimulatorEngine { return transitionList.getTransitionUpdateString(index, path.getCurrentState()); } - + /** * Get a string describing the updates making up a transition, specified by its index. * This is in full, i.e. of the form x'=x+1, rather than x'=1. @@ -849,7 +849,7 @@ public class SimulatorEngine { return transitionList.getTransitionUpdateStringFull(index); } - + /** * Get the target (as a new State object) of a transition within a choice, specified by its index/offset. */ @@ -1123,29 +1123,15 @@ public class SimulatorEngine } /** - * Perform approximate model checking for a single property. - * Note: All constants in the model must have already been defined. - * @param modulesFile Model for simulation - * - *

- * The returned result is: - *

- * - * @param propertiesFile - * The PropertiesFile containing the property of interest, constants defined. - * @param expr - * The property of interest - * @param initialState - * The initial state for the sampling. - * @param noIterations - * The number of iterations for the sampling algorithm - * @param maxPathLength - * the maximum path length for the sampling algorithm. - * @throws PrismException - * if anything goes wrong. - * @return the result. + * Perform approximate model checking of a property on a model, using the simulator. + * Sampling starts from the initial state provided or, if null, a random initial state each time. + * Note: All constants in the model/property files must have already been defined. + * @param modulesFile Model for simulation, constants defined + * @param propertiesFile Properties file containing property to check, constants defined + * @param expr The property to check + * @param initialState Initial state (if null, is selected randomly) + * @param numIters The number of iterations (i.e. number of samples to generate) + * @param maxPathLength The maximum path length for sampling */ public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int numIters, int maxPathLength) throws PrismException @@ -1153,6 +1139,7 @@ public class SimulatorEngine ArrayList exprs; Object res[]; + // Just do this via the 'multiple properties' method exprs = new ArrayList(); exprs.add(expr); res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, numIters, maxPathLength); @@ -1222,37 +1209,23 @@ public class SimulatorEngine } /** - * Deals with all of the logistics of performing an experiment and storing the results in an appropriate - * ResultsCollection object. - * - * @param exp - * the experiment in which to store the results. - * @param modulesFile - * The ModulesFile, constants already defined. - * @param propertiesFile - * The PropertiesFile containing the property of interest, constants defined. - * @param undefinedConstants - * defining what should be done for the experiment - * @param resultsCollection - * where the results should be stored - * @param propertyToCheck - * the property to check for the experiment - * @param initialState - * The initial state for the sampling. - * @param maxPathLength - * the maximum path length for the sampling algorithm. - * @param noIterations - * The number of iterations for the sampling algorithm - * @throws PrismException - * if something goes wrong with the results reporting - * @throws InterruptedException - * if the thread is interrupted - * @throws PrismException - * if something goes wrong with the sampling algorithm + * Perform an approximate model checking experiment on a model, using the simulator. + * Sampling starts from the initial state provided or, if null, a random initial state each time. + * Note: All constants in the model/property files must have already been defined. + * @param modulesFile Model for simulation, constants defined + * @param propertiesFile Properties file containing property to check, constants defined + * @param undefinedConstants Details of constant ranges defining the experiment + * @param resultsCollection Where to store the results + * @param expr The property to check + * @param initialState Initial state (if null, is selected randomly) + * @param numIters The number of iterations (i.e. number of samples to generate) + * @param maxPathLength The maximum path length for sampling + * @throws PrismException if something goes wrong with the sampling algorithm + * @throws InterruptedException if the thread is interrupted */ public void modelCheckExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, - ResultsCollection resultsCollection, Expression propertyToCheck, State initialState, int maxPathLength, int noIterations) throws PrismException, - InterruptedException, PrismException + ResultsCollection resultsCollection, Expression expr, State initialState, int maxPathLength, int numIters) throws PrismException, + InterruptedException { int n; Values definedPFConstants = new Values(); @@ -1271,8 +1244,8 @@ public class SimulatorEngine pfcs[i] = definedPFConstants; propertiesFile.setUndefinedConstants(definedPFConstants); try { - checkPropertyForSimulation(propertyToCheck); - indices[i] = addProperty(propertyToCheck, propertiesFile); + checkPropertyForSimulation(expr); + indices[i] = addProperty(expr, propertiesFile); if (indices[i] >= 0) validPropsCount++; } catch (PrismException e) { @@ -1284,7 +1257,7 @@ public class SimulatorEngine // as long as there are at least some valid props, do sampling if (validPropsCount > 0) { - doSampling(initialState, noIterations, maxPathLength); + doSampling(initialState, numIters, maxPathLength); } // process the results @@ -1345,7 +1318,7 @@ public class SimulatorEngine // Start the new path for this iteration (sample) initialisePath(initialState); - + // Generate a path, up to at most maxPathLength steps for (i = 0; i < maxPathLength; i++) { // See if all samplers have established a value; if so, stop.