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

Push some log output into Prism (+ autoformat). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4600 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
3ee7bb5651
commit
58c1803f32
3 changed files with 50 additions and 56 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 27
      prism/src/prism/Prism.java
  2. 72
      prism/src/prism/PrismCL.java
  3. 7
      prism/src/userinterface/properties/GUIExperiment.java

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

@ -1419,7 +1419,7 @@ public class Prism implements PrismSettingsListener
mainLog.print(currentModulesFile.getVarName(i) + " "); mainLog.print(currentModulesFile.getVarName(i) + " ");
} }
mainLog.println(); mainLog.println();
// If required, export parsed PRISM model // If required, export parsed PRISM model
if (exportPrism) { if (exportPrism) {
try { try {
@ -1621,7 +1621,7 @@ public class Prism implements PrismSettingsListener
// Clear any existing built model(s) // Clear any existing built model(s)
clearBuiltModel(); clearBuiltModel();
try { try {
if (currentModulesFile == null) if (currentModulesFile == null)
throw new PrismException("There is no currently loaded PRISM model to build"); throw new PrismException("There is no currently loaded PRISM model to build");
@ -2214,7 +2214,7 @@ public class Prism implements PrismSettingsListener
} else { } else {
currentModelExpl.exportStates(exportType, currentModulesFile.createVarList(), tmpLog); currentModelExpl.exportStates(exportType, currentModulesFile.createVarList(), tmpLog);
} }
// Tidy up // Tidy up
if (file != null) if (file != null)
tmpLog.close(); tmpLog.close();
@ -2374,6 +2374,7 @@ public class Prism implements PrismSettingsListener
{ {
Object res = null; Object res = null;
// Print info
mainLog.printSeparator(); mainLog.printSeparator();
mainLog.println("\nSimulating: " + expr); mainLog.println("\nSimulating: " + expr);
if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
@ -2384,7 +2385,7 @@ public class Prism implements PrismSettingsListener
// Check that property is valid for this model type // Check that property is valid for this model type
expr.checkValid(currentModelType); expr.checkValid(currentModelType);
// Do model checking
// Do simulation
res = getSimulator().modelCheckSingleProperty(currentModulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod); res = getSimulator().modelCheckSingleProperty(currentModulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod);
return new Result(res); return new Result(res);
@ -2409,6 +2410,7 @@ public class Prism implements PrismSettingsListener
{ {
Object[] res = null; Object[] res = null;
// Print info
mainLog.printSeparator(); mainLog.printSeparator();
mainLog.print("\nSimulating"); mainLog.print("\nSimulating");
if (exprs.size() == 1) { if (exprs.size() == 1) {
@ -2428,7 +2430,7 @@ public class Prism implements PrismSettingsListener
for (Expression expr : exprs) for (Expression expr : exprs)
expr.checkValid(currentModelType); expr.checkValid(currentModelType);
// Do model checking
// Do simulation
res = getSimulator().modelCheckMultipleProperties(currentModulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod); res = getSimulator().modelCheckMultipleProperties(currentModulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod);
Result[] resArray = new Result[res.length]; Result[] resArray = new Result[res.length];
@ -2456,11 +2458,18 @@ public class Prism implements PrismSettingsListener
* @throws PrismException if something goes wrong with the sampling algorithm * @throws PrismException if something goes wrong with the sampling algorithm
* @throws InterruptedException if the thread is interrupted * @throws InterruptedException if the thread is interrupted
*/ */
public void modelCheckSimulatorExperiment(PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results,
Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException
public void modelCheckSimulatorExperiment(PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, Expression expr,
State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException
{ {
getSimulator().modelCheckExperiment(currentModulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength,
simMethod);
// Print info
mainLog.printSeparator();
mainLog.println("\nSimulating: " + expr);
if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
mainLog.println("Model constants: " + currentDefinedMFConstants);
mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
// Do simulation
getSimulator().modelCheckExperiment(currentModulesFile, propertiesFile, undefinedConstants, results, expr, initialState, pathLength, simMethod);
} }
/** /**

72
prism/src/prism/PrismCL.java
View File

@ -122,7 +122,7 @@ public class PrismCL implements PrismModelListener
// model failure info // model failure info
boolean modelBuildFail = false; boolean modelBuildFail = false;
Exception modelBuildException = null; Exception modelBuildException = null;
// info about which properties to model check // info about which properties to model check
private int numPropertiesToCheck = 0; private int numPropertiesToCheck = 0;
private List<Property> propertiesToCheck = null; private List<Property> propertiesToCheck = null;
@ -183,7 +183,7 @@ public class PrismCL implements PrismModelListener
undefinedMFConstants = new UndefinedConstants(modulesFile, null); undefinedMFConstants = new UndefinedConstants(modulesFile, null);
undefinedMFConstants.defineUsingConstSwitch(constSwitch); undefinedMFConstants.defineUsingConstSwitch(constSwitch);
// and one set of info for each property // and one set of info for each property
undefinedConstants = new UndefinedConstants[numPropertiesToCheck];
undefinedConstants = new UndefinedConstants[numPropertiesToCheck];
for (i = 0; i < numPropertiesToCheck; i++) { for (i = 0; i < numPropertiesToCheck; i++) {
undefinedConstants[i] = new UndefinedConstants(modulesFile, propertiesFile, propertiesToCheck.get(i)); undefinedConstants[i] = new UndefinedConstants(modulesFile, propertiesFile, propertiesToCheck.get(i));
undefinedConstants[i].defineUsingConstSwitch(constSwitch); undefinedConstants[i].defineUsingConstSwitch(constSwitch);
@ -221,7 +221,7 @@ public class PrismCL implements PrismModelListener
} }
modelBuildFail = false; modelBuildFail = false;
// if requested, generate a random path with the simulator // if requested, generate a random path with the simulator
if (simpath) { if (simpath) {
try { try {
@ -243,7 +243,7 @@ public class PrismCL implements PrismModelListener
doExports(); doExports();
if (modelBuildFail) if (modelBuildFail)
continue; continue;
// Do steady-state/transient probability computation, if required // Do steady-state/transient probability computation, if required
doSteadyState(); doSteadyState();
if (modelBuildFail) if (modelBuildFail)
@ -258,13 +258,6 @@ public class PrismCL implements PrismModelListener
// for simulation we can do multiple values of property constants simultaneously // for simulation we can do multiple values of property constants simultaneously
if (simulate && undefinedConstants[j].getNumPropertyIterations() > 1) { if (simulate && undefinedConstants[j].getNumPropertyIterations() > 1) {
try { try {
// TODO: remove output
mainLog.printSeparator();
mainLog.println("\nSimulating: " + propertiesToCheck.get(j));
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
mainLog.println("Model constants: " + definedMFConstants);
mainLog.println("Property constants: " + undefinedConstants[j].getPFDefinedConstantsString());
simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression());
prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants[j], results[j], propertiesToCheck.get(j).getExpression(), null, prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants[j], results[j], propertiesToCheck.get(j).getExpression(), null,
simMaxPath, simMethod); simMaxPath, simMethod);
@ -294,7 +287,8 @@ public class PrismCL implements PrismModelListener
// Approximate (simulation-based) model checking // Approximate (simulation-based) model checking
else { else {
simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression());
res = prism.modelCheckSimulator(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants, null, simMaxPath, simMethod);
res = prism.modelCheckSimulator(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants, null, simMaxPath,
simMethod);
simMethod.reset(); simMethod.reset();
} }
} catch (PrismException e) { } catch (PrismException e) {
@ -308,7 +302,7 @@ public class PrismCL implements PrismModelListener
results[j].setMultipleErrors(definedMFConstants, null, modelBuildException); results[j].setMultipleErrors(definedMFConstants, null, modelBuildException);
continue; continue;
} }
// store result of model checking // store result of model checking
results[j].setResult(definedMFConstants, definedPFConstants, res.getResult()); results[j].setResult(definedMFConstants, definedPFConstants, res.getResult());
Object cex = res.getCounterexample(); Object cex = res.getCounterexample();
@ -339,7 +333,7 @@ public class PrismCL implements PrismModelListener
// iterate to next property // iterate to next property
undefinedConstants[j].iterateProperty(); undefinedConstants[j].iterateProperty();
} }
// in case of build failure during model checking, store as result for any further properties, and go on to the next model // in case of build failure during model checking, store as result for any further properties, and go on to the next model
if (modelBuildFail) { if (modelBuildFail) {
for (j++; j < numPropertiesToCheck; j++) { for (j++; j < numPropertiesToCheck; j++) {
@ -363,7 +357,7 @@ public class PrismCL implements PrismModelListener
error(e.getMessage()); error(e.getMessage());
} }
} }
// iterate to next model // iterate to next model
undefinedMFConstants.iterateModel(); undefinedMFConstants.iterateModel();
for (j = 0; j < numPropertiesToCheck; j++) { for (j = 0; j < numPropertiesToCheck; j++) {
@ -385,7 +379,7 @@ public class PrismCL implements PrismModelListener
if (!tmpLog.ready()) { if (!tmpLog.ready()) {
errorAndExit("Couldn't open file \"" + exportResultsFilename + "\" for output"); errorAndExit("Couldn't open file \"" + exportResultsFilename + "\" for output");
} }
String sep = exportresultscsv ? ", " : "\t"; String sep = exportresultscsv ? ", " : "\t";
for (i = 0; i < numPropertiesToCheck; i++) { for (i = 0; i < numPropertiesToCheck; i++) {
if (i > 0) if (i > 0)
@ -512,7 +506,7 @@ public class PrismCL implements PrismModelListener
mainLog.println("(" + (i + 1) + ") " + propertiesFile.getPropertyObject(i)); mainLog.println("(" + (i + 1) + ") " + propertiesFile.getPropertyObject(i));
} }
} }
// Load model into PRISM (if not done already) // Load model into PRISM (if not done already)
if (!importtrans) { if (!importtrans) {
prism.loadPRISMModel(modulesFile); prism.loadPRISMModel(modulesFile);
@ -527,7 +521,7 @@ public class PrismCL implements PrismModelListener
int i; int i;
propertiesToCheck = new ArrayList<Property>(); propertiesToCheck = new ArrayList<Property>();
// no properties to check // no properties to check
if (propertiesFile == null) { if (propertiesFile == null) {
numPropertiesToCheck = 0; numPropertiesToCheck = 0;
@ -740,7 +734,7 @@ public class PrismCL implements PrismModelListener
mainLog.println("\nError: " + e.getMessage() + "."); mainLog.println("\nError: " + e.getMessage() + ".");
} }
} }
// export BSCCs to a file // export BSCCs to a file
if (exportbsccs) { if (exportbsccs) {
try { try {
@ -848,19 +842,19 @@ public class PrismCL implements PrismModelListener
} }
// PrismModelListener methods // PrismModelListener methods
@Override @Override
public void notifyModelBuildSuccessful() public void notifyModelBuildSuccessful()
{ {
} }
@Override @Override
public void notifyModelBuildFailed(PrismException e) public void notifyModelBuildFailed(PrismException e)
{ {
modelBuildFail = true; modelBuildFail = true;
modelBuildException = e; modelBuildException = e;
} }
/** /**
* Process command-line arguments/switches. * Process command-line arguments/switches.
*/ */
@ -883,7 +877,7 @@ public class PrismCL implements PrismModelListener
// Note: the order of these switches should match the -help output (just to help keep track of things). // Note: the order of these switches should match the -help output (just to help keep track of things).
// But: processing of "PRISM" options is done elsewhere in PrismSettings // But: processing of "PRISM" options is done elsewhere in PrismSettings
// Any "hidden" options, i.e. not in -help text/manual, are indicated as such. // Any "hidden" options, i.e. not in -help text/manual, are indicated as such.
// print help // print help
if (sw.equals("help") || sw.equals("-help") || sw.equals("?")) { if (sw.equals("help") || sw.equals("-help") || sw.equals("?")) {
printHelp(); printHelp();
@ -977,9 +971,9 @@ public class PrismCL implements PrismModelListener
test = true; test = true;
testExitsOnFail = false; testExitsOnFail = false;
} }
// IMPORT OPTIONS: // IMPORT OPTIONS:
// change model type to pepa // change model type to pepa
else if (sw.equals("importpepa")) { else if (sw.equals("importpepa")) {
importpepa = true; importpepa = true;
@ -1036,9 +1030,9 @@ public class PrismCL implements PrismModelListener
else if (sw.equals("ctmc")) { else if (sw.equals("ctmc")) {
typeOverride = ModelType.CTMC; typeOverride = ModelType.CTMC;
} }
// EXPORT OPTIONS: // EXPORT OPTIONS:
// export results // export results
else if (sw.equals("exportresults")) { else if (sw.equals("exportresults")) {
if (i < args.length - 1) { if (i < args.length - 1) {
@ -1256,12 +1250,12 @@ public class PrismCL implements PrismModelListener
errorAndExit("No file specified for -" + sw + " switch"); errorAndExit("No file specified for -" + sw + " switch");
} }
} }
// NB: Following the ordering of the -help text, more options go here, // NB: Following the ordering of the -help text, more options go here,
// but these are processed in the PrismSettings class; see below // but these are processed in the PrismSettings class; see below
// SIMULATION OPTIONS: // SIMULATION OPTIONS:
// use simulator for approximate/statistical model checking // use simulator for approximate/statistical model checking
else if (sw.equals("sim")) { else if (sw.equals("sim")) {
simulate = true; simulate = true;
@ -1389,7 +1383,7 @@ public class PrismCL implements PrismModelListener
} }
// FURTHER OPTIONS - NEED TIDYING/FIXING // FURTHER OPTIONS - NEED TIDYING/FIXING
// zero-reward loops check on // zero-reward loops check on
else if (sw.equals("zerorewardcheck")) { else if (sw.equals("zerorewardcheck")) {
prism.setCheckZeroLoops(true); prism.setCheckZeroLoops(true);
@ -1397,11 +1391,9 @@ public class PrismCL implements PrismModelListener
// MDP solution method // MDP solution method
else if (sw.equals("valiter")) { else if (sw.equals("valiter")) {
prism.setMDPSolnMethod(Prism.MDP_VALITER); prism.setMDPSolnMethod(Prism.MDP_VALITER);
}
else if (sw.equals("politer")) {
} else if (sw.equals("politer")) {
prism.setMDPSolnMethod(Prism.MDP_POLITER); prism.setMDPSolnMethod(Prism.MDP_POLITER);
}
else if (sw.equals("modpoliter")) {
} else if (sw.equals("modpoliter")) {
prism.setMDPSolnMethod(Prism.MDP_MODPOLITER); prism.setMDPSolnMethod(Prism.MDP_MODPOLITER);
} }
// explicit-state model construction // explicit-state model construction
@ -1412,7 +1404,7 @@ public class PrismCL implements PrismModelListener
else if (sw.equals("explicitbuildtest")) { else if (sw.equals("explicitbuildtest")) {
explicitbuildtest = true; explicitbuildtest = true;
} }
// MISCELLANEOUS UNDOCUMENTED/UNUSED OPTIONS: // MISCELLANEOUS UNDOCUMENTED/UNUSED OPTIONS:
// specify main log (hidden option) // specify main log (hidden option)
@ -1472,7 +1464,7 @@ public class PrismCL implements PrismModelListener
} }
// Other switches - pass to PrismSettings // Other switches - pass to PrismSettings
else { else {
i = prism.getSettings().setFromCommandLineSwitch(args, i) - 1; i = prism.getSettings().setFromCommandLineSwitch(args, i) - 1;
} }
@ -1536,7 +1528,7 @@ public class PrismCL implements PrismModelListener
if (prism.getExplicit()) { if (prism.getExplicit()) {
explicitbuild = false; explicitbuild = false;
} }
// check not trying to do gauss-seidel with mtbdd engine // check not trying to do gauss-seidel with mtbdd engine
if (prism.getEngine() == Prism.MTBDD) { if (prism.getEngine() == Prism.MTBDD) {
j = prism.getLinEqMethod(); j = prism.getLinEqMethod();
@ -1734,9 +1726,9 @@ public class PrismCL implements PrismModelListener
mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file"); mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file");
mainLog.println("-exportprism <file> ............ Export final PRISM model to a file"); mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");
mainLog.println("-exportprismconst <file> ....... Export final PRISM model with expanded constants to a file"); mainLog.println("-exportprismconst <file> ....... Export final PRISM model with expanded constants to a file");
prism.getSettings().printHelp(mainLog); prism.getSettings().printHelp(mainLog);
mainLog.println(); mainLog.println();
mainLog.println("SIMULATION OPTIONS:"); mainLog.println("SIMULATION OPTIONS:");
mainLog.println("-sim ........................... Use the PRISM simulator to approximate results of model checking"); mainLog.println("-sim ........................... Use the PRISM simulator to approximate results of model checking");

7
prism/src/userinterface/properties/GUIExperiment.java
View File

@ -270,13 +270,6 @@ public class GUIExperiment
if (useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) if (useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS)
&& undefinedConstants.getNumPropertyIterations() > 1) { && undefinedConstants.getNumPropertyIterations() > 1) {
try { try {
// TODO
logSeparator();
logln("\nSimulating: " + propertyToCheck);
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
logln("Model constants: " + definedMFConstants);
logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
// convert initial Values -> State // convert initial Values -> State
// (remember: null means use default or pick randomly) // (remember: null means use default or pick randomly)
parser.State initialState; parser.State initialState;

Write Preview
Loading…
Cancel
Save