Browse Source

Code tidy (incl. remove warnings) to help with merging.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8783 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
commit
8ce321ffb9
  1. 19
      prism/src/explicit/ConstructModel.java

19
prism/src/explicit/ConstructModel.java

@ -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()));

Loading…
Cancel
Save