From 81451753d16d268d547a7567b598f98af3769727 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 25 Aug 2016 23:10:59 +0000 Subject: [PATCH] Bug fix for explicit engine model import - we should not assume that the initial state is 0. This also highlights a bug that ModelExplicit should store initial states as a state, not a list, but that issue is not fixed here. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11744 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 3 ++- prism/src/explicit/DTMCModelChecker.java | 1 + prism/src/explicit/DTMCSimple.java | 2 -- prism/src/explicit/MDPSimple.java | 2 -- prism/src/explicit/ModelExplicit.java | 2 ++ prism/src/explicit/PrismSTPGAbstractRefine.java | 1 + 6 files changed, 6 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index fc199bf6..51917514 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -933,7 +933,8 @@ public class CTMCModelChecker extends ProbModelChecker mc = new CTMCModelChecker(null); ctmc = new CTMCSimple(); ctmc.buildFromPrismExplicit(args[0]); - //System.out.println(dtmc); + ctmc.addInitialState(0); + //System.out.println(ctmc); labels = mc.loadLabelsFile(args[1]); //System.out.println(labels); target = labels.get(args[2]); diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 70e90811..d72741f4 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -1622,6 +1622,7 @@ public class DTMCModelChecker extends ProbModelChecker mc = new DTMCModelChecker(null); dtmc = new DTMCSimple(); dtmc.buildFromPrismExplicit(args[0]); + dtmc.addInitialState(0); //System.out.println(dtmc); Map labels = mc.loadLabelsFile(args[1]); //System.out.println(labels); diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index f9516f45..017314b6 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -172,8 +172,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple } catch (NumberFormatException e) { throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + getModelType()); } - // Set initial state (assume 0) - initialStates.add(0); } // Mutators (other) diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 59e16506..875c9875 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -370,8 +370,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple } catch (NumberFormatException e) { throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + getModelType()); } - // Set initial state (assume 0) - initialStates.add(0); } // Mutators (other) diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 5a4f068b..f44afb7a 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -163,6 +163,8 @@ public abstract class ModelExplicit implements Model /** * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file). + * Note that initial states are not configured (since this info is not in the file), + * so this needs to be done separately (using {@link #addInitialState(int)}. */ public abstract void buildFromPrismExplicit(String filename) throws PrismException; diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 7bcf2168..88a3ace6 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -95,6 +95,7 @@ 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());