diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2c20f656..5465542d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -892,7 +892,7 @@ public class Prism implements PrismSettingsListener // get rid of non det vars if necessary tmp = model.getTrans(); JDD.Ref(tmp); - if (model instanceof NondetModel) + if (model.getType() == Model.MDP) { tmp = JDD.MaxAbstract(tmp, ((NondetModel)model).getAllDDNondetVars()); } @@ -922,7 +922,7 @@ public class Prism implements PrismSettingsListener public void exportTransToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException { // can only do ordered version of export for MDPs - if (model instanceof NondetModel) { + if (model.getType() == Model.MDP) { if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix for MDPs; using ordered."); ordered = true; } @@ -982,7 +982,7 @@ public class Prism implements PrismSettingsListener String s; // can only do ordered version of export for MDPs - if (model instanceof NondetModel) { + if (model.getType() == Model.MDP) { if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition reward matrix for MDPs; using ordered"); ordered = true; } @@ -1135,24 +1135,21 @@ public class Prism implements PrismSettingsListener // Check that property is valid for this model type // and create new model checker object - if (model instanceof ProbModel) - { + switch (model.getType()) { + case Model.DTMC: expr.checkValid(ModulesFile.PROBABILISTIC); mc = new ProbModelChecker(this, model, propertiesFile); - } - else if (model instanceof NondetModel) - { + break; + case Model.MDP: expr.checkValid(ModulesFile.NONDETERMINISTIC); mc = new NondetModelChecker(this, model, propertiesFile); - } - else if (model instanceof StochModel) - { + break; + case Model.CTMC: expr.checkValid(ModulesFile.STOCHASTIC); mc = new StochModelChecker(this, model, propertiesFile); - } - else - { - throw new PrismException("Unknown model type"); + break; + default: + throw new PrismException("Unknown model type"+model.getType()); } // Do model checking @@ -1282,11 +1279,11 @@ public class Prism implements PrismSettingsListener mainLog.println("\nComputing steady-state probabilities..."); l = System.currentTimeMillis(); - if (model instanceof ProbModel) { + if (model.getType() == Model.DTMC) { mc = new ProbModelChecker(this, model, null); probs = ((ProbModelChecker)mc).doSteadyState(); } - else if (model instanceof StochModel) { + else if (model.getType() == Model.DTMC) { mc = new StochModelChecker(this, model, null); probs = ((StochModelChecker)mc).doSteadyState(); } @@ -1319,12 +1316,12 @@ public class Prism implements PrismSettingsListener l = System.currentTimeMillis(); - if (model instanceof ProbModel) { + if (model.getType() == Model.DTMC) { mainLog.println("\nComputing transient probabilities (time = " + (int)time + ")..."); mc = new ProbModelChecker(this, model, null); probs = ((ProbModelChecker)mc).doTransient((int)time); } - else if (model instanceof StochModel) { + else if (model.getType() == Model.CTMC) { mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); mc = new StochModelChecker(this, model, null); probs = ((StochModelChecker)mc).doTransient(time); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 37ad8205..179bc42e 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -679,7 +679,7 @@ public class PrismCL private void doSteadyState() throws PrismException { // compute steady-state probabilities - if (model instanceof StochModel || model instanceof ProbModel) { + if (model.getType() == Model.CTMC || model.getType() == Model.DTMC) { prism.doSteadyState(model); } else { @@ -695,7 +695,7 @@ public class PrismCL int i; // compute transient probabilities - if (model instanceof StochModel) { + if (model.getType() == Model.CTMC) { try { d = Double.parseDouble(transientTime); } @@ -704,7 +704,7 @@ public class PrismCL } prism.doTransient(model, d); } - else if (model instanceof ProbModel) { + else if (model.getType() == Model.DTMC) { try { i = Integer.parseInt(transientTime); } diff --git a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java index 5048141d..9d2b18c8 100644 --- a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java +++ b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java @@ -64,7 +64,8 @@ public class ComputeSteadyStateThread extends GUIComputationThread //Do Computation try { - if(!(computeThis instanceof StochModel || computeThis instanceof ProbModel)) throw new PrismException("Can only compute steady-state probabilities for CTMCs"); + if (!(computeThis.getType() == Model.CTMC || computeThis.getType() == Model.DTMC)) + throw new PrismException("Can only compute steady-state probabilities for CTMCs"); prism.doSteadyState(computeThis); } catch(PrismException e) diff --git a/prism/src/userinterface/model/computation/ComputeTransientThread.java b/prism/src/userinterface/model/computation/ComputeTransientThread.java index bc7e792c..497f5174 100644 --- a/prism/src/userinterface/model/computation/ComputeTransientThread.java +++ b/prism/src/userinterface/model/computation/ComputeTransientThread.java @@ -66,7 +66,8 @@ public class ComputeTransientThread extends GUIComputationThread //Do Computation try { - if(!(computeThis instanceof StochModel || computeThis instanceof ProbModel)) throw new PrismException("Can only compute transient probabilities for DTMCs/CTMCs"); + if (!(computeThis.getType() == Model.CTMC || computeThis.getType() == Model.DTMC)) + throw new PrismException("Can only compute transient probabilities for DTMCs/CTMCs"); plug.getPrism().doTransient(computeThis, transientTime); } catch(PrismException e)