|
|
@ -1884,7 +1884,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, |
|
|
currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, |
|
|
explicitFilesNumStates); |
|
|
explicitFilesNumStates); |
|
|
} else { |
|
|
} else { |
|
|
throw new PrismException("Explicit import not yet supported for explicit engine"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Explicit import not yet supported for explicit engine"); |
|
|
} |
|
|
} |
|
|
break; |
|
|
break; |
|
|
default: |
|
|
default: |
|
|
@ -2086,7 +2086,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
JDDNode tmp; |
|
|
JDDNode tmp; |
|
|
|
|
|
|
|
|
if (getExplicit()) |
|
|
if (getExplicit()) |
|
|
throw new PrismException("Export to Spy file not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Export to Spy file not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
// Build model, if necessary |
|
|
// Build model, if necessary |
|
|
buildModelIfRequired(); |
|
|
buildModelIfRequired(); |
|
|
@ -2117,7 +2117,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
public void exportToDotFile(File file) throws FileNotFoundException, PrismException |
|
|
public void exportToDotFile(File file) throws FileNotFoundException, PrismException |
|
|
{ |
|
|
{ |
|
|
if (getExplicit()) |
|
|
if (getExplicit()) |
|
|
throw new PrismException("Export to Dot file not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Export to Dot file not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
// Build model, if necessary |
|
|
// Build model, if necessary |
|
|
buildModelIfRequired(); |
|
|
buildModelIfRequired(); |
|
|
@ -2180,7 +2180,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
currentModelExpl.exportToPrismExplicitTra(tmpLog); |
|
|
currentModelExpl.exportToPrismExplicitTra(tmpLog); |
|
|
break; |
|
|
break; |
|
|
case Prism.EXPORT_MATLAB: |
|
|
case Prism.EXPORT_MATLAB: |
|
|
throw new PrismException("Export not yet supported"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Export not yet supported"); |
|
|
case Prism.EXPORT_DOT: |
|
|
case Prism.EXPORT_DOT: |
|
|
currentModelExpl.exportToDotFile(tmpLog); |
|
|
currentModelExpl.exportToDotFile(tmpLog); |
|
|
break; |
|
|
break; |
|
|
@ -2189,7 +2189,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
break; |
|
|
break; |
|
|
case Prism.EXPORT_MRMC: |
|
|
case Prism.EXPORT_MRMC: |
|
|
case Prism.EXPORT_ROWS: |
|
|
case Prism.EXPORT_ROWS: |
|
|
throw new PrismException("Export not yet supported"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Export not yet supported"); |
|
|
} |
|
|
} |
|
|
tmpLog.close(); |
|
|
tmpLog.close(); |
|
|
} |
|
|
} |
|
|
@ -2222,7 +2222,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
String s; |
|
|
String s; |
|
|
|
|
|
|
|
|
if (getExplicit()) |
|
|
if (getExplicit()) |
|
|
throw new PrismException("Export of state rewards not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
throw new PrismNotSupportedException("Export of state rewards not yet supported by explicit engine"); |
|
|
|
|
|
|
|
|
// rows format does not apply to vectors |
|
|
// rows format does not apply to vectors |
|
|
if (exportType == EXPORT_ROWS) |
|
|
if (exportType == EXPORT_ROWS) |
|
|
|