From 890620fd5f23de230e8d5c7dd6761251a93e6ed7 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 26 Aug 2016 06:48:38 +0000 Subject: [PATCH] PrismSTPGAbstractRefine: set initial states from the label file git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11748 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/PrismSTPGAbstractRefine.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 02ba0805..7cc931f4 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -28,6 +28,7 @@ package explicit; import java.util.*; +import common.IterableStateSet; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; @@ -95,7 +96,6 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine throw new PrismNotSupportedException("Cannot handle model type " + modelType); } modelConcrete.buildFromPrismExplicit(traFile); - modelConcrete.addInitialState(0); if (buildEmbeddedDtmc) { // TODO: do more efficiently (straight from tra file?) mainLog.println("Concrete " + "CTMC" + ": " + modelConcrete.infoString()); @@ -124,6 +124,11 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine if (targetConcrete == null) throw new PrismException("Unknown label \"" + targetLabel + "\""); + // set the initial states from the set initialConcrete + for (int state : new IterableStateSet(initialConcrete, modelConcrete.getNumStates())) { + modelConcrete.addInitialState(state); + } + // If the 'exact' flag is set, just do model checking on the concrete model (no abstraction) if (exact) { doExactModelChecking();