diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 19010969..5017f960 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -142,7 +142,7 @@ public class ConstructModel extends PrismComponent VarList varList = modulesFile.createVarList(); if (varList.containsUnboundedVariables()) mainLog.printWarning("Model contains one or more unbounded variables: model construction may not terminate"); - + // Starting reachability... mainLog.print("\nComputing reachable states..."); mainLog.flush(); @@ -170,6 +170,10 @@ public class ConstructModel extends PrismComponent case CTMDP: modelSimple = ctmdp = new CTMDPSimple(); break; + case STPG: + case SMG: + case PTA: + throw new PrismException("Model construction not supported for " + modelType + "s"); } } @@ -213,8 +217,8 @@ public class ConstructModel extends PrismComponent // Look at each outgoing choice in turn nc = engine.getNumChoices(); for (i = 0; i < nc; i++) { - - if (!justReach && (modelType == ModelType.MDP || modelType == ModelType.CTMDP)) { + // For nondet models, collect transitions in a Distribution + if (!justReach && modelType.nondeterministic()) { distr = new Distribution(); } // Look at each transition in the choice @@ -242,14 +246,17 @@ public class ConstructModel extends PrismComponent ctmc.addToProbability(src, dest, engine.getTransitionProbability(i, j)); break; case MDP: - distr.add(dest, engine.getTransitionProbability(i, j)); - break; case CTMDP: distr.add(dest, engine.getTransitionProbability(i, j)); break; + case STPG: + case SMG: + case PTA: + throw new PrismException("Model construction not supported for " + modelType + "s"); } } } + // For nondet models, add collated transition to model if (!justReach) { if (modelType == ModelType.MDP) { if (distinguishActions) { @@ -319,6 +326,10 @@ public class ConstructModel extends PrismComponent case CTMDP: model = sort ? new CTMDPSimple(ctmdp, permut) : mdp; break; + case STPG: + case SMG: + case PTA: + throw new PrismException("Model construction not supported for " + modelType + "s"); } model.setStatesList(statesList); model.setConstantValues(new Values(modulesFile.getConstantValues()));