From 55c0034a18637081a02c3ca76581e5f87d6f026b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 26 Aug 2016 06:28:35 +0000 Subject: [PATCH] explicit model import: some more minor fixes to set correct initial states Followup to SVN 11744. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11746 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMDPModelChecker.java | 1 + prism/src/explicit/MDPModelChecker.java | 1 + prism/src/explicit/ModelSimple.java | 2 ++ prism/src/explicit/PrismExplicit.java | 1 + prism/src/explicit/STPGAbstrSimple.java | 2 -- prism/src/explicit/STPGModelChecker.java | 1 + 6 files changed, 6 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 16681a7d..53a973ac 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -284,6 +284,7 @@ public class CTMDPModelChecker extends ProbModelChecker mc = new CTMDPModelChecker(null); ctmdp = new CTMDPSimple(); ctmdp.buildFromPrismExplicit(args[0]); + ctmdp.addInitialState(0); System.out.println(ctmdp); labels = mc.loadLabelsFile(args[1]); System.out.println(labels); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 517e445c..edec0848 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -1754,6 +1754,7 @@ public class MDPModelChecker extends ProbModelChecker mc = new MDPModelChecker(null); mdp = new MDPSimple(); mdp.buildFromPrismExplicit(args[0]); + mdp.addInitialState(0); //System.out.println(mdp); labels = mc.loadLabelsFile(args[1]); //System.out.println(labels); diff --git a/prism/src/explicit/ModelSimple.java b/prism/src/explicit/ModelSimple.java index 4ef2ba47..5b9ddd48 100644 --- a/prism/src/explicit/ModelSimple.java +++ b/prism/src/explicit/ModelSimple.java @@ -44,6 +44,8 @@ public interface ModelSimple extends 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/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index f35e90fa..d20885e4 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -464,6 +464,7 @@ public class PrismExplicit extends PrismComponent prism.exportLabelsToFile(null, Prism.EXPORT_PLAIN, new File("tmp.lab")); DTMCSimple modelExplicit = new DTMCSimple(); modelExplicit.buildFromPrismExplicit("tmp.tra"); + modelExplicit.addInitialState(0); PrismExplicit pe = new PrismExplicit(prism.getMainLog(), prism.getSettings()); pe.modelCheck(modelExplicit, null, propertiesFile, propertiesFile.getProperty(0)); } catch (PrismException e) { diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index de4ea1b0..1d9ce338 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -227,8 +227,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } 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/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index ce6f518e..b5fce8d8 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -918,6 +918,7 @@ public class STPGModelChecker extends ProbModelChecker mc = new STPGModelChecker(null); stpg = new STPGAbstrSimple(); stpg.buildFromPrismExplicit(args[0]); + stpg.addInitialState(0); //System.out.println(stpg); labels = mc.loadLabelsFile(args[1]); //System.out.println(labels);