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

Push exportprism and exportprismconst options from PrismCL into Prism. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4564 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
8f45a5d491
commit
7ee82b3b13
2 changed files with 86 additions and 58 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. 95
      prism/src/prism/Prism.java
  2. 49
      prism/src/prism/PrismCL.java

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

@ -116,14 +116,19 @@ public class Prism implements PrismSettingsListener
// Main PRISM settings
private PrismSettings settings;
// Export parsed PRISM model?
protected boolean exportPrism = false;
protected String exportPrismFilename = null;
protected boolean exportPrismConst = false;
protected String exportPrismConstFilename = null;
// Export target state info?
protected boolean exportTarget;
protected String exportTargetFilename;
protected boolean exportTarget = false;
protected String exportTargetFilename = null;
// Export product model info?
protected boolean exportProductTrans;
protected String exportProductTransFilename;
protected boolean exportProductStates;
protected String exportProductStatesFilename;
protected boolean exportProductTrans = false;
protected String exportProductTransFilename = null;
protected boolean exportProductStates = false;
protected String exportProductStatesFilename = null;
// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
// See constructor below for default values
@ -230,12 +235,6 @@ public class Prism implements PrismSettingsListener
modelListeners = new ArrayList<PrismModelListener>();
// default values for miscellaneous options
exportTarget = false;
exportTargetFilename = null;
exportProductTrans = false;
exportProductTransFilename = null;
exportProductStates = false;
exportProductStatesFilename = null;
doReach = true;
bsccComp = true;
checkZeroLoops = false;
@ -413,6 +412,26 @@ public class Prism implements PrismSettingsListener
// Set methods for miscellaneous options
public void setExportPrism(boolean b) throws PrismException
{
exportPrism = b;
}
public void setExportPrismFilename(String s) throws PrismException
{
exportPrismFilename = s;
}
public void setExportPrismConst(boolean b) throws PrismException
{
exportPrismConst = b;
}
public void setExportPrismConstFilename(String s) throws PrismException
{
exportPrismConstFilename = s;
}
public void setExportTarget(boolean b) throws PrismException
{
exportTarget = b;
@ -643,6 +662,26 @@ public class Prism implements PrismSettingsListener
// Get methods for miscellaneous options
public boolean getExportPrism()
{
return exportPrism;
}
public String getExportPrismFilename()
{
return exportPrismFilename;
}
public boolean getExportPrismConst()
{
return exportPrismConst;
}
public String getExportPrismConstFilename()
{
return exportPrismConstFilename;
}
public boolean getExportTarget()
{
return exportTarget;
@ -1382,6 +1421,20 @@ public class Prism implements PrismSettingsListener
mainLog.print(currentModulesFile.getVarName(i) + " ");
}
mainLog.println();
// If required, export parsed PRISM model
if (exportPrism) {
try {
File f = (exportPrismFilename.equals("stdout")) ? null : new File(exportPrismFilename);
exportPRISMModel(f);
}
// In case of error, just print a warning
catch (FileNotFoundException e) {
mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismFilename + "\" for output");
} catch (PrismException e) {
mainLog.printWarning("PRISM code export failed: " + e.getMessage());
}
}
}
/**
@ -1400,6 +1453,20 @@ public class Prism implements PrismSettingsListener
// Reset dependent info
currentModel = null;
currentModelExpl = null;
// If required, export parsed PRISM model, with constants expanded
if (exportPrismConst) {
try {
File f = (exportPrismConstFilename.equals("stdout")) ? null : new File(exportPrismConstFilename);
exportPRISMModelWithExpandedConstants(f);
}
// In case of error, just print a warning
catch (FileNotFoundException e) {
mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismFilename + "\" for output");
} catch (PrismException e) {
mainLog.printWarning("PRISM code export failed: " + e.getMessage());
}
}
}
/**
@ -2677,7 +2744,7 @@ public class Prism implements PrismSettingsListener
/**
* Get a string describing an output format, e.g. "in plain text format" for EXPORT_PLAIN.
*/
private static String getStringForExportType(int exportType) throws PrismException
private static String getStringForExportType(int exportType)
{
switch (exportType) {
case EXPORT_PLAIN:
@ -2701,7 +2768,7 @@ public class Prism implements PrismSettingsListener
* Get a string describing the output destination specified by a File:
* "to file \"filename\"..." if non-null; "below:" if null
*/
private static String getDestinationStringForFile(File file) throws PrismException
private static String getDestinationStringForFile(File file)
{
return (file == null) ? "below:" : "to file \"" + file + "\"...";
}

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

@ -59,8 +59,6 @@ public class PrismCL
private boolean exportresults = false;
private boolean exportresultsmatrix = false;
private boolean exportresultscsv = false;
private boolean exportprism = false;
private boolean exportprismconst = false;
private boolean exportPlainDeprecated = false;
private int exportType = Prism.EXPORT_PLAIN;
private boolean exportordered = true;
@ -108,8 +106,6 @@ public class PrismCL
private String exportResultsFilename = null;
private String exportSteadyStateFilename = null;
private String exportTransientFilename = null;
private String exportPrismFilename = null;
private String exportPrismConstFilename = null;
private String simpathFilename = null;
// logs
@ -241,8 +237,7 @@ public class PrismCL
}
}
// Do any exports of code/model
doPrismLangExports();
// Do any model exports
doExports();
// Do steady-state/transient probability computation, if required
@ -547,40 +542,6 @@ public class PrismCL
}
}
/**
* Do any exports of PRISM code that have been requested.
*/
private void doPrismLangExports()
{
// output parsed prism model here if required
if (exportprism) {
try {
File f = (exportPrismFilename.equals("stdout")) ? null : new File(exportPrismFilename);
prism.exportPRISMModel(f);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
error("Couldn't open file \"" + exportPrismFilename + "\" for output");
} catch (PrismException e) {
error(e.getMessage());
}
}
// output parsed prism model, with constants, here if required
if (exportprismconst) {
try {
File f = (exportPrismConstFilename.equals("stdout")) ? null : new File(exportPrismConstFilename);
prism.exportPRISMModelWithExpandedConstants(f);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
error("Couldn't open file \"" + exportPrismConstFilename + "\" for output");
} catch (PrismException e) {
error(e.getMessage());
}
}
}
/**
* Build a model, usually from the passed in modulesFileToBuild. However, if importtrans=true,
* then explicit model import is done and modulesFileToBuild can be null.
@ -1198,8 +1159,8 @@ public class PrismCL
// export prism model to file
else if (sw.equals("exportprism")) {
if (i < args.length - 1) {
exportprism = true;
exportPrismFilename = args[++i];
prism.setExportPrism(true);
prism.setExportPrismFilename(args[++i]);
} else {
errorAndExit("No file specified for -" + sw + " switch");
}
@ -1207,8 +1168,8 @@ public class PrismCL
// export prism model to file (with consts expanded)
else if (sw.equals("exportprismconst")) {
if (i < args.length - 1) {
exportprismconst = true;
exportPrismConstFilename = args[++i];
prism.setExportPrismConst(true);
prism.setExportPrismConstFilename(args[++i]);
} else {
errorAndExit("No file specified for -" + sw + " switch");
}

Write Preview
Loading…
Cancel
Save