diff --git a/prism/include/SimulatorEngine.h b/prism/include/SimulatorEngine.h index 32b4913e..7330420a 100644 --- a/prism/include/SimulatorEngine.h +++ b/prism/include/SimulatorEngine.h @@ -33,6 +33,12 @@ extern "C" { #define simulator_SimulatorEngine_DOUBLE 2L #undef simulator_SimulatorEngine_BOOLEAN #define simulator_SimulatorEngine_BOOLEAN 3L +#undef simulator_SimulatorEngine_SIM_PATH_NUM_STEPS +#define simulator_SimulatorEngine_SIM_PATH_NUM_STEPS 0L +#undef simulator_SimulatorEngine_SIM_PATH_TIME +#define simulator_SimulatorEngine_SIM_PATH_TIME 1L +#undef simulator_SimulatorEngine_SIM_PATH_DEADLOCK +#define simulator_SimulatorEngine_SIM_PATH_DEADLOCK 2L /* * Class: simulator_SimulatorEngine * Method: Set_Main_Log diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index d60c5488..3bb48e0c 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1183,6 +1183,19 @@ public class Prism } } + // generate a random path through the model using the simulator + + public void generateSimulationPath(ModulesFile modulesFile, String details, int maxPathLength, File file) throws PrismException + { + // do path generation + try { + getSimulator().generateSimulationPath(modulesFile, modulesFile.getInitialValues(), details, maxPathLength, file); + } + catch (SimulatorException e) { + throw new PrismException(e.getMessage()); + } + } + // model checking using APMC techniques public void checkPropertyForAPMC(ModulesFile modulesFile, PropertiesFile propertiesFile, PCTLFormula f) throws PrismException diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index e487920e..0af8e74b 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -56,6 +56,7 @@ public class PrismCL private int exportType = Prism.EXPORT_PLAIN; private boolean exportordered = true; private boolean simulate = false; + private boolean simpath = false; private boolean apmc = false; private int typeOverride = 0; @@ -66,6 +67,9 @@ public class PrismCL // argument to -const switch private String constSwitch = null; + // argument to -simpath switch + private String simpathDetails = null; + // import info private String importInitString = null; @@ -84,6 +88,7 @@ public class PrismCL private String exportDotFilename = null; private String exportTransDotFilename = null; private String exportResultsFilename = null; + private String simpathFilename = null; // logs private PrismLog mainLog = null; @@ -191,6 +196,19 @@ public class PrismCL continue; } + // if requested, generate a random path with simulator (and then skip anything else) + if (simpath) { + try { + File f = (simpathFilename.equals("stdout")) ? null : new File(simpathFilename); + prism.generateSimulationPath(modulesFile, simpathDetails, simMaxPath, f); + } + catch (PrismException e) { + error(e.getMessage()); + } + undefinedConstants.iterateModel(); + continue; + } + // only do explicit model construction if necessary if (!simulate) { @@ -923,6 +941,17 @@ public class PrismCL else if (sw.equals("sim")) { simulate = true; } + // generate path with simulator + else if (sw.equals("simpath")) { + if (i < args.length-2) { + simpath = true; + simpathDetails = args[++i]; + simpathFilename = args[++i]; + } + else { + errorAndExit("The -"+sw+" switch requires two arguments (path details, filename)"); + } + } // use apmc techniques else if (sw.equals("apmc")) { if (Apmc.isEnabled()) { diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 2336b44e..6b892026 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -36,6 +36,7 @@ import prism.*; * exploration. *
  • To perform Monte-Carlo sampling techniques for approximate property * verification.
  • + *
  • To generate whole random paths at once.
  • * * Each type of use only builds the relevant data structures of the simulator * engine. @@ -161,6 +162,16 @@ import prism.*; * of performing an experiment and storing the results in an * appropriate ResultsCollection object. * + * + *

    Path Generation

    + * + * The following utility method is used for generating (and exporting) + * a single path satsifying certain criteria: + * + * + * * @author Andrew Hinton */ public class SimulatorEngine @@ -234,6 +245,10 @@ public class SimulatorEngine */ public static final int BOOLEAN = Expression.BOOLEAN; + // Types of random path to generate + public static final int SIM_PATH_NUM_STEPS = 0; + public static final int SIM_PATH_TIME = 1; + public static final int SIM_PATH_DEADLOCK = 2; //------------------------------------------------------------------------------ // CLASS MEMBERS @@ -775,6 +790,8 @@ public class SimulatorEngine loadModulesFile(modulesFile, modulesFile.getConstantValues()); + if (propertiesFile == null) propertiesFile = new PropertiesFile(modulesFile); + propertyConstants = propertiesFile.getConstantValues(); this.propertiesFile = propertiesFile; @@ -983,83 +1000,115 @@ public class SimulatorEngine /** * Exports the current path to a file in a simple space separated format. - * @param f the file to which the path should be exported to. + * @param file the file to which the path should be exported to (mainLog if null). * @throws SimulatorException if there is a problem with writing the file. */ - public void exportPath(File f) throws SimulatorException + public void exportPath(File file) throws SimulatorException { - try + exportPath(file, false, " "); + } + + /** + * Exports the current path to a file in a simple space separated format. + * @param file the file to which the path should be exported to (mainLog if null). + * @param timeCumul show time in cumulative form? + * @param colSep string used to separate columns in display + * @throws SimulatorException if there is a problem with writing the file. + */ + public void exportPath(File file, boolean timeCumul, String colSep) throws SimulatorException + { + PrismLog log; + + // create new file log or use main log + if (file != null) { + log = new PrismFileLog(file.getPath()); + if (!log.ready()) { + throw new SimulatorException("Could not open file \""+file+"\" for output"); + } + mainLog.println("\nExporting path to file \""+file+"\"..."); + } else { + log = mainLog; + log.println(); + } + + exportPathToLog(log, timeCumul, colSep); + } + + /** + * Exports the current path to a file in a simple space separated format. + * @param filename the PrismLog to which the path should be exported to + * @param colSep string used to separate columns in display + * @throws SimulatorException if there is a problem with writing the file. + */ + public void exportPathToLog(PrismLog log, boolean timeCumul, String colSep) throws SimulatorException + { + int i, j, n, nv, nr; + double d, t; + boolean stochastic = (modulesFile.getType() == ModulesFile.STOCHASTIC); + + if(modulesFile == null) { - int i, j, n, nv, nr; - PrintWriter pw = new PrintWriter(new FileWriter(f), false); - - if(modulesFile == null) - { - pw.flush(); - pw.close(); - return; + log.flush(); + log.close(); + return; + } + //Write headers + log.print("step"); + nv = getNumVariables(); + nr = modulesFile.getNumRewardStructs(); + for(j = 0; j < nv; j++) + { + log.print(colSep+varNames[j]); + } + if (stochastic) + { + log.print(colSep+(timeCumul?"time":"time_in_state")); + } + if (nr == 1) { + log.print(colSep+"state_reward"+colSep+"transition_reward"); + } else { + for(j = 0; j < nr; j++) { + log.print(colSep+"state_reward"+j+colSep+"transition_reward"+j); } - //Write headers - pw.print("step "); - nv = getNumVariables(); - nr = modulesFile.getNumRewardStructs(); + } + log.println(); + + //Write path + n = getPathSize(); + nv = getNumVariables(); + nr = modulesFile.getNumRewardStructs(); + t = 0.0; + for(i = 0; i < n; i++) + { + log.print(i); for(j = 0; j < nv; j++) { - if (j>0) pw.print(" "); - pw.print(varNames[j]); - } - if(modulesFile.getType() == ModulesFile.STOCHASTIC) - { - pw.print(" time_in_state"); - } - if (nr == 1) { - pw.print(" state_reward transition_reward"); - } else { - for(j = 0; j < nr; j++) { - pw.print(" state_reward"+j+" transition_reward"+j); - } - } - pw.println(); - - //Write path - - n = getPathSize(); - nv = getNumVariables(); - nr = modulesFile.getNumRewardStructs(); - for(i = 0; i < n; i++) - { - pw.print(i+" "); - for(j = 0; j < nv; j++) + log.print(colSep); + if(varTypes[j] == Expression.BOOLEAN) { - if (j>0) pw.print(" "); - if(varTypes[j] == Expression.BOOLEAN) - { - if(getPathData(j, i) == 0) pw.print("false"); - else pw.print("true"); - } - else - { - pw.print(getPathData(j, i)); - } + if(getPathData(j, i) == 0) log.print("false"); + else log.print("true"); } - if(modulesFile.getType() == ModulesFile.STOCHASTIC) + else { - pw.print(" "+((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; + } + } + + // export path + if (simPathType == SIM_PATH_DEADLOCK && queryIsDeadlock() != 1) { + mainLog.println("\nNo deadlock state found within "+maxPathLength+" steps."); + } else { + exportPath(file, true, simPathSep); + } + + // 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."); + } + } + /** * Returns a pointer to the built reward formula * @param operand the PCTLFormula to be built into the engine.