= actionNames.length) return "[]";
- else return "[" +actionNames[actionIndex] + "]";
+ if (actionIndex < 0 || actionIndex >= actionNames.length)
+ return "[]";
+ else
+ return "[" + actionNames[actionIndex] + "]";
}
-
+
/**
- * Asks the c++ engine for the index of the action of the
- * current update at the given index.
+ * Asks the c++ engine for the index of the action of the current update at the given index.
*/
private static native int getActionIndexOfUpdate(int i);
-
+
/**
- * Returns the module name of the udpate at the given
- * index.
- * @param i the index of the update of interest.
- * @return the module name of the udpate at the given
- * index.
+ * Returns the module name of the udpate at the given index.
+ *
+ * @param i
+ * the index of the update of interest.
+ * @return the module name of the udpate at the given index.
*/
public String getModuleNameOfUpdate(int i)
{
int moduleIndex = getModuleIndexOfUpdate(i);
- if(moduleIndex < 0 || moduleIndex >= moduleNames.length) return "";
- else return moduleNames[moduleIndex];
+ if (moduleIndex < 0 || moduleIndex >= moduleNames.length)
+ return "";
+ else
+ return moduleNames[moduleIndex];
}
-
+
/**
- * Asks the c++ engine for the index of the module of the
- * current update at the given index
- * @param i the index of the update of interest.
- * @return the index of the module of the
- * current update at the given index
+ * Asks the c++ engine for the index of the module of the current update at the given index
+ *
+ * @param i
+ * the index of the update of interest.
+ * @return the index of the module of the current update at the given index
*/
public static native int getModuleIndexOfUpdate(int i);
-
+
/**
* Returns the probability/rate of the update at the given index
- * @param i the index of the update of interest.
+ *
+ * @param i
+ * the index of the update of interest.
* @return the probability/rate of the update at the given index.
*/
public static native double getProbabilityOfUpdate(int i);
-
+
/**
- * Returns a string representation of the assignments for the current
- * update at the given index.
- * @param index the index of the update of interest.
- * @return a string representation of the assignments for the current
- * update at the given index.
+ * Returns a string representation of the assignments for the current update at the given index.
+ *
+ * @param index
+ * the index of the update of interest.
+ * @return a string representation of the assignments for the current update at the given index.
*/
public String getAssignmentDescriptionOfUpdate(int index)
{
String assignment = "";
int numAssigns = getNumAssignmentsOfUpdate(index);
-
-
-
- //System.out.println("getAssignmentDesctipyionOfCurrentUpdate" + index);
- for(int i = 0; i < numAssigns; i++)
- {
+
+ // System.out.println("getAssignmentDesctipyionOfCurrentUpdate" + index);
+ for (int i = 0; i < numAssigns; i++) {
int var = getAssignmentVariableIndexOfUpdate(index, i);
int value = getAssignmentValueOfUpdate(index, i);
-
- if(var < 0 || var >= varNames.length) return "";
+
+ if (var < 0 || var >= varNames.length)
+ return "";
String varName = varNames[var];
- if(varTypes[var] == Expression.BOOLEAN)
- if(value == 0)
+ if (varTypes[var] == Expression.BOOLEAN)
+ if (value == 0)
assignment += varName + "\'=false";
else
assignment += varName + "\'=true";
else
assignment += varName + "\'=" + value;
-
- if(i != numAssigns-1) assignment+=", ";
+
+ if (i != numAssigns - 1)
+ assignment += ", ";
}
return assignment;
}
-
+
/**
- * Returns the number of assignments for the current update at the
- * given index.
+ * Returns the number of assignments for the current update at the given index.
*/
private static native int getNumAssignmentsOfUpdate(int i);
-
+
/**
- * Returns the index of the variable being assigned to for the
- * current update at the given index (updateIndex) and for its
- * assignment indexed assignmentIndex
+ * Returns the index of the variable being assigned to for the current update at the given index (updateIndex) and
+ * for its assignment indexed assignmentIndex
*/
private static native int getAssignmentVariableIndexOfUpdate(int updateIndex, int assignmentIndex);
-
+
/**
- * Returns the value of the assignment for the current update at
- * the given index (updateIndex and for its assignment indexed
- * assignmentIndex.
+ * Returns the value of the assignment for the current update at the given index (updateIndex and for its assignment
+ * indexed assignmentIndex.
*/
private static native int getAssignmentValueOfUpdate(int updateIndex, int assignmentIndex);
-
+
/**
- * For mdps, updates can belong to different probability distributions. These
- * probability distributions are indexed. This returns the probability
- * distribution that the indexed update belongs to.
- * @param updateIndex the index of the update of interest.
- * @return the probability
- * distribution that the indexed update belongs to.
+ * For mdps, updates can belong to different probability distributions. These probability distributions are indexed.
+ * This returns the probability distribution that the indexed update belongs to.
+ *
+ * @param updateIndex
+ * the index of the update of interest.
+ * @return the probability distribution that the indexed update belongs to.
*/
public static native int getDistributionIndexOfUpdate(int updateIndex);
-
-
- //------------------------------------------------------------------------------
- // PROPERTIES AND SAMPLING (not yet sorted)
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // PROPERTIES AND SAMPLING (not yet sorted)
+ // ------------------------------------------------------------------------------
+
/**
- * Allocate space for storage of PCTL Formulae
+ * Allocate space for storage of PCTL Formulae
*/
private static native int allocatePCTLManager();
-
+
/**
- * Allocate space for storage of sampling information
+ * Allocate space for storage of sampling information
*/
private static native int allocateSampling();
-
+
/**
* Provides access to the propertyConstants
+ *
* @return the propertyConstants
*/
public Values getPropertyConstants()
{
- if(propertyConstants == null)
- {
+ if (propertyConstants == null) {
propertyConstants = new Values();
}
return propertyConstants;
}
-
+
/**
* Convenience method performing various things done before sampling
- */
+ */
private void setupForSampling(ModulesFile modulesFile, PropertiesFile propertiesFile) throws SimulatorException
{
int resultError;
-
+
deallocateEngine();
-
+
loadModulesFile(modulesFile, modulesFile.getConstantValues());
-
+
propertyConstants = propertiesFile.getConstantValues();
this.propertiesFile = propertiesFile;
-
+
resultError = allocatePCTLManager();
- if(resultError == ERROR)
- {
+ if (resultError == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
resultError = allocateSampling();
- if(resultError == ERROR)
- {
+ if (resultError == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
}
-
+
/**
* Gets (double) result from simulator for a given property/index and process result
- */
+ */
private Object processSamplingResult(Expression expr, int index)
{
- if(index == -1)
- {
+ if (index == -1) {
return new SimulatorException("Property cannot be handled by the PRISM simulator");
- }
- else
- {
+ } else {
double result = getSamplingResult(index);
- if(result == UNDEFINED_DOUBLE) result = Double.POSITIVE_INFINITY;
- // only handle P=?/R=? properties (we could check against the bounds in P>p etc. but results would be a bit dubious)
+ if (result == UNDEFINED_DOUBLE)
+ result = Double.POSITIVE_INFINITY;
+ // only handle P=?/R=? properties (we could check against the bounds in P>p etc. but results would be a bit
+ // dubious)
if (expr instanceof ExpressionProb) {
- if (((ExpressionProb)expr).getProb() == null) {
+ if (((ExpressionProb) expr).getProb() == null) {
return new Double(result);
} else {
return new SimulatorException("Property cannot be handled by the PRISM simulator");
}
} else if (expr instanceof ExpressionReward) {
- if (((ExpressionReward)expr).getReward() == null) {
+ if (((ExpressionReward) expr).getReward() == null) {
return new Double(result);
} else {
return new SimulatorException("Property cannot be handled by the PRISM simulator");
}
- }
- else {
+ } else {
return new SimulatorException("Property cannot be handled by the PRISM simulator");
}
}
}
-
- //PCTL Stuff
-
+
+ // PCTL Stuff
+
public static native int exportBinary(String filename);
-
- public void exportBinaryForSingleProperty(
- ModulesFile modulesFile,
- PropertiesFile propertiesFile,
- Expression expr,
- Values initialState,
- String filename
- ) throws SimulatorException
+
+ public void exportBinaryForSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr,
+ Values initialState, String filename) throws SimulatorException
{
setupForSampling(modulesFile, propertiesFile);
-
+
int index = addProperty(expr);
-
- if(index == -1)
+
+ if (index == -1)
throw new SimulatorException("Property cannot be handled by the PRISM simulator");
-
+
loadInitialState(initialState);
-
+
int resultError = exportBinary(filename);
-
- if(resultError == ERROR)
- {
+
+ if (resultError == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
-
+
deallocateEngine();
}
-
- public void exportBinaryForMultipleProperties(
- ModulesFile modulesFile,
- PropertiesFile propertiesFile,
- ArrayList exprs,
- Values initialState,
- String filename
- ) throws SimulatorException
+
+ public void exportBinaryForMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile,
+ ArrayList exprs, Values initialState, String filename) throws SimulatorException
{
setupForSampling(modulesFile, propertiesFile);
-
+
int[] indices = addProperties(exprs);
-
+
boolean existsOne = false;
- for(int i = 0; i < indices.length; i++)
- {
- if(indices[i]>=0)
- {
+ for (int i = 0; i < indices.length; i++) {
+ if (indices[i] >= 0) {
existsOne = true;
break;
}
}
- if(!existsOne)
+ if (!existsOne)
throw new SimulatorException("None of the selected properties can be handled by the PRISM simulator");
-
+
loadInitialState(initialState);
-
+
int resultError = exportBinary(filename);
-
- if(resultError == ERROR)
- {
+
+ if (resultError == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
-
+
deallocateEngine();
}
-
-
- /**
- * Returns an ArrayList of Values objects for the each propery iteration
- */
- public ArrayList exportBinaryForExperiment(
- userinterface.properties.GUIExperiment exp,
- java.lang.Thread experimentThread,
- ModulesFile modulesFile,
- PropertiesFile propertiesFile,
- UndefinedConstants undefinedConstants,
- Expression propertyToCheck,
- Values initialState,
- String filename
- ) throws PrismException, InterruptedException, SimulatorException
+
+ /**
+ * Returns an ArrayList of Values objects for the each propery iteration
+ */
+ public ArrayList exportBinaryForExperiment(userinterface.properties.GUIExperiment exp,
+ java.lang.Thread experimentThread, ModulesFile modulesFile, PropertiesFile propertiesFile,
+ UndefinedConstants undefinedConstants, Expression propertyToCheck, Values initialState, String filename)
+ throws PrismException, InterruptedException, SimulatorException
{
setupForSampling(modulesFile, propertiesFile);
-
+
ArrayList definedPFConstantsCollection = new ArrayList();
Values definedPFConstants = new Values();
-
- int[]indices = new int[undefinedConstants.getNumPropertyIterations()];
- int[]types = new int[undefinedConstants.getNumPropertyIterations()];
-
- for(int i = 0; i < undefinedConstants.getNumPropertyIterations(); i++)
- {
- if (propertiesFile != null)
- {
+
+ int[] indices = new int[undefinedConstants.getNumPropertyIterations()];
+ int[] types = new int[undefinedConstants.getNumPropertyIterations()];
+
+ for (int i = 0; i < undefinedConstants.getNumPropertyIterations(); i++) {
+ if (propertiesFile != null) {
definedPFConstants = undefinedConstants.getPFConstantValues();
definedPFConstantsCollection.add(definedPFConstants);
propertiesFile.setUndefinedConstants(definedPFConstants);
-
+
propertyConstants = propertiesFile.getConstantValues();
}
indices[i] = addProperty(propertyToCheck);
types[i] = propertyToCheck.getType();
-
+
undefinedConstants.iterateProperty();
}
-
+
loadInitialState(initialState);
-
+
int resultError = exportBinary(filename);
-
- if(resultError == ERROR)
- {
+
+ if (resultError == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
-
+
deallocateEngine();
-
+
return definedPFConstantsCollection;
}
-
- /**
- * 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
- *
- * The returned result is:
+
+ /**
+ * 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
+ *
+ *
+ * The returned result is:
*
- * - A Double object: for =?[] properties
+ *
- A Double object: for =?[] properties
*
- * @param modulesFile The ModulesFile, constants already defined.
- * @param propertiesFile The PropertiesFile containing the property of interest, constants defined.
- * @param expr The property of interest
- * @param initialState The initial state for the sampling.
- * @param noIterations The number of iterations for the sampling algorithm
- * @param maxPathLength the maximum path length for the sampling algorithm.
- * @throws SimulatorException if anything goes wrong.
+ *
+ * @param modulesFile
+ * The ModulesFile, constants already defined.
+ * @param propertiesFile
+ * The PropertiesFile containing the property of interest, constants defined.
+ * @param expr
+ * The property of interest
+ * @param initialState
+ * The initial state for the sampling.
+ * @param noIterations
+ * The number of iterations for the sampling algorithm
+ * @param maxPathLength
+ * the maximum path length for the sampling algorithm.
+ * @throws SimulatorException
+ * if anything goes wrong.
* @return the result.
*/
- public Object modelCheckSingleProperty(
- ModulesFile modulesFile,
- PropertiesFile propertiesFile,
- Expression expr,
- Values initialState,
- int noIterations,
- int maxPathLength
- ) throws SimulatorException
+ public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr,
+ Values initialState, int noIterations, int maxPathLength) throws SimulatorException
{
ArrayList exprs;
Object res[];
-
+
exprs = new ArrayList();
exprs.add(expr);
- res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations, maxPathLength);
-
- if (res[0] instanceof SimulatorException) throw (SimulatorException)res[0]; else return res[0];
+ res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations,
+ maxPathLength);
+
+ if (res[0] instanceof SimulatorException)
+ throw (SimulatorException) res[0];
+ else
+ return res[0];
}
-
+
/**
- * This method completely encapsulates the model checking of multiple properties
- * prerequisites modulesFile constants should all be defined
- * propertiesFile constants should all be defined
- *
- * The returned result is an array each item of which is either:
+ * This method completely encapsulates the model checking of multiple properties prerequisites modulesFile constants
+ * should all be defined propertiesFile constants should all be defined
+ *
+ *
+ * The returned result is an array each item of which is either:
*
- * - Double object: for =?[] properties
- *
- An exception if there was a problem
+ *
- Double object: for =?[] properties
+ *
- An exception if there was a problem
*
- * @param modulesFile The ModulesFile, constants already defined.
- * @param propertiesFile The PropertiesFile containing the property of interest, constants defined.
- * @param exprs The properties of interest
- * @param initialState The initial state for the sampling.
- * @param noIterations The number of iterations for the sampling algorithm
- * @param maxPathLength the maximum path length for the sampling algorithm.
- * @throws SimulatorException if anything goes wrong.
+ *
+ * @param modulesFile
+ * The ModulesFile, constants already defined.
+ * @param propertiesFile
+ * The PropertiesFile containing the property of interest, constants defined.
+ * @param exprs
+ * The properties of interest
+ * @param initialState
+ * The initial state for the sampling.
+ * @param noIterations
+ * The number of iterations for the sampling algorithm
+ * @param maxPathLength
+ * the maximum path length for the sampling algorithm.
+ * @throws SimulatorException
+ * if anything goes wrong.
* @return the result.
*/
- public Object[] modelCheckMultipleProperties(
- ModulesFile modulesFile,
- PropertiesFile propertiesFile,
- ArrayList exprs,
- Values initialState,
- int noIterations,
- int maxPathLength
- ) throws SimulatorException
+ public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile,
+ ArrayList exprs, Values initialState, int noIterations, int maxPathLength) throws SimulatorException
{
setupForSampling(modulesFile, propertiesFile);
-
+
Object[] results = new Object[exprs.size()];
int[] indices = new int[exprs.size()];
-
+
// Add the properties to the simulator (after a check that they are valid)
int validPropsCount = 0;
- for(int i = 0; i < exprs.size(); i++) {
+ for (int i = 0; i < exprs.size(); i++) {
try {
- checkPropertyForSimulation((Expression)exprs.get(i), modulesFile.getType());
- indices[i] = addProperty((Expression)exprs.get(i));
- if (indices[i] >= 0) validPropsCount++;
- }
- catch (SimulatorException e) {
+ checkPropertyForSimulation((Expression) exprs.get(i), modulesFile.getType());
+ indices[i] = addProperty((Expression) exprs.get(i));
+ if (indices[i] >= 0)
+ validPropsCount++;
+ } catch (SimulatorException e) {
results[i] = e;
indices[i] = -1;
}
}
-
+
// as long as there are at least some valid props, do sampling
- if(validPropsCount > 0) {
+ if (validPropsCount > 0) {
loadInitialState(initialState);
int result = doSampling(noIterations, maxPathLength);
- if(result == ERROR)
- {
+ if (result == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
}
-
+
// process the results
- for(int i = 0; i < results.length; i++)
- {
+ 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 SimulatorException))
- results[i] = processSamplingResult((Expression)exprs.get(i), indices[i]);
+ results[i] = processSamplingResult((Expression) exprs.get(i), indices[i]);
}
-
+
deallocateEngine();
-
+
// display results to log
if (results.length == 1) {
- if (!(results[0] instanceof SimulatorException)) mainLog.println("\nResult: " + results[0]);
- }
- else {
+ if (!(results[0] instanceof SimulatorException))
+ mainLog.println("\nResult: " + results[0]);
+ } else {
mainLog.println("\nResults:");
- for(int i = 0; i < results.length; i++) mainLog.println(exprs.get(i) + " : " + results[i]);
+ for (int i = 0; i < results.length; i++)
+ mainLog.println(exprs.get(i) + " : " + results[i]);
}
-
+
return results;
}
-
- /**
- * Deals with all of the logistics
- * of performing an experiment and storing the results in an
- * appropriate ResultsCollection object.
- * @param exp the experiment in which to store the results.
- * @param modulesFile The ModulesFile, constants already defined.
- * @param propertiesFile The PropertiesFile containing the property of interest, constants defined.
- * @param undefinedConstants defining what should be done for the experiment
- * @param resultsCollection where the results should be stored
- * @param propertyToCheck the property to check for the experiment
- * @param initialState The initial state for the sampling.
- * @param maxPathLength the maximum path length for the sampling algorithm.
- * @param noIterations The number of iterations for the sampling algorithm
- * @throws PrismException if something goes wrong with the results reporting
- * @throws InterruptedException if the thread is interrupted
- * @throws SimulatorException 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, SimulatorException
+
+ /**
+ * Deals with all of the logistics of performing an experiment and storing the results in an appropriate
+ * ResultsCollection object.
+ *
+ * @param exp
+ * the experiment in which to store the results.
+ * @param modulesFile
+ * The ModulesFile, constants already defined.
+ * @param propertiesFile
+ * The PropertiesFile containing the property of interest, constants defined.
+ * @param undefinedConstants
+ * defining what should be done for the experiment
+ * @param resultsCollection
+ * where the results should be stored
+ * @param propertyToCheck
+ * the property to check for the experiment
+ * @param initialState
+ * The initial state for the sampling.
+ * @param maxPathLength
+ * the maximum path length for the sampling algorithm.
+ * @param noIterations
+ * The number of iterations for the sampling algorithm
+ * @throws PrismException
+ * if something goes wrong with the results reporting
+ * @throws InterruptedException
+ * if the thread is interrupted
+ * @throws SimulatorException
+ * 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,
+ SimulatorException
{
int n;
Values definedPFConstants = new Values();
-
+
setupForSampling(modulesFile, propertiesFile);
-
+
n = undefinedConstants.getNumPropertyIterations();
Object[] results = new Object[n];
Values[] pfcs = new Values[n];
int[] indices = new int[n];
-
+
// Add the properties to the simulator (after a check that they are valid)
int validPropsCount = 0;
- for(int i = 0; i < n; i++) {
+ for (int i = 0; i < n; i++) {
definedPFConstants = undefinedConstants.getPFConstantValues();
pfcs[i] = definedPFConstants;
propertiesFile.setUndefinedConstants(definedPFConstants);
@@ -1842,56 +1815,62 @@ public class SimulatorEngine
try {
checkPropertyForSimulation(propertyToCheck, modulesFile.getType());
indices[i] = addProperty(propertyToCheck);
- if (indices[i] >= 0) validPropsCount++;
- }
- catch (SimulatorException e) {
+ if (indices[i] >= 0)
+ validPropsCount++;
+ } catch (SimulatorException e) {
results[i] = e;
indices[i] = -1;
}
undefinedConstants.iterateProperty();
}
-
+
// as long as there are at least some valid props, do sampling
- if(validPropsCount > 0) {
+ if (validPropsCount > 0) {
loadInitialState(initialState);
int result = doSampling(noIterations, maxPathLength);
- if(result == ERROR)
- {
+ if (result == ERROR) {
throw new SimulatorException(getLastErrorMessage());
}
}
-
+
// process the results
- for(int i = 0; i < n; i++)
- {
+ for (int i = 0; i < n; i++) {
// if we have already stored an error for this property, keep it as the result, otherwise process
if (!(results[i] instanceof Exception))
results[i] = processSamplingResult(propertyToCheck, indices[i]);
// store it in the ResultsCollection
resultsCollection.setResult(undefinedConstants.getMFConstantValues(), pfcs[i], results[i]);
}
-
+
deallocateEngine();
-
+
// display results to log
if (indices.length == 1) {
- if (!(results[0] instanceof Exception)) mainLog.println("\nResult: " + results[0]);
- }
- else {
+ if (!(results[0] instanceof Exception))
+ 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));
}
}
/**
* Generate a random path with the simulator
- * @param modulesFile The ModulesFile, constants already defined
- * @param initialState The first state of the path
- * @param details Information about the path to be generated
- * @param file The file to output the path to (stdout if null)
- * @throws SimulatorException if something goes wrong
- */
- public void generateSimulationPath(ModulesFile modulesFile, Values initialState, String details, int maxPathLength, File file) throws SimulatorException, PrismException
+ *
+ * @param modulesFile
+ * The ModulesFile, constants already defined
+ * @param initialState
+ * The first state of the path
+ * @param details
+ * Information about the path to be generated
+ * @param file
+ * The file to output the path to (stdout if null)
+ * @throws SimulatorException
+ * if something goes wrong
+ */
+ public void generateSimulationPath(ModulesFile modulesFile, Values initialState, String details, int maxPathLength,
+ File file) throws SimulatorException, PrismException
{
String s, ss[];
int i, j, n;
@@ -1899,14 +1878,14 @@ public class SimulatorEngine
boolean done;
boolean stochastic = (modulesFile.getType() == ModulesFile.STOCHASTIC);
int simPathType = -1;
- int simPathLength = 0 ;
- double simPathTime = 0.0 ;
+ int simPathLength = 0;
+ double simPathTime = 0.0;
String simPathSep = " ";
ArrayList simVars = null;
VarList varList;
boolean simLoopCheck = true;
int simPathRepeat = 1;
-
+
// parse details
ss = details.split(",");
n = ss.length;
@@ -1916,24 +1895,31 @@ public class SimulatorEngine
simPathType = SIM_PATH_TIME;
try {
simPathTime = Double.parseDouble(ss[i].substring(5));
- if (simPathTime < 0.0) throw new NumberFormatException();
+ if (simPathTime < 0.0)
+ throw new NumberFormatException();
} catch (NumberFormatException e) {
- throw new SimulatorException("Invalid path time limit \""+ss[i]+"\"");
+ throw new SimulatorException("Invalid path time limit \"" + ss[i] + "\"");
}
- }
- else if (ss[i].equals("deadlock")) {
+ } else if (ss[i].equals("deadlock")) {
// path until deadlock
simPathType = SIM_PATH_DEADLOCK;
- }
- else if (ss[i].indexOf("sep=") == 0) {
+ } else if (ss[i].indexOf("sep=") == 0) {
// specify column separator to display path
simPathSep = ss[i].substring(4);
- if (simPathSep.equals("space")) { simPathSep = " "; continue; }
- if (simPathSep.equals("tab")) { simPathSep = "\t"; continue; }
- if (simPathSep.equals("comma")) { simPathSep = ","; continue; }
+ if (simPathSep.equals("space")) {
+ simPathSep = " ";
+ continue;
+ }
+ if (simPathSep.equals("tab")) {
+ simPathSep = "\t";
+ continue;
+ }
+ if (simPathSep.equals("comma")) {
+ simPathSep = ",";
+ continue;
+ }
throw new SimulatorException("Separator must be one of: \"space\", \"tab\", \"comma\"");
- }
- else if (ss[i].indexOf("vars=") == 0) {
+ } else if (ss[i].indexOf("vars=") == 0) {
// specify which variables to display
varList = modulesFile.createVarList();
simVars = new ArrayList();
@@ -1942,112 +1928,154 @@ public class SimulatorEngine
if (s.length() < 1 || s.charAt(0) != '(')
throw new SimulatorException("Invalid format for \"vars=(...)\"");
s = s.substring(1);
- if (s.indexOf(')')>-1) { s = s.substring(0, s.length()-1); done = true; }
+ if (s.indexOf(')') > -1) {
+ s = s.substring(0, s.length() - 1);
+ done = true;
+ }
j = varList.getIndex(s);
- if (j == -1) throw new SimulatorException("Unknown variable \""+s+"\" in \"vars=(...)\" list");
+ if (j == -1)
+ throw new SimulatorException("Unknown variable \"" + s + "\" in \"vars=(...)\" list");
simVars.add(new Integer(j));
while (i < n && !done) {
s = ss[++i];
- if (s.indexOf(')')>-1) { s = s.substring(0, s.length()-1); done = true; }
+ if (s.indexOf(')') > -1) {
+ s = s.substring(0, s.length() - 1);
+ done = true;
+ }
j = varList.getIndex(s);
- if (j == -1) throw new SimulatorException("Unknown variable \""+s+"\" in \"vars=(...)\" list");
+ if (j == -1)
+ throw new SimulatorException("Unknown variable \"" + s + "\" in \"vars=(...)\" list");
simVars.add(new Integer(j));
}
- }
- else if (ss[i].indexOf("loopcheck=") == 0) {
+ } else if (ss[i].indexOf("loopcheck=") == 0) {
// switch loop detection on/off (default is on)
s = ss[i].substring(10);
- if (s.equals("true")) { simLoopCheck = true; continue; }
- if (s.equals("false")) { simLoopCheck = false; continue; }
+ if (s.equals("true")) {
+ simLoopCheck = true;
+ continue;
+ }
+ if (s.equals("false")) {
+ simLoopCheck = false;
+ continue;
+ }
throw new SimulatorException("Value for \"loopcheck\" flag must be \"true\" or \"false\"");
- }
- else if (ss[i].indexOf("repeat=") == 0) {
+ } else if (ss[i].indexOf("repeat=") == 0) {
// how many times to repeat path generation until successful (for "deadlock" option)
try {
simPathRepeat = Integer.parseInt(ss[i].substring(7));
- if (simPathRepeat < 1) throw new NumberFormatException();
+ if (simPathRepeat < 1)
+ throw new NumberFormatException();
} catch (NumberFormatException e) {
throw new SimulatorException("Value for \"repeat\" option must be a positive integer");
}
- }
- else {
+ } else {
// path of fixed number of steps
simPathType = SIM_PATH_NUM_STEPS;
try {
simPathLength = Integer.parseInt(ss[i]);
- if (simPathLength < 0) throw new NumberFormatException();
+ if (simPathLength < 0)
+ throw new NumberFormatException();
} catch (NumberFormatException e) {
- throw new SimulatorException("Invalid path length \""+ss[i]+"\"");
+ throw new SimulatorException("Invalid path length \"" + ss[i] + "\"");
}
}
}
- if (simPathType < 0) throw new SimulatorException("Invalid path details \""+details+"\"");
-
+ if (simPathType < 0)
+ throw new SimulatorException("Invalid path details \"" + details + "\"");
+
// print details
switch (simPathType) {
- case SIM_PATH_NUM_STEPS: mainLog.println("\nGenerating random path of length "+simPathLength+" steps..."); break;
- case SIM_PATH_TIME: mainLog.println("\nGenerating random path with time limit "+simPathTime+"..."); break;
- case SIM_PATH_DEADLOCK: mainLog.println("\nGenerating random path until deadlock state..."); break;
+ case SIM_PATH_NUM_STEPS:
+ mainLog.println("\nGenerating random path of length " + simPathLength + " steps...");
+ break;
+ case SIM_PATH_TIME:
+ mainLog.println("\nGenerating random path with time limit " + simPathTime + "...");
+ break;
+ case SIM_PATH_DEADLOCK:
+ mainLog.println("\nGenerating random path until deadlock state...");
+ break;
}
-
+
// display warning if attempt to use "repeat=" option and not "deadlock" option
if (simPathRepeat > 1 && simPathType != SIM_PATH_DEADLOCK) {
simPathRepeat = 1;
- mainLog.println("\nWarning: Ignoring \"repeat\" option - it is only valid when looking for deadlocks.");
+ mainLog.println("\nWarning: Ignoring \"repeat\" option - it is only valid when looking for deadlocks.");
}
-
+
// generate path
startNewPath(modulesFile, null, initialState);
for (j = 0; j < simPathRepeat; j++) {
- if (j > 0) restartNewPath(initialState);
+ if (j > 0)
+ restartNewPath(initialState);
i = 0;
t = 0.0;
done = false;
while (!done) {
// generate a single step of path
automaticChoices(1, simLoopCheck);
- if (stochastic) t += getTimeSpentInPathState(i++); else t = ++i;
+ if (stochastic)
+ t += getTimeSpentInPathState(i++);
+ else
+ t = ++i;
// check for termination (depending on type)
switch (simPathType) {
- case SIM_PATH_NUM_STEPS: if (i >= simPathLength) done = true; break;
- case SIM_PATH_TIME: if (t >= simPathTime || i >= maxPathLength) done = true; break;
- case SIM_PATH_DEADLOCK: if (queryIsDeadlock() == 1 || i >= maxPathLength) done = true; break;
+ case SIM_PATH_NUM_STEPS:
+ if (i >= simPathLength)
+ done = true;
+ break;
+ case SIM_PATH_TIME:
+ if (t >= simPathTime || i >= maxPathLength)
+ done = true;
+ break;
+ case SIM_PATH_DEADLOCK:
+ if (queryIsDeadlock() == 1 || i >= maxPathLength)
+ done = true;
+ break;
}
// stop if a loop was found (and loop checking was not disabled)
- if (simLoopCheck && isPathLooping()) break;
+ if (simLoopCheck && isPathLooping())
+ break;
}
-
+
// if we are generating multiple paths (to find a deadlock) only stop if deadlock actually found
- if (simPathType == SIM_PATH_DEADLOCK && queryIsDeadlock() == 1) break;
+ if (simPathType == SIM_PATH_DEADLOCK && queryIsDeadlock() == 1)
+ break;
}
- if (j < simPathRepeat) j++;
-
+ if (j < simPathRepeat)
+ j++;
+
// display warning if a deterministic loop was detected (but not in case where multiple paths generated)
if (simLoopCheck && isPathLooping() && simPathRepeat == 1) {
- mainLog.println("\nWarning: Deterministic loop detected after "+i+" steps (use loopcheck=false option to extend path).");
+ mainLog.println("\nWarning: Deterministic loop detected after " + i
+ + " steps (use loopcheck=false option to extend path).");
}
-
+
// if we needed multiple paths to find a deadlock, say how many
- if (simPathRepeat > 1 && j > 1) mainLog.println("\n"+j+" paths were generated.");
-
+ if (simPathRepeat > 1 && j > 1)
+ mainLog.println("\n" + j + " paths were generated.");
+
// export path
if (simPathType == SIM_PATH_DEADLOCK && queryIsDeadlock() != 1) {
- mainLog.print("\nNo deadlock state found within "+maxPathLength+" steps");
- if (simPathRepeat > 1) mainLog.print(" (generated "+simPathRepeat+" paths)");
+ mainLog.print("\nNo deadlock state found within " + maxPathLength + " steps");
+ if (simPathRepeat > 1)
+ mainLog.print(" (generated " + simPathRepeat + " paths)");
mainLog.println(".");
} else {
exportPath(file, true, simPathSep, simVars);
}
-
+
// warning if stopped early
if (simPathType == SIM_PATH_TIME && t < simPathTime) {
- mainLog.println("\nWarning: Path terminated before time "+simPathTime+" because maximum path length ("+maxPathLength+") reached.");
+ mainLog.println("\nWarning: Path terminated before time " + simPathTime + " because maximum path length ("
+ + maxPathLength + ") reached.");
}
}
/**
* Returns a pointer to the built reward formula
- * @param expr the ExpressionReward to be built into the engine.
+ *
+ * @param expr
+ * the ExpressionReward to be built into the engine.
* @return a pointer to the built reward formula
*/
public long addExpressionReward(ExpressionReward expr)
@@ -2059,197 +2087,204 @@ public class SimulatorEngine
double time;
Object rs = null;
int rsi = -1;
-
- if (!(expr.getPathExpression() instanceof PathExpressionTemporal)) return -1;
- pe = (PathExpressionTemporal)expr.getPathExpression();
-
+
+ if (!(expr.getPathExpression() instanceof PathExpressionTemporal))
+ return -1;
+ pe = (PathExpressionTemporal) expr.getPathExpression();
+
allConstants.addValues(getConstants());
allConstants.addValues(getPropertyConstants());
-
+
// process reward struct index
rs = expr.getRewardStructIndex();
if (rs == null) {
rsi = 0;
- }
- else if (rs instanceof Expression) {
+ } else if (rs instanceof Expression) {
try {
- rsi = ((Expression)rs).evaluateInt(allConstants, null) - 1;
- } catch(PrismException e) {
- System.err.println("Property: "+pe.toString()+" could not be used in the simulator because: \n"+ e.toString());
+ rsi = ((Expression) rs).evaluateInt(allConstants, null) - 1;
+ } catch (PrismException e) {
+ System.err.println("Property: " + pe.toString() + " could not be used in the simulator because: \n"
+ + e.toString());
return -1;
}
+ } else if (rs instanceof String) {
+ rsi = modulesFile.getRewardStructIndex((String) rs);
}
- else if (rs instanceof String) {
- rsi = modulesFile.getRewardStructIndex((String)rs);
- }
-
+
try {
switch (pe.getOperator()) {
-
+
case PathExpressionTemporal.R_C:
time = pe.getUpperBound().evaluateDouble(allConstants, null);
return loadPctlCumulative(rsi, time);
-
+
case PathExpressionTemporal.R_I:
time = pe.getUpperBound().evaluateDouble(allConstants, null);
return loadPctlInstantanious(rsi, time);
-
+
case PathExpressionTemporal.R_F:
- if (!(pe.getOperand2() instanceof PathExpressionExpr)) return -1;
+ if (!(pe.getOperand2() instanceof PathExpressionExpr))
+ return -1;
expr2 = ((PathExpressionExpr) pe.getOperand2()).getExpression();
exprPtr2 = expr2.toSimulator(this);
return loadPctlReachability(rsi, exprPtr2);
-
- default: return -1;
+
+ default:
+ return -1;
}
- }
- catch(PrismException e) {
- System.err.println("Property: "+pe.toString()+" could not be used in the simulator because: \n"+ e.toString());
+ } catch (PrismException e) {
+ System.err.println("Property: " + pe.toString() + " could not be used in the simulator because: \n"
+ + e.toString());
return -1;
}
}
-
+
/**
* Returns a pointer to the built prob formula
- * @param expr the ExpressionProb to be built into the engine.
+ *
+ * @param expr
+ * the ExpressionProb to be built into the engine.
* @return a pointer to the built prob formula
*/
public long addExpressionProb(ExpressionProb expr)
{
Values allConstants = new Values();
- PathExpressionTemporal pe;
+ PathExpressionTemporal pet;
+ PathExpression pe2;
Expression expr1, expr2;
long exprPtr1, exprPtr2;
double time1, time2;
-
- if (!(expr.getPathExpression() instanceof PathExpressionTemporal)) return -1;
- pe = (PathExpressionTemporal)expr.getPathExpression();
-
+ boolean negated = false;
+
+ if (!(expr.getPathExpression() instanceof PathExpressionTemporal))
+ return -1;
+ pet = (PathExpressionTemporal) expr.getPathExpression();
+
allConstants.addValues(getConstants());
allConstants.addValues(getPropertyConstants());
-
+
+ // Convert anything that is not until/next into until
+ if (!(pet.getOperator() == PathExpressionTemporal.P_X || pet.getOperator() == PathExpressionTemporal.P_U)) {
+ try {
+ pe2 = pet.convertToUntilForm();
+ } catch (PrismException e) {
+ return -1;
+ }
+ if (pe2 instanceof PathExpressionLogical
+ && ((PathExpressionLogical) pe2).getOperator() == PathExpressionLogical.NOT) {
+ pet = (PathExpressionTemporal) ((PathExpressionLogical) pe2).getOperand2();
+ negated = true;
+ } else {
+ pet = (PathExpressionTemporal) pe2;
+ negated = false;
+ }
+ }
+
try {
- switch (pe.getOperator()) {
-
+ switch (pet.getOperator()) {
+
case PathExpressionTemporal.P_X:
- if (!(pe.getOperand2() instanceof PathExpressionExpr)) return -1;
- expr2 = ((PathExpressionExpr) pe.getOperand2()).getExpression();
+ if (!(pet.getOperand2() instanceof PathExpressionExpr))
+ return -1;
+ expr2 = ((PathExpressionExpr) pet.getOperand2()).getExpression();
exprPtr2 = expr2.toSimulator(this);
return loadPctlNext(exprPtr2);
-
+
case PathExpressionTemporal.P_U:
- if (!(pe.getOperand1() instanceof PathExpressionExpr)) return -1;
- expr1 = ((PathExpressionExpr) pe.getOperand1()).getExpression();
+ if (!(pet.getOperand1() instanceof PathExpressionExpr))
+ return -1;
+ expr1 = ((PathExpressionExpr) pet.getOperand1()).getExpression();
exprPtr1 = expr1.toSimulator(this);
- if (!(pe.getOperand2() instanceof PathExpressionExpr)) return -1;
- expr2 = ((PathExpressionExpr) pe.getOperand2()).getExpression();
+ if (!(pet.getOperand2() instanceof PathExpressionExpr))
+ return -1;
+ expr2 = ((PathExpressionExpr) pet.getOperand2()).getExpression();
exprPtr2 = expr2.toSimulator(this);
- if (pe.hasBounds()) {
- time1 = (pe.getLowerBound() == null) ?0.0 : pe.getLowerBound().evaluateDouble(allConstants, null);
- time2 = (pe.getUpperBound() == null) ?Integer.MAX_VALUE : pe.getUpperBound().evaluateDouble(allConstants, null);
- return loadPctlBoundedUntil(exprPtr1, exprPtr2, time1, time2);
- }else {
- return loadPctlUntil(exprPtr1, exprPtr2);
+ if (pet.hasBounds()) {
+ time1 = (pet.getLowerBound() == null) ? 0.0 : pet.getLowerBound()
+ .evaluateDouble(allConstants, null);
+ time2 = (pet.getUpperBound() == null) ? Integer.MAX_VALUE : pet.getUpperBound().evaluateDouble(
+ allConstants, null);
+ if (!negated) {
+ return loadPctlBoundedUntil(exprPtr1, exprPtr2, time1, time2);
+ } else {
+ return loadPctlBoundedUntilNegated(exprPtr1, exprPtr2, time1, time2);
+ }
+ } else {
+ if (!negated) {
+ return loadPctlUntil(exprPtr1, exprPtr2);
+ } else {
+ return loadPctlUntilNegated(exprPtr1, exprPtr2);
+ }
}
- case PathExpressionTemporal.P_F:
- expr1 = Expression.True();
- exprPtr1 = expr1.toSimulator(this);
- if (!(pe.getOperand2() instanceof PathExpressionExpr)) return -1;
- expr2 = ((PathExpressionExpr) pe.getOperand2()).getExpression();
- exprPtr2 = expr2.toSimulator(this);
- if (pe.hasBounds()) {
- time1 = (pe.getLowerBound() == null) ?0.0 : pe.getLowerBound().evaluateDouble(allConstants, null);
- time2 = (pe.getUpperBound() == null) ?Integer.MAX_VALUE : pe.getUpperBound().evaluateDouble(allConstants, null);
- return loadPctlBoundedUntil(exprPtr1, exprPtr2, time1, time2);
- }else {
- return loadPctlUntil(exprPtr1, exprPtr2);
- }
-
- case PathExpressionTemporal.P_G:
- expr1 = Expression.True();
- exprPtr1 = expr1.toSimulator(this);
- if (!(pe.getOperand2() instanceof PathExpressionExpr)) return -1;
- expr2 = Expression.Not(((PathExpressionExpr) pe.getOperand2()).getExpression());
- exprPtr2 = expr2.toSimulator(this);
- if (pe.hasBounds()) {
- time1 = (pe.getLowerBound() == null) ?0.0 : pe.getLowerBound().evaluateDouble(allConstants, null);
- time2 = (pe.getUpperBound() == null) ?Integer.MAX_VALUE : pe.getUpperBound().evaluateDouble(allConstants, null);
- return loadPctlBoundedUntilNegated(exprPtr1, exprPtr2, time1, time2);
- }else {
- return loadPctlUntilNegated(exprPtr1, exprPtr2);
- }
-
- default: return -1;
+ default:
+ return -1;
}
- }
- catch(PrismException e) {
- System.err.println("Property: "+pe.toString()+" could not be used in the simulator because: \n"+ e.toString());
+ } catch (PrismException e) {
+ System.err.println("Property: " + pet.toString() + " could not be used in the simulator because: \n"
+ + e.toString());
return -1;
}
}
-
- /** Returns the index of the property, if it can be added, -1 if nots
+
+ /**
+ * Returns the index of the property, if it can be added, -1 if nots
*/
private int addProperty(Expression prop)
{
Values allConstants = new Values();
allConstants.addValues(getConstants());
allConstants.addValues(getPropertyConstants());
-
+
long pathPointer;
- if(prop instanceof ExpressionProb) {
- pathPointer = addExpressionProb((ExpressionProb)prop);
- if(pathPointer == -1) return -1;
-
- if (((ExpressionProb)prop).getProb() == null) {
+ if (prop instanceof ExpressionProb) {
+ pathPointer = addExpressionProb((ExpressionProb) prop);
+ if (pathPointer == -1)
+ return -1;
+
+ if (((ExpressionProb) prop).getProb() == null) {
return loadProbQuestion(pathPointer);
- }
- else {
+ } else {
return -1;
}
- }
- else if (prop instanceof ExpressionReward) {
- pathPointer = addExpressionReward((ExpressionReward)prop);
- if(pathPointer == -1) return -1;
-
- if (((ExpressionReward)prop).getReward() == null) {
+ } else if (prop instanceof ExpressionReward) {
+ pathPointer = addExpressionReward((ExpressionReward) prop);
+ if (pathPointer == -1)
+ return -1;
+
+ if (((ExpressionReward) prop).getReward() == null) {
return loadRewardQuestion(pathPointer);
- }
- else {
+ } else {
return -1;
}
- }
- else return -1;
+ } else
+ return -1;
}
-
-
+
private static native int doSampling(int noIterations, int maxPathLength);
-
+
private static native double getSamplingResult(int propertyIndex);
-
+
private static native int getNumReachedMaxPath(int propertyIndex);
-
+
/**
* Used to halt the sampling algorithm in its tracks.
*/
public static native void stopSampling();
-
+
/**
- * Returns an array of indices of the properties within
- * the simulator... -1 means that the formula could not be
- * loaded
+ * Returns an array of indices of the properties within the simulator... -1 means that the formula could not be
+ * loaded
*/
private int[] addProperties(ArrayList props)
{
- int [] indices = new int[props.size()];
- for(int i = 0; i < props.size(); i++)
- {
- indices[i] = addProperty((Expression)(props.get(i)));
+ int[] indices = new int[props.size()];
+ for (int i = 0; i < props.size(); i++) {
+ indices[i] = addProperty((Expression) (props.get(i)));
}
return indices;
}
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
@@ -2257,21 +2292,24 @@ public class SimulatorEngine
{
return propertiesFile.getCombinedLabelList();
}
-
+
// Methods to compute parameters for simulation
-
+
public double computeSimulationApproximation(double confid, int numSamples)
{
- return Math.sqrt((4.0 * log(10, 2.0/confid))/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);
+ 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));
+ 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);
@@ -2279,7 +2317,7 @@ public class SimulatorEngine
// Method to check if a property is suitable for simulation
// If not, throws an exception with the reason
-
+
public void checkPropertyForSimulation(Expression prop, int modelType) throws SimulatorException
{
// Check general validity of property
@@ -2288,447 +2326,464 @@ public class SimulatorEngine
} catch (PrismLangException e) {
throw new SimulatorException(e.getMessage());
}
-
+
// Simulator can only be applied to P=? or R=? properties
boolean ok = true;
PathExpression pe = null;
- if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward)) ok = false;
+ if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward))
+ ok = false;
else if (prop instanceof ExpressionProb) {
- if ((((ExpressionProb)prop).getProb() != null)) ok = false;
- pe = ((ExpressionProb)prop).getPathExpression();
+ if ((((ExpressionProb) prop).getProb() != null))
+ ok = false;
+ pe = ((ExpressionProb) prop).getPathExpression();
+ } else if (prop instanceof ExpressionReward) {
+ if ((((ExpressionReward) prop).getReward() != null))
+ ok = false;
+ pe = ((ExpressionReward) prop).getPathExpression();
}
- else if (prop instanceof ExpressionReward) {
- if ((((ExpressionReward)prop).getReward() != null)) ok = false;
- pe = ((ExpressionReward)prop).getPathExpression();
- }
- if (!ok) throw new SimulatorException("Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\"");
-
+ if (!ok)
+ throw new SimulatorException(
+ "Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\"");
+
// Check that there are no nested probabilistic operators
try {
- pe.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(""); }
+ pe.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) {
+ } catch (PrismLangException e) {
throw new SimulatorException("Simulator cannot handle nested P, R or S operators");
}
}
- //------------------------------------------------------------------------------
- // STATE PROPOSITION METHODS
- //------------------------------------------------------------------------------
-
+ // ------------------------------------------------------------------------------
+ // STATE PROPOSITION METHODS
+ // ------------------------------------------------------------------------------
+
/**
- * Loads the boolean expression stored at exprPointer into the simulator engine.
- * Returns the index of where the proposition is being stored
+ * Loads the boolean expression stored at exprPointer into the simulator engine. Returns the index of where the
+ * proposition is being stored
*/
public static native int loadProposition(long exprPointer);
-
+
/**
- * For the state proposition stored at the given index, this returns 1 if it
- * is true in the current state and 0 if not. -1 is returned if the index
- * is invalid.
+ * For the state proposition stored at the given index, this returns 1 if it is true in the current state and 0 if
+ * not. -1 is returned if the index is invalid.
*/
public static native int queryProposition(int index);
-
+
/**
- * For the state proposition stored at the given index, this returns 1 if it
- * is true in the state at the given path step and 0 if not. -1 is returned if the index
- * is invalid.
+ * For the state proposition stored at the given index, this returns 1 if it is true in the state at the given path
+ * step and 0 if not. -1 is returned if the index is invalid.
*/
public static native int queryProposition(int index, int step);
-
+
/**
- * For the current state, this returns 1 if it is the same as
- * the initial state for the current path
+ * For the current state, this returns 1 if it is the same as the initial state for the current path
*/
public static native int queryIsInitial();
-
+
/**
- * For the state at the given index, this returns 1 if it is
- * the same as the initial state for the current path
+ * For the state at the given index, this returns 1 if it is the same as the initial state for the current path
*/
public static native int queryIsInitial(int step);
-
+
/**
- * For the current state, this returns 1 if it is a deadlock
- * state.
+ * For the current state, this returns 1 if it is a deadlock state.
*/
public static native int queryIsDeadlock();
-
+
/**
- * For the state at the given index, this returns 1 if it is
- * a deadlock state.
+ * For the state at the given index, this returns 1 if it is a deadlock state.
*/
public static native int queryIsDeadlock(int step);
-
- //------------------------------------------------------------------------------
- // PATH FORMULA METHODS
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // PATH FORMULA METHODS
+ // ------------------------------------------------------------------------------
+
/**
- * Loads the path formula stored at pathPointer into the simulator engine.
- * Returns the index of where the path is being stored
+ * Loads the path formula stored at pathPointer into the simulator engine. Returns the index of where the path is
+ * being stored
*/
public static native int findPathFormulaIndex(long pathPointer);
-
+
/**
- * For the path formula at the given index, this returns:
- *
- * - -1 if the answer is unknown
- *
- 0 if the answer is false
- *
- 1 if the answer is true
- *
- 2 if the answer is numeric
- *
+ * For the path formula at the given index, this returns:
+ *
+ * - -1 if the answer is unknown
+ *
- 0 if the answer is false
+ *
- 1 if the answer is true
+ *
- 2 if the answer is numeric
+ *
*/
public static native int queryPathFormula(int index);
-
+
/**
- * Returns the numberic answer for the indexed path formula
+ * Returns the numberic answer for the indexed path formula
*/
public static native double queryPathFormulaNumeric(int index);
-
- //------------------------------------------------------------------------------
- // EXPRESSION CREATION METHODS
- // These methods provide facilities to create expressions (either for
- // the model or for properties).
- // The data structures are built in c++. The methods return integers
- // that are actually pointers to CExpression objects. They are
- // public because they are used in the
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // EXPRESSION CREATION METHODS
+ // These methods provide facilities to create expressions (either for
+ // the model or for properties).
+ // The data structures are built in c++. The methods return integers
+ // that are actually pointers to CExpression objects. They are
+ // public because they are used in the
+ // ------------------------------------------------------------------------------
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalConstant(int constIndex, int type);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealConstant(int constIndex);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createIntegerVar(int varIndex);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createBooleanVar(int varIndex);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createDouble(double value);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createInteger(int value);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createBoolean(boolean value);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createCeil(long exprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createFloor(long exprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalPow(long baseExpressionPointer, long exponentExpressionPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealPow(long baseExpressionPointer, long exponentExpressionPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createMod(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createLog(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNot(long exprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createAnd(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createOr(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalMax(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalMin(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealMax(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealMin(long[] exprPointers);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalTimes(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalPlus(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalMinus(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealTimes(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealPlus(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealMinus(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createDivide(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createIte(long conditionPointer, long truePointer, long falsePointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealIte(long conditionPointer, long truePointer, long falsePointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalEquals(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealEquals(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalNotEquals(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealNotEquals(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalLessThan(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealLessThan(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalGreaterThan(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealGreaterThan(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalLessThanEqual(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealLessThanEqual(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createNormalGreaterThanEqual(long lexprPointer, long rexprPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createRealGreaterThanEqual(long lexprPointer, long rexprPointer);
-
-
- //------------------------------------------------------------------------------
- // PCTL FORMULAE CREATION METHODS
- // These methods provide facilities to build PCTL and CSL Formulae
- //------------------------------------------------------------------------------
-
- //internal formulae (these methods return a pointer to the formula's memory
- //location
-
- private static native long loadPctlBoundedUntil(long leftExprPointer, long rightExprPointer, double lowerBound, double upperBound);
- private static native long loadPctlBoundedUntilNegated(long leftExprPointer, long rightExprPointer, double lowerBound, double upperBound);
-
+
+ // ------------------------------------------------------------------------------
+ // PCTL FORMULAE CREATION METHODS
+ // These methods provide facilities to build PCTL and CSL Formulae
+ // ------------------------------------------------------------------------------
+
+ // internal formulae (these methods return a pointer to the formula's memory
+ // location
+
+ private static native long loadPctlBoundedUntil(long leftExprPointer, long rightExprPointer, double lowerBound,
+ double upperBound);
+
+ private static native long loadPctlBoundedUntilNegated(long leftExprPointer, long rightExprPointer,
+ double lowerBound, double upperBound);
+
private static native long loadPctlUntil(long leftExprPointer, long rightExprPointer);
+
private static native long loadPctlUntilNegated(long leftExprPointer, long rightExprPointer);
-
+
private static native long loadPctlNext(long exprPointer);
-
+
private static native long loadPctlReachability(int rsi, long expressionPointer);
-
+
private static native long loadPctlCumulative(int rsi, double time);
-
+
private static native long loadPctlInstantanious(int rsi, double time);
-
- //prob formulae (these return the index of the property within the engine.
-
+
+ // prob formulae (these return the index of the property within the engine.
+
private static native int loadProbQuestion(long pathPointer);
-
-
- //rewards formulae (these return the index of the property within the engine.
-
+
+ // rewards formulae (these return the index of the property within the engine.
+
private static native int loadRewardQuestion(long pathPointer);
-
-
- //------------------------------------------------------------------------------
- // TRANSITION TABLE CREATION METHODS
- // These methods provide facilities to build the transition table's commands,
- // updates and assignments.
- // The data structures are built in c++. The methods return integers
- // that are actually pointers.
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // TRANSITION TABLE CREATION METHODS
+ // These methods provide facilities to build the transition table's commands,
+ // updates and assignments.
+ // The data structures are built in c++. The methods return integers
+ // that are actually pointers.
+ // ------------------------------------------------------------------------------
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createCommand(long guardPointer, int actionIndex, int moduleIndex, int numUpdates);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long addUpdate(long commandPointer, long probPointer, int numAssignments);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long addAssignment(long updatePointer, int varIndex, long rhsPointer);
-
-
- //------------------------------------------------------------------------------
- // REWARDS TABLE CREATION METHODS
- // These methods provide facilities to build the rewards tables.
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // REWARDS TABLE CREATION METHODS
+ // These methods provide facilities to build the rewards tables.
+ // ------------------------------------------------------------------------------
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createStateReward(long guardPointer, long rewardPointer);
-
+
/**
* Used by the recursive model/properties loading methods (not part of the API)
*/
public static native long createTransitionReward(int actionIndex, long guardPointer, long rewardPointer);
-
- //------------------------------------------------------------------------------
- // UTILITY METHODS
- // These are for debugging purposes only
- //------------------------------------------------------------------------------
-
+
+ // ------------------------------------------------------------------------------
+ // UTILITY METHODS
+ // These are for debugging purposes only
+ // ------------------------------------------------------------------------------
+
/**
* Convienience method to print an expression at a given pointer location
- * @param exprPointer the expression pointer.
+ *
+ * @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.
+ *
+ * @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);
-
+
/**
* Deletes an expression from memory.
+ *
* @deprecated A bit drastic now.
- * @param exprPointer the pointer to the location of the expression
+ * @param exprPointer
+ * the pointer to the location of the expression
*/
- public static native void deleteExpression(long exprPointer); //use with care!
-
+ public static native void deleteExpression(long exprPointer); // use with care!
+
/**
* 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.
+
+ // ------------------------------------------------------------------------------
+ // 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();
-
+
}
-//==================================================================================
+// ==================================================================================