diff --git a/prism/src/simulator/Makefile b/prism/src/simulator/Makefile index bbb00349..dd2e030c 100644 --- a/prism/src/simulator/Makefile +++ b/prism/src/simulator/Makefile @@ -12,7 +12,7 @@ THIS_DIR = simulator PRISM_DIR_REL = ../.. -JAVA_FILES = $(wildcard *.java networking/*.java) +JAVA_FILES = $(wildcard *.java sampler/*.java networking/*.java) CLASS_FILES = $(JAVA_FILES:%.java=$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class) default: all diff --git a/prism/src/simulator/Path.java b/prism/src/simulator/PathFull.java similarity index 81% rename from prism/src/simulator/Path.java rename to prism/src/simulator/PathFull.java index d25371f9..8b91dff7 100644 --- a/prism/src/simulator/Path.java +++ b/prism/src/simulator/PathFull.java @@ -36,8 +36,10 @@ import prism.PrismLog; /** * Stores and manipulates a path though a model. + * The full path is stored, i.e. all info at all steps. + * State objects and arrays are copied for storage. */ -public class Path +public class PathFull extends Path { class Step { @@ -74,57 +76,10 @@ public class Path protected double totalStateReward[]; protected double totalTransitionReward[]; - // ACCESSORS - - public int size() - { - return size; - } - - public State getState(int step) - { - return path.get(step).state; - } - - public double getStateReward(int step, int i) - { - return path.get(step).stateRewards[i]; - } - - public State getCurrentState() - { - return getState(size - 1); - } - - public double getTime(int i) - { - return path.get(i).time; - } - - public double getCumulativeTime(int i) - { - return path.get(i).timeCumul; - } - - public int getChoice(int i) - { - return path.get(i).choice; - } - - public String getAction(int i) - { - return path.get(i).action; - } - - public double getTransitionReward(int i, int j) - { - return path.get(i).transitionRewards[j]; - } - /** - * Constructor: creates a new (empty) Path object for a specific model. + * Constructor: creates a new (empty) PathFull object for a specific model. */ - public Path(SimulatorEngine engine, ModulesFile modulesFile) + public PathFull(SimulatorEngine engine, ModulesFile modulesFile) { // Store ptr to engine this.engine = engine; @@ -141,7 +96,7 @@ public class Path } /** - * Clear the path + * Clear the path. */ protected void clear() { @@ -155,9 +110,9 @@ public class Path } } - /** - * Initialise the path with an initial state and rewards. - */ + // MUTATORS (for Path) + + @Override public void initialise(State initialState, double[] initialStateRewards) { clear(); @@ -173,17 +128,20 @@ public class Path /** * Add a step to the path. + * The passed in State object and arrays (of rewards) will be copied to store in the path. */ + @Override public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards) { addStep(0, choice, action, transRewards, newState, newStateRewards); } /** - * Add a (timed) step to the path. + * Add a timed step to the path. + * The passed in State object and arrays (of rewards) will be copied to store in the path. */ - public void addStep(double time, int choice, String action, double[] transRewards, State newState, - double[] newStateRewards) + @Override + public void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards) { Step step; // Add info to last existing step @@ -204,17 +162,111 @@ public class Path // Add (copies of) new state and state rewards to new step step.state = new State(newState); step.stateRewards = newStateRewards.clone(); + // Update totals + totalTime += time; + } + + // ACCESSORS (for Path) + + @Override + public int size() + { + return size; + } + + @Override + public State getPreviousState() + { + return path.get(path.size() - 2).state; + } + + @Override + public State getCurrentState() + { + return path.get(path.size() - 1).state; + } + + @Override + public double getTimeSoFar() + { + return totalTime; + } + + @Override + public double getTimeInPreviousState() + { + return path.get(path.size() - 2).time; + } + + @Override + public double getRewardCumulatedSoFar(int index) + { + return totalReward[index]; + } + + @Override + public double getPreviousStateReward(int index) + { + return path.get(path.size() - 2).stateRewards[index]; + } + + @Override + public double getPreviousTransitionReward(int index) + { + return path.get(path.size() - 2).transitionRewards[index]; + } + + @Override + public double getCurrentStateReward(int index) + { + return path.get(path.size() - 1).stateRewards[index]; + } + + // ACCESSORS (additional) + + public State getState(int step) + { + return path.get(step).state; + } + + public double getStateReward(int step, int i) + { + return path.get(step).stateRewards[i]; + } + + public double getTime(int i) + { + return path.get(i).time; + } + + public double getCumulativeTime(int i) + { + return path.get(i).timeCumul; + } + + public int getChoice(int i) + { + return path.get(i).choice; + } + + public String getAction(int i) + { + return path.get(i).action; + } + + public double getTransitionReward(int i, int j) + { + return path.get(i).transitionRewards[j]; } /** - * Exports path to a file. + * Export path to a file. * @param log: PrismLog to which the path should be exported to. * @param timeCumul: Show time in cumulative form? * @param colSep: String used to separate columns in display * @param vars: Restrict printing to these variables (indices) and steps which change them (ignore if null) */ - public void exportToLog(PrismLog log, boolean timeCumul, String colSep, ArrayList vars) - throws PrismException + public void exportToLog(PrismLog log, boolean timeCumul, String colSep, ArrayList vars) throws PrismException { int i, j, n, nv; double d, t; @@ -304,9 +356,7 @@ public class Path log.close(); } - /** - * Generate string representation. - */ + @Override public String toString() { int i; diff --git a/prism/src/simulator/PathOnTheFly.java b/prism/src/simulator/PathOnTheFly.java new file mode 100644 index 00000000..a88d6ce1 --- /dev/null +++ b/prism/src/simulator/PathOnTheFly.java @@ -0,0 +1,198 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.*; +import parser.ast.*; + +/** + * Stores and manipulates a path though a model. + * Minimal info is stored - just enough to allow checking of properties. + * State objects and arrays are just stored as references to existing objects, but never modified. + * TODO: decide whether to copy states (we already copy rewards actually) + */ +public class PathOnTheFly extends Path +{ + // Parent simulator engine + protected SimulatorEngine engine; + // Model to which the path corresponds + protected ModulesFile modulesFile; + // Does model use continuous time? + protected boolean continuousTime; + // Model info/stats + protected int numRewardStructs; + + // Path info required to implement Path abstract class: + protected int size; + protected State previousState; + protected State currentState; + protected double totalTime; + double timeInPreviousState; + protected double totalRewards[]; + protected double previousStateRewards[]; + protected double previousTransitionRewards[]; + protected double currentStateRewards[]; + + /** + * Constructor: creates a new (empty) PathOnTheFly object for a specific model. + */ + public PathOnTheFly(SimulatorEngine engine, ModulesFile modulesFile) + { + // Store ptr to engine + this.engine = engine; + // Store model and info + this.modulesFile = modulesFile; + continuousTime = modulesFile.getModelType().continuousTime(); + numRewardStructs = modulesFile.getNumRewardStructs(); + // Create arrays to store totals + totalRewards = new double[numRewardStructs]; + previousStateRewards = new double[numRewardStructs]; + previousTransitionRewards = new double[numRewardStructs]; + currentStateRewards = new double[numRewardStructs]; + // Initialise path info + clear(); + } + + /** + * Clear the path. + */ + protected void clear() + { + // Initialise all path info + size = 0; + previousState = null; + currentState = null; + totalTime = 0.0; + timeInPreviousState = 0.0; + for (int i = 0; i < numRewardStructs; i++) { + totalRewards[i] = 0.0; + previousStateRewards[i] = 0.0; + previousTransitionRewards[i] = 0.0; + currentStateRewards[i] = 0.0; + } + } + + // MUTATORS (for Path) + + @Override + public void initialise(State initialState, double[] initialStateRewards) + { + clear(); + currentState = initialState; + currentStateRewards = initialStateRewards; + } + + /** + * Add a step to the path. + * The passed in State object and arrays (of rewards) will be stored as references, but never modified. + */ + @Override + public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards) + { + addStep(0, choice, action, transRewards, newState, newStateRewards); + } + + /** + * Add a timed step to the path. + * The passed in State object and arrays (of rewards) will be stored as references, but never modified. + */ + @Override + public void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards) + { + size = 0; + previousState = currentState; + currentState = newState; + totalTime += time; + timeInPreviousState = time; + for (int i = 0; i < numRewardStructs; i++) { + if (continuousTime) { + totalRewards[i] += currentStateRewards[i] * time + transRewards[i]; + } else { + totalRewards[i] += currentStateRewards[i] + transRewards[i]; + } + previousStateRewards[i] = currentStateRewards[i]; + previousTransitionRewards[i] = transRewards[i]; + currentStateRewards[i] = newStateRewards[i]; + } + } + + // ACCESSORS (for Path) + + @Override + public int size() + { + return size; + } + + @Override + public State getPreviousState() + { + return previousState; + } + + @Override + public State getCurrentState() + { + return currentState; + } + + @Override + public double getTimeSoFar() + { + return totalTime; + } + + @Override + public double getTimeInPreviousState() + { + return timeInPreviousState; + } + + @Override + public double getRewardCumulatedSoFar(int index) + { + return totalRewards[index]; + } + + @Override + public double getPreviousStateReward(int index) + { + return previousStateRewards[index]; + } + + @Override + public double getPreviousTransitionReward(int index) + { + return previousTransitionRewards[index]; + } + + @Override + public double getCurrentStateReward(int index) + { + return currentStateRewards[index]; + } +} diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 2177b3ac..a433940d 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -30,6 +30,7 @@ package simulator; import java.util.*; import java.io.*; +import simulator.sampler.*; import parser.*; import parser.ast.*; import parser.type.*; @@ -152,9 +153,6 @@ import prism.*; * @author Andrew Hinton */ -// REMOVED: -// exportBinary functions - public class SimulatorEngine { // PRISM stuff @@ -173,7 +171,9 @@ public class SimulatorEngine // Properties info private PropertiesFile propertiesFile; - private List pathProps; + private List properties; + private List propertySamplers; + private Values propertyConstants; private ArrayList loadedProperties; @@ -188,15 +188,14 @@ public class SimulatorEngine // NEW STUFF: protected boolean onTheFly; - protected State lastState; + protected State previousState; protected State currentState; protected double currentStateRewards[]; // PATH: - protected Path path = null; + protected PathFull path = null; // TRANSITIONS: - protected List labels; // ------------------------------------------------------------------------------ @@ -243,7 +242,6 @@ public class SimulatorEngine // Current model private Values constants; - // ------------------------------------------------------------------------------ // Basic setup // ------------------------------------------------------------------------------ @@ -262,7 +260,8 @@ public class SimulatorEngine propertiesFile = null; constants = null; propertyConstants = null; - loadedProperties = null; + properties = null; + propertySamplers = null; } /** @@ -298,7 +297,7 @@ public class SimulatorEngine this.propertiesFile = (propertiesFile == null) ? new PropertiesFile(modulesFile) : propertiesFile; propertyConstants = this.propertiesFile.getConstantValues(); // Create empty path object associated with this model - path = new Path(this, modulesFile); + path = new PathFull(this, modulesFile); // This is not on-the-fly onTheFly = false; } @@ -349,6 +348,9 @@ public class SimulatorEngine // Initialise stored path if necessary if (!onTheFly) path.initialise(currentState, currentStateRewards); + // Reset and then update samplers for any loaded properties + resetSamplers(); + updateSamplers(); // Generate updates for initial state updater.calculateTransitions(currentState, transitionList); } @@ -566,12 +568,7 @@ public class SimulatorEngine */ public int addLabel(Expression label) throws PrismLangException { - // Take a copy, get rid of any constants and simplify - Expression labelNew = label.deepCopy(); - labelNew = (Expression) labelNew.replaceConstants(constants); - labelNew = (Expression) labelNew.simplify(); - labels.add(labelNew); - return labels.size() - 1; + return addLabel(label, null); } /** @@ -585,8 +582,11 @@ public class SimulatorEngine // Take a copy, get rid of any constants and simplify Expression labelNew = label.deepCopy(); labelNew = (Expression) labelNew.replaceConstants(constants); - labelNew = (Expression) labelNew.replaceConstants(pf.getConstantValues()); + if (pf != null) { + labelNew = (Expression) labelNew.replaceConstants(pf.getConstantValues()); + } labelNew = (Expression) labelNew.simplify(); + // Add to list and return index labels.add(labelNew); return labels.size() - 1; } @@ -594,13 +594,32 @@ public class SimulatorEngine /** * Add a (path) property to the simulator, whose value will be computed during path generation. * The resulting index of the property is returned: this is used for later queries about the property. + * Any constants/formulas etc. appearing in the label must have been defined in the current model. + * If there are additional constants (e.g. from a properties file), + * then use the {@link #addProperty(Expression, PropertiesFile)} method. */ - private int addProperty(Expression prop) + public int addProperty(Expression prop) throws PrismException { - // clone, converttountil, simplify ??? - - // TODO - return -1; + return addProperty(prop, null); + } + + /** + * Add a (path) property to the simulator, whose value will be computed during path generation. + * The resulting index of the property is returned: this is used for later queries about the property. + * Any constants/formulas etc. appearing in the property must have been defined in the current model + * or be supplied in the (optional) passed in PropertiesFile. + */ + public int addProperty(Expression prop, PropertiesFile pf) throws PrismException + { + // Take a copy, get rid of any constants and simplify + Expression propNew = prop.deepCopy(); + propNew = (Expression) propNew.replaceConstants(constants); + propNew = (Expression) propNew.replaceConstants(pf.getConstantValues()); + propNew = (Expression) propNew.simplify(); + // Create sampler, update lists and return index + properties.add(propNew); + propertySamplers.add(Sampler.createSampler(propNew, modulesFile)); + return properties.size() - 1; } /** @@ -692,9 +711,9 @@ public class SimulatorEngine // Evaluate constants and optimise (a copy of) modules file for simulation modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(constants).simplify(); mainLog.println(modulesFile); - + // Create state/transition storage - lastState = new State(numVars); + previousState = new State(numVars); currentState = new State(numVars); currentStateRewards = new double[modulesFile.getNumRewardStructs()]; transitionList = new TransitionList(); @@ -702,8 +721,10 @@ public class SimulatorEngine // Create updater for model updater = new Updater(this, modulesFile); - // Create storage for labels + // Create storage for labels/properties labels = new ArrayList(); + properties = new ArrayList(); + propertySamplers = new ArrayList(); } /** @@ -720,8 +741,8 @@ public class SimulatorEngine // Get corresponding choice Choice choice = transitionList.getChoice(i); // Remember last state and compute next one (and its state rewards) - lastState.copy(currentState); - choice.computeTarget(offset, lastState, currentState); + previousState.copy(currentState); + choice.computeTarget(offset, previousState, currentState); updater.calculateStateRewards(currentState, currentStateRewards); // Store path info (if necessary) if (!onTheFly) { @@ -730,6 +751,8 @@ public class SimulatorEngine path.addStep(index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); // TODO: first currentStateRewards in above should be new *trans* rewards! } + // Update samplers for any loaded properties + updateSamplers(); // Generate updates for next state updater.calculateTransitions(currentState, transitionList); } @@ -752,8 +775,8 @@ public class SimulatorEngine // Get corresponding choice Choice choice = transitionList.getChoice(i); // Remember last state and compute next one (and its state rewards) - lastState.copy(currentState); - choice.computeTarget(offset, lastState, currentState); + previousState.copy(currentState); + choice.computeTarget(offset, previousState, currentState); updater.calculateStateRewards(currentState, currentStateRewards); // Store path info (if necessary) if (!onTheFly) { @@ -762,10 +785,33 @@ public class SimulatorEngine path.addStep(time, index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); // TODO: first currentStateRewards in above should be new *trans* rewards! } + // Update samplers for any loaded properties + updateSamplers(); // Generate updates for next state updater.calculateTransitions(currentState, transitionList); } + /** + * Reset samplers for any loaded properties that a new step has occurred. + */ + private void resetSamplers() throws PrismLangException + { + for (Sampler sampler : propertySamplers) { + sampler.reset(); + } + } + + /** + * Notify samplers for any loaded properties that a new step has occurred. + */ + private void updateSamplers() throws PrismLangException + { + for (Sampler sampler : propertySamplers) { + if (!sampler.isCurrentValueKnown()) + sampler.update(path); + } + } + // ------------------------------------------------------------------------------ // Queries regarding model // ------------------------------------------------------------------------------ @@ -930,9 +976,7 @@ public class SimulatorEngine // ------------------------------------------------------------------------------ /** - * Returns the number of states stored in the current path table. - * - * @return the number of states stored in the current path table. + * Get the size of the current path (number of steps; or number of states - 1). */ public int getPathSize() { @@ -1204,16 +1248,15 @@ public class SimulatorEngine * if anything goes wrong. * @return the result. */ - public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, - Values initialState, int noIterations, int maxPathLength) throws PrismException + public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, Values initialState, int noIterations, + int maxPathLength) throws PrismException { ArrayList exprs; Object res[]; exprs = new ArrayList(); exprs.add(expr); - res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations, - maxPathLength); + res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations, maxPathLength); if (res[0] instanceof PrismException) throw (PrismException) res[0]; @@ -1240,11 +1283,12 @@ public class SimulatorEngine * * */ - public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, - List exprs, Values initialState, int noIterations, int maxPathLength) - throws PrismException + public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, List exprs, Values initialState, + int noIterations, int maxPathLength) throws PrismException { - createNewOnTheFlyPath(modulesFile, propertiesFile); + // TODO: make on the fly again + //createNewOnTheFlyPath(modulesFile, propertiesFile); + createNewPath(modulesFile, propertiesFile); Object[] results = new Object[exprs.size()]; int[] indices = new int[exprs.size()]; @@ -1256,7 +1300,7 @@ public class SimulatorEngine for (int i = 0; i < exprs.size(); i++) { try { checkPropertyForSimulation((Expression) exprs.get(i), modulesFile.getModelType()); - indices[i] = addProperty((Expression) exprs.get(i)); + indices[i] = addProperty((Expression) exprs.get(i), propertiesFile); if (indices[i] >= 0) validPropsCount++; } catch (PrismException e) { @@ -1267,18 +1311,14 @@ public class SimulatorEngine // as long as there are at least some valid props, do sampling if (validPropsCount > 0) { - initialisePath(initialState); - int result = 0;//doSampling(noIterations, maxPathLength); - if (result == ERROR) { - throw new PrismException(getLastErrorMessage()); - } + doSampling(new State(initialState), noIterations, maxPathLength); } // process the results for (int i = 0; i < results.length; i++) { // if we have already stored an error for this property, keep it as the result if (!(results[i] instanceof PrismException)) - results[i] = processSamplingResult((Expression) exprs.get(i), indices[i]); + results[i] = propertySamplers.get(indices[i]).getMeanValue(); } // display results to log @@ -1323,10 +1363,9 @@ public class SimulatorEngine * @throws PrismException * 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, InterruptedException, - PrismException + public void modelCheckExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, + ResultsCollection resultsCollection, Expression propertyToCheck, Values initialState, int maxPathLength, int noIterations) throws PrismException, + InterruptedException, PrismException { int n; Values definedPFConstants = new Values(); @@ -1347,7 +1386,7 @@ public class SimulatorEngine propertyConstants = propertiesFile.getConstantValues(); try { checkPropertyForSimulation(propertyToCheck, modulesFile.getModelType()); - indices[i] = addProperty(propertyToCheck); + indices[i] = addProperty(propertyToCheck, propertiesFile); if (indices[i] >= 0) validPropsCount++; } catch (PrismException e) { @@ -1381,64 +1420,61 @@ public class SimulatorEngine mainLog.println("\nResult: " + results[0]); } else { mainLog.println("\nResults:"); - mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ", - false)); + mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ", false)); } } - /* - private int doSampling(State initialState, int numIters, int maxPathLength) + private void doSampling(State initialState, int numIters, int maxPathLength) throws PrismException { - int iteration_counter = 0; - int last_percentage_done = -1; - int percentage_done = -1; - double average_path_length = 0; - int min_path_length = 0, max_path_length = 0; - boolean stopped_early = false; + int iters = 0; + int lastPercentageDone = 0; + int percentageDone = 0; + double avgPathLength = 0; + int minPathFound = 0, maxPathFound = 0; + boolean stoppedEarly = false; boolean deadlocks_found = false; - //The current path - int current_index; - + boolean allKnown = false; + int i; + //double* path_cost = new double[no_reward_structs]; //double* total_state_cost = new double[no_reward_structs]; //double* total_transition_cost = new double[no_reward_structs]; - + // Timing info long start, start2, stop; double time_taken; - + //Loop detection requires that deterministic paths are //stored, until that determinism is broken. This path //is allocated dynamically, 10 steps at a time. //CSamplingLoopDetectionHandler* loop_detection = new CSamplingLoopDetectionHandler(); - + //TODO: allow stopping of sampling mid-way through? //External flag set to false boolean should_stop_sampling = false; - + start = start2 = System.currentTimeMillis(); - + mainLog.print("\nSampling progress: ["); mainLog.flush(); - + //The loop continues until each pctl/csl formula is satisfied: //E.g. usually, this is when the correct number of iterations //has been performed, but for some, such as cumulative rewards //this can be early if a loop is detected at any point, this //is all handled by the All_Done_Sampling() function - + // Main sampling loop - while (!should_stop_sampling && !isSamplingDone()) { - + while (!should_stop_sampling && !isSamplingDone() && iters < numIters) { + // Display progress - percentage_done = ((10*(iteration_counter))/numIters)*10; - if (percentage_done > last_percentage_done) { - last_percentage_done = percentage_done; - //cout << " " << last_percentage_done << "%" << endl; - mainLog.print(" " + last_percentage_done + "%"); + percentageDone = ((10 * (iters)) / numIters) * 10; + if (percentageDone > lastPercentageDone) { + lastPercentageDone = percentageDone; + mainLog.print(" " + lastPercentageDone + "%"); mainLog.flush(); } - + //do polling and feedback every 2 seconds stop = System.currentTimeMillis(); if (stop - start2 > 2000) { @@ -1446,32 +1482,34 @@ public class SimulatorEngine //int poll = Poll_Control_File(); //if(poll & STOP_SAMPLING == STOP_SAMPLING) // should_stop_sampling = true; - start2 = System.currentTimeMillis(); + start2 = System.currentTimeMillis(); } - - iteration_counter++; - + + iters++; + // Start the new path for this iteration (sample) - initialisePath(initialState); - + initialisePath(initialState); + //loop_detection->Reset(); - - - notifyPathFormulae(last_state, state_variables, loop_detection); - + // Generate a path, up to at most maxPathLength steps - for (current_index = 0; - !All_PCTL_Answers_Known(loop_detection) && //not got answers for all properties yet - //!loop_detection->Is_Proven_Looping() //not looping (removed this - e.g. cumul rewards can't stop yet) - current_index < path_length; //not exceeding path_length - current_index++) - { - // Make a random transition - automaticChoice(detect); + for (i = 0; i < maxPathLength; i++) { - //if(!loop_detection->Is_Proven_Looping()) { // removed this: for e.g. cumul rewards need to keep counting in loops... + // See if all samplers have established a value; if so, stop. + allKnown = true; + for (Sampler sampler : propertySamplers) { + if (!sampler.isCurrentValueKnown()) + allKnown = false; + } + if (allKnown) + break; - if (modelType.continuousTime()) { + // Make a random transition + automaticChoice(true); + + //if(!loop_detection->Is_Proven_Looping()) { // removed this: for e.g. cumul rewards need to keep counting in loops... + + /*if (modelType.continuousTime()) { double time_in_state = Get_Sampled_Time(); last_state->time_spent_in_state = time_in_state; @@ -1503,84 +1541,67 @@ public class SimulatorEngine } Notify_Path_Formulae(last_state, state_variables, loop_detection); - } + }*/ //} - + } - + // record if we found any deadlocks (can check this outside path gen loop because never escape deadlocks) - if (loop_detection->Is_Deadlock()) deadlocks_found = true; - - // compute path length statistics so far - average_path_length = (average_path_length*(iteration_counter-1)+(current_index))/iteration_counter; - min_path_length = (iteration_counter == 1) ? current_index : ((current_index < min_path_length) ? current_index : min_path_length); - max_path_length = (iteration_counter == 1) ? current_index : ((current_index > max_path_length) ? current_index : max_path_length); - - //Get samples and notify sample collectors - Do_A_Sample(loop_detection); + //if (loop_detection->Is_Deadlock()) deadlocks_found = true; + + // Update path length statistics + avgPathLength = (avgPathLength * (iters - 1) + (i)) / iters; + minPathFound = (iters == 1) ? i : Math.min(minPathFound, i); + maxPathFound = (iters == 1) ? i : Math.max(maxPathFound, i); - // stop early if any of the properties couldn't be sampled - if (Get_Total_Num_Reached_Max_Path() > 0) { stopped_early = true; break; } + // If not all samplers could produce values, this an error + if (!allKnown) { + stoppedEarly = true; + break; + } - }//end sampling while - - if (!stopped_early) { + // Update state of samplers based on last path + for (Sampler sampler : propertySamplers) { + sampler.updateStats(); + } + } + + if (!stoppedEarly) { if (!should_stop_sampling) mainLog.print(" 100% ]"); mainLog.println(); stop = System.currentTimeMillis(); time_taken = (stop - start) / 1000.0; mainLog.print("\nSampling complete: "); - mainLog.print(iteration_counter + " iterations in " + time_taken + " seconds (average " + time_taken/iteration_counter + ")\n"); - mainLog.print("Path length statistics: average " + average_path_length + ", min " + min_path_length + ", max " + max_path_length + "\n"); + mainLog.print(iters + " iterations in " + time_taken + " seconds (average " + time_taken / iters + ")\n"); + mainLog.print("Path length statistics: average " + avgPathLength + ", min " + minPathFound + ", max " + maxPathFound + "\n"); } else { - mainLog.print(" ...\n\nSampling terminated early after " + iteration_counter + " iterations.\n"); + mainLog.print(" ...\n\nSampling terminated early after " + iters + " iterations.\n"); } - + // print a warning if deadlocks occurred at any point if (deadlocks_found) mainLog.print("\nWarning: Deadlocks were found during simulation: self-loops were added\n"); - + // print a warning if simulation was stopped by the user if (should_stop_sampling) mainLog.print("\nWarning: Simulation was terminated before completion.\n"); - + //write to feedback file with true to indicate that we have finished sampling - Write_Feedback(iteration_counter, numIters, true); - - //Print_Sampling_Results(); - delete loop_detection; - delete[] starting_variables; - delete last_state; - delete[] path_cost; - delete[] total_state_cost; - delete[] total_transition_cost; - - if (stopped_early) { - Report_Error("One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length"); - throw 0; - } - - - // TODO: - return -1; - }*/ + //Write_Feedback(iteration_counter, numIters, true); - private void notifyPathFormulae() - { - /*for(int i = 0; i< no_path_formulae; i++) - { - if(!registered_path_formulae[i]->Is_Answer_Known(loop_detection)) - registered_path_formulae[i]->Notify_State(last_state, current_state); - }*/ + if (stoppedEarly) { + throw new PrismException( + "One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length"); + } } - + private boolean isSamplingDone() { // TODO return false; } - + private static native double getSamplingResult(int propertyIndex); private static native int getNumReachedMaxPath(int propertyIndex); @@ -1647,8 +1668,7 @@ public class SimulatorEngine expr = ((ExpressionReward) prop).getExpression(); } if (!ok) - throw new PrismException( - "Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\""); + throw new PrismException("Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\""); // Check that there are no nested probabilistic operators try { diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index a34ad8fd..2db1534c 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -108,8 +108,8 @@ public class Updater int i, j, n, count, n2, n3; double p; - System.out.println("Synchs: " + synchs); - System.out.println("Calc updates for " + state); + //System.out.println("Synchs: " + synchs); + //System.out.println("Calc updates for " + state); // Clear lists/bitsets transitionList.clear(); for (i = 0; i < numModules; i++) { @@ -125,7 +125,7 @@ public class Updater for (i = 0; i < numModules; i++) { calculateUpdatesForModule(i, state); } - System.out.println("updateLists: " + updateLists); + //System.out.println("updateLists: " + updateLists); // Combination of updates depends on model type /*switch (modelType) { @@ -167,7 +167,7 @@ public class Updater // TODO throw new PrismLangException("Don't handle local nondet yet"); } - System.out.println("prod" + j + ": " + prod); + //System.out.println("prod" + j + ": " + prod); } transitionList.add(prod); n++; @@ -226,7 +226,7 @@ public class Updater // For DTMCs, need to randomise - System.out.println(transitionList); + //System.out.println(transitionList); } diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java new file mode 100644 index 00000000..49e1faed --- /dev/null +++ b/prism/src/simulator/sampler/Sampler.java @@ -0,0 +1,205 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import parser.ast.*; +import prism.PrismException; +import prism.PrismLangException; + +/** + * Samplers: determine values based on a sequence of simulation paths. + */ +public abstract class Sampler +{ + protected boolean valueKnown; + + /** + * Is the current value of the sampler known, based on the path seen so far? + */ + public boolean isCurrentValueKnown() + { + return valueKnown; + } + + /** + * Reset the current value of the sampler and whether it is known or not. + */ + public abstract void reset(); + + /** + * Reset all statistics for the sampler. + */ + public abstract void resetStats(); + + /** + * Update the current value of the sampler based on the current simulation path. + * It is assumed that this is called at every step of the path. + * It is also assumed that this is not called after the value becomes known. + */ + public abstract void update(Path path) throws PrismLangException; + + /** + * Update the statistics for the sampler, assuming that the current path is finished. + */ + public abstract void updateStats(); + + /** + * Get the current value of the sampler. + */ + public abstract Object getCurrentValue(); + + /** + * Get the mean value of the sampler, over all paths seen. + */ + public abstract Object getMeanValue(); + + // Static methods for sampler creation + + /** + * Create a sampler for an expression (P=? or R=?). + * Expression should contain no constants/formula/etc. + * The model to which the property applies should also be specified. + */ + public static Sampler createSampler(Expression expr, ModulesFile mf) throws PrismException + { + Sampler sampler = null; + // P=? + if (expr instanceof ExpressionProb) { + ExpressionProb propProb = (ExpressionProb) expr; + // Test whether this is a simple path formula (i.e. non-LTL) + if (propProb.getExpression().isSimplePathFormula()) { + sampler = createSamplerForProbPathPropertySimple(propProb.getExpression(), mf); + } else { + throw new PrismException("LTL-style path formulas are not supported by the simulator"); + } + } + // R=? + else if (expr instanceof ExpressionReward) { + sampler = createSamplerForRewardProperty((ExpressionReward) expr, mf); + } + // Neither + else { + throw new PrismException("Can't create sampler for property \"" + expr + "\""); + } + return sampler; + } + + private static SamplerBoolean createSamplerForProbPathPropertySimple(Expression expr, ModulesFile mf) throws PrismException + { + // Negation/parentheses + if (expr instanceof ExpressionUnaryOp) { + ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; + // Parentheses + if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { + // Recurse + return createSamplerForProbPathPropertySimple(exprUnary.getOperand(), mf); + } + // Negation + else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { + // Recurse, then negate meaning + SamplerBoolean sampler = createSamplerForProbPathPropertySimple(exprUnary.getOperand(), mf); + sampler.negate(); + return sampler; + } + } + // Temporal operators + else if (expr instanceof ExpressionTemporal) { + ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + // Next + if (exprTemp.getOperator() == ExpressionTemporal.P_X) { + return new SamplerNext(exprTemp); + } + // Until + else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { + if (exprTemp.hasBounds()) { + if (mf.getModelType().continuousTime()) { + // Continuous-time bounded until + return new SamplerBoundedUntilCont(exprTemp); + } else { + // Discrete-time bounded until + return new SamplerBoundedUntilDisc(exprTemp); + } + } else { + // Unbounded until + return new SamplerUntil(exprTemp); + } + } + // Anything else - convert to until and recurse + else { + return createSamplerForProbPathPropertySimple(exprTemp.convertToUntilForm(), mf); + } + } + + throw new PrismException("Can't create sampler for property \"" + expr + "\""); + } + + private static SamplerDouble createSamplerForRewardProperty(ExpressionReward expr, ModulesFile mf) throws PrismException + { + // Extract reward structure index + Object rs = expr.getRewardStructIndex(); + int rsi = -1; + if (mf.getNumRewardStructs() == 0) + throw new PrismException("Model has no rewards specified"); + if (rs == null) { + rsi = 0; + } else if (rs instanceof Expression) { + rsi = ((Expression) rs).evaluateInt() - 1; + rs = new Integer(rsi + 1); // for better error reporting below + } else if (rs instanceof String) { + rsi = mf.getRewardStructIndex((String) rs); + } + if (rsi == -1) + throw new PrismException("Invalid reward structure index \"" + rs + "\""); + + // Construct sampler based on type + ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression(); + switch (exprTemp.getOperator()) { + case ExpressionTemporal.R_C: + if (mf.getModelType().continuousTime()) { + // Continuous-time cumulative reward + return new SamplerRewardCumulCont(exprTemp, rsi); + } else { + // Discrete-time cumulative reward + return new SamplerRewardCumulDisc(exprTemp, rsi); + } + case ExpressionTemporal.R_I: + if (mf.getModelType().continuousTime()) { + // Continuous-time instantaneous reward + return new SamplerRewardInstCont(exprTemp, rsi); + } else { + // Discrete-time instantaneous reward + return new SamplerRewardInstDisc(exprTemp, rsi); + } + case ExpressionTemporal.R_F: + // reachability reward + return new SamplerRewardReach(exprTemp, rsi); + } + + throw new PrismException("Can't create sampler for property \"" + expr + "\""); + } +} diff --git a/prism/src/simulator/sampler/SamplerBoolean.java b/prism/src/simulator/sampler/SamplerBoolean.java new file mode 100644 index 00000000..a991add4 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerBoolean.java @@ -0,0 +1,99 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.PrismLangException; + +/** + * Samplers for properties that associate a simulation path with a Boolean value. + */ +public abstract class SamplerBoolean extends Sampler +{ + // Value of current path + protected boolean value; + // Whether the actual value should be the negation of 'value' + protected boolean negated = false; + // Stats over all paths + protected int numSamples; + protected int numTrue; + + @Override + public void reset() + { + valueKnown = false; + value = false; + } + + @Override + public void resetStats() + { + numSamples = 0; + numTrue = 0; + } + + @Override + public abstract void update(Path path) throws PrismLangException; + + @Override + public void updateStats() + { + numSamples++; + // XOR: value && !negated || !value && negated + if (value != negated) + numTrue++; + } + + @Override + public Object getCurrentValue() + { + // XOR: value && !negated || !value && negated + return new Boolean(value != negated); + } + + @Override + public Object getMeanValue() + { + return new Double(numTrue / (double) numSamples); + } + + /** + * Negate the meaning of this sampler. + */ + public boolean negate() + { + return negated = !negated; + } + + /** + * Is this sampler negated? + */ + public boolean getNegated() + { + return negated; + } +} diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java new file mode 100644 index 00000000..ea2f31a7 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -0,0 +1,114 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +/** + * Construct a sampler for a (continuous-time) bounded until property. + * Passed in ExpressionTemporal should be a formula of this type. + * All constants should have already been evaluated/replaced. + */ +public class SamplerBoundedUntilCont extends SamplerBoolean +{ + private Expression left; + private Expression right; + private double lb; + private double ub; + + /** + * Construct a sampler for a (continuous) time-bounded until formula. + * Passed in ExpressionTemporal should be a property of this type. + * All constants should have already been evaluated/replaced. + */ + public SamplerBoundedUntilCont(ExpressionTemporal expr) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.P_U) + throw new PrismException("Error creating Sampler"); + left = expr.getOperand1(); + right = expr.getOperand2(); + lb = expr.getLowerBound() == null ? 0.0 : expr.getLowerBound().evaluateDouble(); + ub = expr.getUpperBound() == null ? Double.POSITIVE_INFINITY: expr.getUpperBound().evaluateDouble(); + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + if (path.size() > 0) { + double time_so_far = path.getTimeSoFar(); + if (time_so_far > ub) { + // must take into account the possibility of missing lower bound + + // could have missed out evaluation of right + if (time_so_far - path.getTimeInPreviousState() <= lb) { + if (right.evaluateBoolean(path.getPreviousState())) { + valueKnown = true; + value = true; + } else { + valueKnown = true; + value = false; + } + } else { + valueKnown = true; + value = false; + } + } else if (time_so_far <= lb) { + if (!left.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = false; + } + } else { + if (right.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = true; + } else if (!left.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = false; + } + } + } else { + if (lb == 0.0) { + if (right.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = true; + } + } else { + if (!left.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = false; + } + } + } + } +} diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java new file mode 100644 index 00000000..ed64c5ec --- /dev/null +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -0,0 +1,84 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.*; +import parser.ast.*; + +public class SamplerBoundedUntilDisc extends SamplerBoolean +{ + private Expression left; + private Expression right; + private int lb; + private int ub; + + /** + * Construct a sampler for a (discrete-time) bounded until property. + * Passed in ExpressionTemporal should be a property of this type. + * All constants should have already been evaluated/replaced. + */ + public SamplerBoundedUntilDisc(ExpressionTemporal expr) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.P_U) + throw new PrismException("Error creating Sampler"); + left = expr.getOperand1(); + right = expr.getOperand2(); + lb = expr.getLowerBound() == null ? 0 : expr.getLowerBound().evaluateInt(); + ub = expr.getUpperBound() == null ? Integer.MAX_VALUE : expr.getUpperBound().evaluateInt(); + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + int pathSize = path.size(); + if (pathSize > ub) { + valueKnown = true; + value = false; + } else if (pathSize < lb) { + if (!left.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = false; + } + } else { + State currentState = path.getCurrentState(); + if (right.evaluateBoolean(currentState)) { + valueKnown = true; + value = true; + } else if (!left.evaluateBoolean(currentState)) { + valueKnown = true; + value = false; + } + } + } +} diff --git a/prism/src/simulator/sampler/SamplerDouble.java b/prism/src/simulator/sampler/SamplerDouble.java new file mode 100644 index 00000000..aa84bad2 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerDouble.java @@ -0,0 +1,78 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.PrismLangException; + +/** + * Samplers for properties that associate a simulation path with a real (double) value. + */ +public abstract class SamplerDouble extends Sampler +{ + // Value of current path + protected double value; + // Stats over all paths + protected double valueSum; + protected int numSamples; + + @Override + public void reset() + { + valueKnown = false; + value = 0.0; + } + + @Override + public void resetStats() + { + valueSum = 0.0; + numSamples = 0; + } + + @Override + public abstract void update(Path path) throws PrismLangException; + + @Override + public void updateStats() + { + valueSum += value; + numSamples++; + } + + @Override + public Object getCurrentValue() + { + return new Double(value); + } + + @Override + public Object getMeanValue() + { + return new Double(valueSum / numSamples); + } +} diff --git a/prism/src/simulator/sampler/SamplerNext.java b/prism/src/simulator/sampler/SamplerNext.java new file mode 100644 index 00000000..472aeaca --- /dev/null +++ b/prism/src/simulator/sampler/SamplerNext.java @@ -0,0 +1,66 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.*; +import parser.ast.*; + +public class SamplerNext extends SamplerBoolean +{ + private Expression target; + + /** + * Construct a sampler for a "next" property. + * Passed in ExpressionTemporal should be a property of this type. + * All constants should have already been evaluated/replaced. + */ + public SamplerNext(ExpressionTemporal expr) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.P_X) + throw new PrismException("Error creating Sampler"); + target = expr.getOperand2(); + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + // X "target" is true iff state 1 satisfies "target" + if (path.size() == 1) { + valueKnown = true; + value = target.evaluateBoolean(path.getCurrentState()); + } + // Nothing else to do: if path size is 0, can't decide; + // if path size > 1 (should never happen), nothing changes + } +} diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java new file mode 100644 index 00000000..18d351ce --- /dev/null +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -0,0 +1,75 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +public class SamplerRewardCumulCont extends SamplerDouble +{ + private double timeBound; + private int rewardStructIndex; + + /** + * Construct a sampler for a (continuous-time) cumulative reward property. + * Passed in ExpressionTemporal should be a property of this type. + * Reward structure index should also be specified. + * All constants should have already been evaluated/replaced. + */ + public SamplerRewardCumulCont(ExpressionTemporal expr, int rewardStructIndex) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.R_C) + throw new PrismException("Error creating Sampler"); + timeBound = expr.getUpperBound().evaluateDouble(); + this.rewardStructIndex = rewardStructIndex; + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + // As soon as time bound exceeded, compute reward total + if (path.getTimeSoFar() >= timeBound) { + valueKnown = true; + value = path.getRewardCumulatedSoFar(rewardStructIndex); + // Compute excess time, i.e. how long ago time bound was reached + double excessTime = timeBound - path.getTimeSoFar(); + // If this is > 0 (very likely, unless time bound = 0), + // need to subtract reward accumulated in excess time + // (i.e. fraction of previous state reward, and transition reward) + if (excessTime > 0) { + value -= path.getPreviousStateReward(rewardStructIndex) * (excessTime / path.getTimeInPreviousState()); + value -= path.getPreviousTransitionReward(rewardStructIndex); + } + } + } +} diff --git a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java new file mode 100644 index 00000000..afc5eee2 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java @@ -0,0 +1,66 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +public class SamplerRewardCumulDisc extends SamplerDouble +{ + private int timeBound; + private int rewardStructIndex; + + /** + * Construct a sampler for a (discrete-time) cumulative reward property. + * Passed in ExpressionTemporal should be a property of this type. + * Reward structure index should also be specified. + * All constants should have already been evaluated/replaced. + */ + public SamplerRewardCumulDisc(ExpressionTemporal expr, int rewardStructIndex) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.R_C) + throw new PrismException("Error creating Sampler"); + timeBound = expr.getUpperBound().evaluateInt(); + this.rewardStructIndex = rewardStructIndex; + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + // As soon as time bound reached, store current reward total + if (path.size() == timeBound) { + valueKnown = true; + value = path.getRewardCumulatedSoFar(rewardStructIndex); + } + } +} diff --git a/prism/src/simulator/sampler/SamplerRewardInstCont.java b/prism/src/simulator/sampler/SamplerRewardInstCont.java new file mode 100644 index 00000000..acac15dd --- /dev/null +++ b/prism/src/simulator/sampler/SamplerRewardInstCont.java @@ -0,0 +1,72 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +public class SamplerRewardInstCont extends SamplerDouble +{ + private double time; + private int rewardStructIndex; + + /** + * Construct a sampler for a (continuous-time) instantaneous reward property. + * Passed in ExpressionTemporal should be a property of this type. + * Reward structure index should also be specified. + * All constants should have already been evaluated/replaced. + */ + public SamplerRewardInstCont(ExpressionTemporal expr, int rewardStructIndex) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.R_C) + throw new PrismException("Error creating Sampler"); + time = expr.getUpperBound().evaluateDouble(); + this.rewardStructIndex = rewardStructIndex; + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + // As soon as time bound exceeded, compute reward + if (path.getTimeSoFar() >= time) { + valueKnown = true; + // Time bound was exceeded in either previous or current state + // (unless the time bound is 0, the latter is very unlikely) + if (path.getTimeSoFar() > time) { + value = path.getPreviousStateReward(rewardStructIndex); + } else { + value = path.getCurrentStateReward(rewardStructIndex); + } + } + } +} diff --git a/prism/src/simulator/sampler/SamplerRewardInstDisc.java b/prism/src/simulator/sampler/SamplerRewardInstDisc.java new file mode 100644 index 00000000..1109efb8 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerRewardInstDisc.java @@ -0,0 +1,66 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +public class SamplerRewardInstDisc extends SamplerDouble +{ + private int time; + private int rewardStructIndex; + + /** + * Construct a sampler for a (discrete-time) instantaneous reward property. + * Passed in ExpressionTemporal should be a property of this type. + * Reward structure index should also be specified. + * All constants should have already been evaluated/replaced. + */ + public SamplerRewardInstDisc(ExpressionTemporal expr, int rewardStructIndex) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.R_C) + throw new PrismException("Error creating Sampler"); + time = expr.getUpperBound().evaluateInt(); + this.rewardStructIndex = rewardStructIndex; + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + // As soon as time bound reached, store current state reward + if (path.size() == time) { + valueKnown = true; + value = path.getCurrentStateReward(rewardStructIndex); + } + } +} diff --git a/prism/src/simulator/sampler/SamplerRewardReach.java b/prism/src/simulator/sampler/SamplerRewardReach.java new file mode 100644 index 00000000..f124ae6f --- /dev/null +++ b/prism/src/simulator/sampler/SamplerRewardReach.java @@ -0,0 +1,65 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import prism.*; +import parser.ast.*; + +public class SamplerRewardReach extends SamplerDouble +{ + private Expression target; + private int rewardStructIndex; + + /** + * Construct a sampler for a reachability reward property. + * Passed in ExpressionTemporal should be a property of this type. + * Reward structure index should also be specified. + * All constants should have already been evaluated/replaced. + */ + public SamplerRewardReach(ExpressionTemporal expr, int rewardStructIndex) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.R_F) + throw new PrismException("Error creating Sampler"); + target = expr.getOperand2(); + this.rewardStructIndex = rewardStructIndex; + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + if (target.evaluateBoolean(path.getCurrentState())) { + valueKnown = true; + value = path.getRewardCumulatedSoFar(rewardStructIndex); + } + } +} diff --git a/prism/src/simulator/sampler/SamplerUntil.java b/prism/src/simulator/sampler/SamplerUntil.java new file mode 100644 index 00000000..ad5b6f92 --- /dev/null +++ b/prism/src/simulator/sampler/SamplerUntil.java @@ -0,0 +1,74 @@ +//============================================================================== +// +// Copyright (c) 2002- +// 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.sampler; + +import simulator.*; +import parser.State; +import parser.ast.Expression; +import parser.ast.ExpressionTemporal; +import prism.PrismException; +import prism.PrismLangException; + +public class SamplerUntil extends SamplerBoolean +{ + private Expression left; + private Expression right; + + /** + * Construct a sampler for a (unbounded) until property. + * Passed in ExpressionTemporal should be a property of this type. + * All constants should have already been evaluated/replaced. + */ + public SamplerUntil(ExpressionTemporal expr) throws PrismException + { + // Make sure expression is of the correct type + // Then extract other required info + if (expr.getOperator() != ExpressionTemporal.P_U) + throw new PrismException("Error creating Sampler"); + left = expr.getOperand1(); + right = expr.getOperand2(); + // Initialise sampler info + reset(); + resetStats(); + } + + @Override + public void update(Path path) throws PrismLangException + { + State currentState = path.getCurrentState(); + // Have we reached the target (i.e. RHS of until)? + if (right.evaluateBoolean(currentState)) { + valueKnown = true; + value = true; + } + // Or, if not, have we violated the LJS of the until? + else if (!left.evaluateBoolean(currentState)) { + valueKnown = true; + value = false; + } + } +}