s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

More simulator additions/tidying. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1891 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
82b8965563
commit
763285cc4c
4 changed files with 174 additions and 304 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 25
      prism/src/prism/Prism.java
  2. 443
      prism/src/simulator/SimulatorEngine.java
  3. 4
      prism/src/userinterface/properties/GUIMultiProperties.java
  4. 6
      prism/src/userinterface/simulator/GUISimulator.java

25
prism/src/prism/Prism.java
View File

@ -28,8 +28,7 @@
package prism;
import java.io.*;
import java.util.ArrayList;
import java.util.Vector;
import java.util.*;
import jdd.*;
import dv.*;
@ -1405,20 +1404,23 @@ public class Prism implements PrismSettingsListener
// check if a property is suitable for analysis with the simulator
public void checkPropertyForSimulation(Expression f, ModelType modelType) throws PrismException
public void checkPropertyForSimulation(Expression expr) throws PrismException
{
getSimulator().checkPropertyForSimulation(f, modelType);
getSimulator().checkPropertyForSimulation(expr);
}
// model check using simulator
// returns result or throws an exception in case of error
public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression f, Values initialState, int noIterations, int maxPathLength) throws PrismException
public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, Values initialState, int noIterations, int maxPathLength) throws PrismException
{
Object res = null;
//do model checking
res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, f, initialState, noIterations, maxPathLength);
// Check that property is valid for this model type
expr.checkValid(modulesFile.getModelType());
// Do model checking
res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, expr, new State(initialState), noIterations, maxPathLength);
return new Result(res);
}
@ -1427,11 +1429,16 @@ public class Prism implements PrismSettingsListener
// returns an array of results, some of which may be Exception objects if there were errors
// in the case of an error which affects all properties, an exception is thrown
public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, ArrayList<Expression> fs, Values initialState, int noIterations, int maxPathLength) throws PrismException
public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, Values initialState, int noIterations, int maxPathLength) throws PrismException
{
Object[] res = null;
res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, fs, initialState, noIterations, maxPathLength);
// Check that properties are valid for this model type
for (Expression expr : exprs)
expr.checkValid(modulesFile.getModelType());
// Do model checking
res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, new State(initialState), noIterations, maxPathLength);
Result[] resArray = new Result[res.length];
for (int i = 0; i < res.length; i++) resArray[i] = new Result(res[i]);

443
prism/src/simulator/SimulatorEngine.java
View File

@ -3,7 +3,6 @@
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
// * Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
//
//------------------------------------------------------------------------------
//
@ -38,6 +37,8 @@ import parser.visitor.ASTTraverse;
import prism.*;
/**
* TODO: rewrite from scratch:
*
* The SimulatorEngine class uses the JNI to provide a Java interface to the PRISM simulator engine library, written in
* c++. There are two ways to use this API:
* <UL>
@ -184,7 +185,7 @@ public class SimulatorEngine
// TODO: remove these now can get from path?
protected State previousState;
protected State currentState;
// TODO: just temp storage?
// (if so, remove 'current', 'prev' from names?)
protected double currentStateRewards[];
@ -335,45 +336,28 @@ public class SimulatorEngine
executeTimedTransition(i, offset, time, index);
}
/**
* This function makes n automatic choices of updates to the global state.
*
* @param n
* the number of automatic choices to be made.
* @throws PrismException
* if something goes wrong when updating the state.
*/
public void automaticTransitions(int n) throws PrismException
{
automaticTransitions(n, true);
}
public void automaticTransitions(int n, boolean detect) throws PrismException
{
int i;
for (i = 0; i < n; i++)
automaticTransition(detect);
}
/**
* Select, at random, a transition from the current transition list and execute it.
* For continuous-time models, the time to be spent in the state before leaving is also picked randomly.
* @param detect Whether...
* throws an exception if deadlock...
* If there is currently a deadlock, no transition is taken.
* The function returns a boolean value, with true indicating a transition was successfully taken.
* @param detect Whether... TODO
*/
public void automaticTransition(boolean detect) throws PrismException
public boolean automaticTransition(boolean detect) throws PrismException
{
Choice choice;
int numChoices, i, j;
double d, r;
// Check for deadlock; if so, stop and return false
numChoices = transitionList.getNumChoices();
if (numChoices == 0)
return false;
//throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
switch (modelType) {
case DTMC:
case MDP:
// Check for deadlock
numChoices = transitionList.getNumChoices();
if (numChoices == 0)
throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
// Pick a random choice
i = rng.randomUnifInt(numChoices);
choice = transitionList.getChoice(i);
@ -384,10 +368,6 @@ public class SimulatorEngine
executeTransition(i, j, -1);
break;
case CTMC:
// Check for deadlock
numChoices = transitionList.getNumChoices();
if (numChoices == 0)
throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
// Get sum of all rates
r = transitionList.getProbabilitySum();
// Pick a random number to determine choice/transition
@ -398,62 +378,52 @@ public class SimulatorEngine
executeTimedTransition(ref.i, ref.offset, rng.randomExpDouble(r), -1);
break;
}
return true;
}
/**
* Randomly select and execute transitions until the specified time delay is first exceeded.
* (Time is measured from the initial execution of this method, not total time.)
* (For discrete-time models, this just results in ceil(time) steps being executed.)
* (If deadlock...
*/
/**
* This function makes a number of automatic choices of updates to the global state, untill `time' has passed.
*
* @param time is the length of time to pass.
* @throws PrismException
* if something goes wrong when updating the state.
* Select, at random, n successive transitions and execute them.
* For continuous-time models, the time to be spent in each state before leaving is also picked randomly.
* If a deadlock is found, the process stops.
* The function returns the number of transitions successfully taken.
*/
public void automaticTransitions(double time) throws PrismException
public int automaticTransitions(int n, boolean detect) throws PrismException
{
automaticTransitions(time, true);
int i = 0;
while (i < n) {
if (!automaticTransition(detect))
break;
i++;
}
return i;
}
/**
* This function makes n automatic choices of updates to the global state, untill `time' has passed.
*
* @param time
* is the length of time to pass.
* @param detect
* whether to employ loop detection.
* @throws PrismException
* if something goes wrong when updating the state.
* Randomly select and execute transitions until the specified time delay is first exceeded.
* (Time is measured from the initial execution of this method, not total time.)
* (For discrete-time models, this just results in ceil(time) steps being executed.)
* If a deadlock is found, the process stops.
* The function returns the number of transitions successfully taken.
*/
public void automaticTransitions(double time, boolean detect) throws PrismException
public int automaticTransitions(double time, boolean detect) throws PrismException
{
// For discrete-time models, this just results in ceil(time) steps being executed.
if (!modelType.continuousTime()) {
automaticTransitions((int) Math.ceil(time), detect);
return automaticTransitions((int) Math.ceil(time), detect);
} else {
double startTime = path.getTotalTime();
double currentTime = startTime;
// Loop until delay exceed
while (currentTime - startTime < time) {
int i = 0;
double targetTime = path.getTotalTime() + time;
while (path.getTotalTime() < targetTime) {
if (automaticTransition(detect))
i++;
else
break;
// TODO
/* Break when looping. */
//if (detect && loop_detection->Is_Proven_Looping())
//break;
if (queryIsDeadlock())
/* Break when deadlocking. */
// if (loop_detection->Is_Deadlock())
break;
double probability = 0.0;
//Automatic_Update(loop_detection, probability);
// Because we cannot guarantee that we know the selected index, we have to show this.
//stored_path[current_index]->choice_made = PATH_NO_CHOICE_MADE;
//stored_path[current_index]->probability = probability;
// Unless requested not to (detect==false), this function will stop exploring when a loop is detected.
// Because Automatic_Update() checks for loops before making a transition, we overshoot.
// Hence at this point if we are looping we step back a state,
@ -487,84 +457,63 @@ public class SimulatorEngine
}*/
}
return i;
}
}
/**
* Backtrack to a particular step within the current path.
* Time point should be >=0 and <= the total path size.
* (Not applicable for on-the-fly paths)
* @param step The step to backtrack to.
*/
public void backtrack(int step) throws PrismException
public void backtrackTo(int step) throws PrismException
{
// Check step is valid
if (step < 0) {
throw new PrismException("Cannot backtrack to a negative step index");
}
if (step > path.size()) {
throw new PrismException("There is no step " + step + " to backtrack to");
}
// Back track in path
((PathFull) path).backtrack(step);
// Update previous/current state info
previousState = path.getPreviousState();
if (step == 0)
previousState.clear();
else
previousState.copy(path.getPreviousState());
currentState = path.getCurrentState();
// Recompute samplers for any loaded properties
recomputeSamplers();
// Generate updates for new current state
updater.calculateTransitions(currentState, transitionList);
/*
// if go back at least one step, escape deadlock
if (step < current_index) loop_detection->Set_Deadlock(false);
current_index = step;
//copy the state stored in this path to model_variables
stored_path[current_index]->Make_Current_State_This();
//recalculate timer and rewards
path_timer = 0.0;
for(int i = 0; i < no_reward_structs; i++) {
path_cost[i] = 0.0;
total_state_cost[i] = 0.0;
total_transition_cost[i] = 0.0;
}
for(int i = 0; i < current_index; i++)
{
if(stored_path[i]->time_known)
path_timer += stored_path[i]->time_spent_in_state;
for (int j = 0; j < no_reward_structs; j++) {
total_state_cost[j] += stored_path[i]->state_cost[j];
total_transition_cost[j] += stored_path[i]->transition_cost[j];
}
}
for (int j = 0; j < no_reward_structs; j++) {
path_cost[j] = total_state_cost[j] + total_transition_cost[j];
}
Recalculate_Path_Formulae();
Calculate_State_Reward(state_variables);
Calculate_Updates(state_variables);
loop_detection->Backtrack(step);
*/
}
/**
* This function backtracks the current path to such that the cumulative time is equal or less than the time
* parameter.
*
* @param time
* the cumulative time to backtrack to.
* @throws PrismException
* is something goes wrong when backtracking.
* Backtrack to a particular (continuous) time point within the current path.
* Time point should be >=0 and <= the total path time.
* (Not applicable for on-the-fly paths)
* @param time The amount of time to backtrack.
*/
public void backtrack(double time) throws PrismException
public void backtrackTo(double time) throws PrismException
{
// Backtrack(time) in simpath.cc
//doBacktrack(time);
// Check step is valid
if (time < 0) {
throw new PrismException("Cannot backtrack to a negative time point");
}
if (time > path.getTotalTime()) {
throw new PrismException("There is no time point " + time + " to backtrack to");
}
int step, n;
PathFull pathFull = (PathFull) path;
n = path.size();
// Find the index of the step we are in at that point
// i.e. the first state whose cumulative time on entering exceeds 'time'
for (step = 0; step <= n && pathFull.getCumulativeTime(step) < time; step++)
;
// Then backtrack to this step
backtrackTo(step);
}
/**
@ -1059,7 +1008,7 @@ public class SimulatorEngine
{
return path.getTotalCumulativeReward(rsi);
}
// ------------------------------------------------------------------------------
// Querying of current path (full paths only)
// ------------------------------------------------------------------------------
@ -1194,7 +1143,6 @@ public class SimulatorEngine
*/
public static native int loopEnd();
/**
* Export the current path to a file in a simple space separated format.
* (Not applicable for on-the-fly paths)
@ -1233,14 +1181,77 @@ public class SimulatorEngine
}
// ------------------------------------------------------------------------------
// PROPERTIES AND SAMPLING (not yet sorted)
// Model checking (approximate)
// ------------------------------------------------------------------------------
// PCTL Stuff
/**
* Check whether a property is suitable for approximate model checking using the simulator.
* If not, an explanatory error message is thrown as an exception.
*/
public void checkPropertyForSimulation(Expression prop) throws PrismException
{
// Simulator can only be applied to P=? or R=? properties
boolean ok = true;
Expression expr = null;
if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward))
ok = false;
else if (prop instanceof ExpressionProb) {
if ((((ExpressionProb) prop).getProb() != null))
ok = false;
expr = ((ExpressionProb) prop).getExpression();
} else if (prop instanceof ExpressionReward) {
if ((((ExpressionReward) prop).getReward() != null))
ok = false;
expr = ((ExpressionReward) prop).getExpression();
}
if (!ok)
throw new PrismException("Simulator can only handle P=? or R=? properties");
// Check that there are no nested probabilistic operators
try {
expr.accept(new ASTTraverse()
{
public void visitPre(ExpressionProb e) throws PrismLangException
{
throw new PrismLangException("");
}
public void visitPre(ExpressionReward e) throws PrismLangException
{
throw new PrismLangException("");
}
public void visitPre(ExpressionSS e) throws PrismLangException
{
throw new PrismLangException("");
}
});
} catch (PrismLangException e) {
throw new PrismException("Simulator cannot handle nested P, R or S operators");
}
}
// Methods to compute parameters for simulation
public double computeSimulationApproximation(double confid, int numSamples)
{
return Math.sqrt((4.0 * PrismUtils.log(2.0 / confid, 10)) / numSamples);
}
public double computeSimulationConfidence(double approx, int numSamples)
{
return 2.0 / Math.pow(10, (numSamples * approx * approx) / 4.0);
}
public int computeSimulationNumSamples(double approx, double confid)
{
return (int) Math.ceil(4.0 * PrismUtils.log(2.0 / confid, 10) / (approx * approx));
}
/**
* This method completely encapsulates the model checking of a property so long as: prerequisites modulesFile
* constants should all be defined propertiesFile constants should all be defined
* Perform approximate model checking for a single property.
* Note: All constants in the model must have already been defined.
* @param modulesFile Model for simulation
*
* <P>
* The returned result is:
@ -1248,8 +1259,6 @@ public class SimulatorEngine
* <LI> A Double object: for =?[] properties
* </UL>
*
* @param modulesFile
* The ModulesFile, constants already defined.
* @param propertiesFile
* The PropertiesFile containing the property of interest, constants defined.
* @param expr
@ -1264,7 +1273,7 @@ public class SimulatorEngine
* if anything goes wrong.
* @return the result.
*/
public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, Values initialState, int noIterations,
public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int numIters,
int maxPathLength) throws PrismException
{
ArrayList exprs;
@ -1272,7 +1281,7 @@ public class SimulatorEngine
exprs = new ArrayList();
exprs.add(expr);
res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations, maxPathLength);
res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, numIters, maxPathLength);
if (res[0] instanceof PrismException)
throw (PrismException) res[0];
@ -1282,25 +1291,17 @@ public class SimulatorEngine
/**
* Perform approximate model checking of properties 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 exprs The properties to check
* @param initialState
* The initial state for the sampling.
* @param noIterations The number of iterations (i.e. number of samples to generate)
* @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
*
* <P>
* The returned result is an array each item of which is either:
* <UL>
* <LI> Double object: for =?[] properties
* <LI> An exception if there was a problem
* </UL>
*
*/
public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, Values initialState,
int noIterations, int maxPathLength) throws PrismException
public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, State initialState,
int numIters, int maxPathLength) throws PrismException
{
createNewOnTheFlyPath(modulesFile);
@ -1311,7 +1312,7 @@ public class SimulatorEngine
int validPropsCount = 0;
for (int i = 0; i < exprs.size(); i++) {
try {
checkPropertyForSimulation((Expression) exprs.get(i), modulesFile.getModelType());
checkPropertyForSimulation((Expression) exprs.get(i));
indices[i] = addProperty((Expression) exprs.get(i), propertiesFile);
if (indices[i] >= 0)
validPropsCount++;
@ -1323,7 +1324,7 @@ public class SimulatorEngine
// as long as there are at least some valid props, do sampling
if (validPropsCount > 0) {
doSampling(new State(initialState), noIterations, maxPathLength);
doSampling(initialState, numIters, maxPathLength);
}
// process the results
@ -1396,7 +1397,7 @@ public class SimulatorEngine
pfcs[i] = definedPFConstants;
propertiesFile.setUndefinedConstants(definedPFConstants);
try {
checkPropertyForSimulation(propertyToCheck, modulesFile.getModelType());
checkPropertyForSimulation(propertyToCheck);
indices[i] = addProperty(propertyToCheck, propertiesFile);
if (indices[i] >= 0)
validPropsCount++;
@ -1473,7 +1474,7 @@ public class SimulatorEngine
//is all handled by the All_Done_Sampling() function
// Main sampling loop
while (!should_stop_sampling && !isSamplingDone() && iters < numIters) {
while (!should_stop_sampling && iters < numIters) {
// Display progress
percentageDone = ((10 * (iters)) / numIters) * 10;
@ -1605,148 +1606,10 @@ public class SimulatorEngine
}
}
private boolean isSamplingDone()
{
// TODO
return false;
}
private static native double getSamplingResult(int propertyIndex);
private static native int getNumReachedMaxPath(int propertyIndex);
/**
* TODO
* Used to halt the sampling algorithm in its tracks.
*/
public static native void stopSampling();
// Methods to compute parameters for simulation
public double computeSimulationApproximation(double confid, int numSamples)
{
return Math.sqrt((4.0 * log(10, 2.0 / confid)) / numSamples);
}
public double computeSimulationConfidence(double approx, int numSamples)
{
return 2.0 / Math.pow(10, (numSamples * approx * approx) / 4.0);
}
public int computeSimulationNumSamples(double approx, double confid)
{
return (int) Math.ceil(4.0 * log(10, 2.0 / confid) / (approx * approx));
}
public static double log(double base, double x)
{
return Math.log(x) / Math.log(base);
}
// Method to check if a property is suitable for simulation
// If not, throws an exception with the reason
public void checkPropertyForSimulation(Expression prop, ModelType modelType) throws PrismException
{
// Check general validity of property
try {
prop.checkValid(modelType);
} catch (PrismLangException e) {
throw new PrismException(e.getMessage());
}
// Simulator can only be applied to P=? or R=? properties
boolean ok = true;
Expression expr = null;
if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward))
ok = false;
else if (prop instanceof ExpressionProb) {
if ((((ExpressionProb) prop).getProb() != null))
ok = false;
expr = ((ExpressionProb) prop).getExpression();
} else if (prop instanceof ExpressionReward) {
if ((((ExpressionReward) prop).getReward() != null))
ok = false;
expr = ((ExpressionReward) prop).getExpression();
}
if (!ok)
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 {
expr.accept(new ASTTraverse()
{
public void visitPre(ExpressionProb e) throws PrismLangException
{
throw new PrismLangException("");
}
public void visitPre(ExpressionReward e) throws PrismLangException
{
throw new PrismLangException("");
}
public void visitPre(ExpressionSS e) throws PrismLangException
{
throw new PrismLangException("");
}
});
} catch (PrismLangException e) {
throw new PrismException("Simulator cannot handle nested P, R or S operators");
}
}
// ------------------------------------------------------------------------------
// UTILITY METHODS
// These are for debugging purposes only
// ------------------------------------------------------------------------------
/**
* Convienience method to print an expression at a given pointer location
*
* @param exprPointer
* the expression pointer.
*/
public static native void printExpression(long exprPointer);
/**
* Returns a string representation of the expression at the given pointer location.
*
* @param exprPointer
* the pointer location of the expression.
* @return a string representation of the expression at the given pointer location.
*/
public static native String expressionToString(long exprPointer);
/**
* Returns a string representation of the loaded simulator engine model.
*
* @return a string representation of the loaded simulator engine model.
*/
public static native String modelToString();
/**
* Returns a string representation of the stored path.
*
* @return a string representation of the stored path.
*/
public static native String pathToString();
/**
* Prints the current update set to the command line.
*/
public static native void printCurrentUpdates();
// ------------------------------------------------------------------------------
// ERROR HANDLING
// ------------------------------------------------------------------------------
/**
* If any native method has had a problem, it should have passed a message to the error handler. This method returns
* that message.
*
* @return returns the last c++ error message.
*/
public static native String getLastErrorMessage();
}
// ==================================================================================

4
prism/src/userinterface/properties/GUIMultiProperties.java
View File

@ -271,7 +271,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
GUIProperty guiP = (GUIProperty)validGUIProperties.get(i);
try
{
getPrism().checkPropertyForSimulation(guiP.getProperty(), parsedModel.getModelType());
getPrism().checkPropertyForSimulation(guiP.getProperty());
simulatableGUIProperties.add(guiP);
}
catch(PrismException e)
@ -387,7 +387,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
{
try
{
getPrism().checkPropertyForSimulation(gp.getProperty(), parsedModel.getModelType());
getPrism().checkPropertyForSimulation(gp.getProperty());
}
catch(PrismException e)
{

6
prism/src/userinterface/simulator/GUISimulator.java
View File

@ -489,7 +489,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
try {
setComputing(true);
engine.backtrack(time);
engine.backtrackTo(time);
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
@ -511,7 +511,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
try {
setComputing(true);
engine.backtrack(step);
engine.backtrackTo(step);
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
@ -532,7 +532,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
try {
setComputing(true);
// Instruct simulator to go back to step 0
engine.backtrack(0);
engine.backtrackTo(0);
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();

Write Preview
Loading…
Cancel
Save