|
|
@ -2787,6 +2787,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
currentModulesFile = dc.getNewModulesFile(); |
|
|
currentModulesFile = dc.getNewModulesFile(); |
|
|
currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues()); |
|
|
currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues()); |
|
|
currentModelType = ModelType.MDP; |
|
|
currentModelType = ModelType.MDP; |
|
|
|
|
|
clearBuiltModel(); |
|
|
currentModel = null; |
|
|
currentModel = null; |
|
|
currentModelExpl = null; |
|
|
currentModelExpl = null; |
|
|
// If required, export generated PRISM model |
|
|
// If required, export generated PRISM model |
|
|
@ -2806,6 +2807,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener |
|
|
digital = false; |
|
|
digital = false; |
|
|
currentModulesFile = oldModulesFile; |
|
|
currentModulesFile = oldModulesFile; |
|
|
currentModelType = ModelType.PTA; |
|
|
currentModelType = ModelType.PTA; |
|
|
|
|
|
clearBuiltModel(); |
|
|
currentModel = null; |
|
|
currentModel = null; |
|
|
currentModelExpl = null; |
|
|
currentModelExpl = null; |
|
|
} |
|
|
} |
|
|
|