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

Auto-format (for merging purposes). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10717 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
5ce657090b
commit
0b04c50ea5
1 changed files with 36 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 70
      prism/src/prism/Prism.java

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

@ -172,7 +172,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
}
}
}
//------------------------------------------------------------------------------
// Settings / flags / options
//------------------------------------------------------------------------------
@ -194,9 +194,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
protected boolean exportProductStates = false;
protected String exportProductStatesFilename = null;
// Store the final results vector after model checking?
protected boolean storeVector = false;
protected boolean storeVector = false;
// Generate/store a strategy during model checking?
protected boolean genStrat = false;
protected boolean genStrat = false;
// Do bisimulation minimisation before model checking?
protected boolean doBisim = false;
@ -657,7 +657,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
{
return "PRISM";
}
/**
* Get current version number, as a string.
*/
@ -782,7 +782,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
{
return settings.getBoolean(PrismSettings.PRISM_PROB1);
}
public boolean getPreRel()
{
return settings.getBoolean(PrismSettings.PRISM_PRE_REL);
@ -1070,7 +1070,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
{
return explicit.SCCComputer.createSCCComputer(this, model);
}
/**
* Get an ECComputer object.
*/
@ -1082,7 +1082,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
/**
* Get an ECComputer object.
*/
public ECComputer getECComputer(JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars) throws PrismException
public ECComputer getECComputer(JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars)
throws PrismException
{
return ECComputer.createECComputer(this, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars);
}
@ -1094,7 +1095,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
{
return explicit.ECComputer.createECComputer(this, model);
}
//------------------------------------------------------------------------------
// Utility methods
//------------------------------------------------------------------------------
@ -1483,7 +1484,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
}
return importer;
}
/**
* Import a PRISM model from a PRISM preprocessor file
* @param file File to read in
@ -1891,7 +1892,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
private void doBuildModel() throws PrismException
{
long l; // timer
// Clear any existing built model(s)
clearBuiltModel();
@ -2418,7 +2419,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
new StateListMTBDD(sccComputer.getBSCCs().get(i), currentModel).printMatlab(tmpLog);
JDD.Deref(sccComputer.getBSCCs().get(i));
} else {
explicit.StateValues.createFromBitSet(sccComputerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true);
explicit.StateValues.createFromBitSet(sccComputerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB,
true, true);
}
if (exportType == EXPORT_MATLAB)
tmpLog.println("];");
@ -2511,7 +2513,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
new StateListMTBDD(ecComputer.getMECStates().get(i), currentModel).printMatlab(tmpLog);
JDD.Deref(ecComputer.getMECStates().get(i));
} else {
explicit.StateValues.createFromBitSet(ecComputerExpl.getMECStates().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true);
explicit.StateValues.createFromBitSet(ecComputerExpl.getMECStates().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB,
true, true);
}
if (exportType == EXPORT_MATLAB)
tmpLog.println("];");
@ -2521,7 +2524,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (file != null)
tmpLog.close();
}
/**
* Export the (states of the) currently loaded model's strongly connected components (SCCs) to a file
* @param exportType Type of export; one of: <ul>
@ -2600,7 +2603,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
new StateListMTBDD(sccComputer.getSCCs().get(i), currentModel).printMatlab(tmpLog);
JDD.Deref(sccComputer.getSCCs().get(i));
} else {
explicit.StateValues.createFromBitSet(sccComputerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true);
explicit.StateValues.createFromBitSet(sccComputerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB,
true, true);
}
if (exportType == EXPORT_MATLAB)
tmpLog.println("];");
@ -2654,7 +2658,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
for (int i = 0; i < numLabels; i++) {
labelNames.add(ll.getLabelName(i));
}
// Export
if (getExplicit()) {
PrismLog out = getPrismLogForFile(file);
@ -2780,7 +2784,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// Create new model checker object and do model checking
if (!getExplicit()) {
ModelChecker mc = createModelChecker(propertiesFile);
ModelChecker mc = createModelChecker(propertiesFile);
res = mc.check(prop.getExpression());
} else {
explicit.StateModelChecker mc = createModelCheckerExplicit(propertiesFile);
@ -3014,7 +3018,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
Result result = mc.check(modelExpl, prop.getExpression());
// Convert result of parametric model checking to just a rational
// There should be just one region since no parameters are used
RegionValues regVals = (RegionValues) result.getResult();
@ -3025,17 +3029,17 @@ public class Prism extends PrismComponent implements PrismSettingsListener
BigRational rat = func.evaluate(new param.Point(new BigRational[] { new BigRational(0) }));
// Restore in result object
result.setResult(rat);
// Print result to log
String resultString = "Result";
if (!("Result".equals(prop.getExpression().getResultName())))
resultString += " (" + prop.getExpression().getResultName().toLowerCase() + ")";
resultString += ": " + result.getResultString();
mainLog.print("\n" + resultString);
return result;
}
/**
* Perform parametric model checking on the currently loaded model.
* @param propertiesFile parent properties file
@ -3078,17 +3082,17 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
Result result = mc.check(modelExpl, prop.getExpression());
// Print result to log
String resultString = "Result";
if (!("Result".equals(prop.getExpression().getResultName())))
resultString += " (" + prop.getExpression().getResultName().toLowerCase() + ")";
resultString += ": " + result.getResultString();
mainLog.print("\n" + resultString);
return result;
}
/**
* Export a strategy. The associated model should be attached to the strategy.
* Strictly, speaking that does not need to be the currently loaded model,
@ -3124,7 +3128,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (file != null)
tmpLog.close();
}
/**
* Generate a random path through the model using the simulator.
* @param modulesFile The model
@ -3222,16 +3226,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
ProbModelChecker mc;
if (model.getModelType() == ModelType.DTMC) {
mc = new ProbModelChecker(this, model, null);
}
else if (model.getModelType() == ModelType.CTMC) {
} else if (model.getModelType() == ModelType.CTMC) {
mc = new StochModelChecker(this, model, null);
}
else {
} else {
throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
}
return mc.doSteadyState(fileIn);
}
/**
* Compute steady-state probabilities (for a DTMC or CTMC) using the explicit engine.
* Optionally (if non-null), read in the initial probability distribution from a file.
@ -3293,7 +3295,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// Print message
mainLog.printSeparator();
String strTime = currentModelType.continuousTime() ? Double.toString(time) : Integer.toString((int) time);
mainLog.println("\nComputing transient probabilities (time = " + strTime + ")...");
mainLog.println("\nComputing transient probabilities (time = " + strTime + ")...");
l = System.currentTimeMillis();
@ -3586,10 +3588,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
StateModelChecker mc = StateModelChecker.createModelChecker(currentModelType, this, currentModel, propertiesFile);
// Pass any additional local settings
// TODO
return mc;
}
/**
* Utility method to create and initialise an (explicit) model checker based on the current model.
* @param propertiesFile Optional properties file for extra info needed during model checking (can be null)
@ -3609,10 +3611,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mc.setStoreVector(storeVector);
mc.setGenStrat(genStrat);
mc.setDoBisim(doBisim);
return mc;
}
/**
* Either create a new PrismFileLog for {@code file} or,
* if {@code file} is null, return {@code mainLog}.

Write Preview
Loading…
Cancel
Save