diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 43d38d10..7c71e066 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -9,14 +9,15 @@ import jltl2ba.SimpleLTL; import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import prism.ModelInfo; import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; @SuppressWarnings({"unused", "static-access", "serial"}) public class PrismParser implements PrismParserConstants { - // The modules file associated with properties file being parsed - private static ModulesFile modulesFile; + // The model associated with the properties file being parsed + private static ModelInfo modelInfo; // List of keyword strings private static ArrayList keywordList = new ArrayList(); @@ -157,16 +158,16 @@ public class PrismParser implements PrismParserConstants { // Parse properties file (pass ModulesFile in to get at its constants) - public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str) throws PrismLangException - { return parsePropertiesFile(mf, str, false); } + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, InputStream str) throws PrismLangException + { return parsePropertiesFile(modelInfo, str, false); } - public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str, boolean strict) throws PrismLangException + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, InputStream str, boolean strict) throws PrismLangException { PropertiesFile pf = null; // (Re)start parser ReInit(str); - modulesFile = mf; + this.modelInfo = modelInfo; // Parse try { pf = strict ? PropertiesFile() : PropertiesFileSemicolonless(); @@ -490,7 +491,7 @@ public class PrismParser implements PrismParserConstants { // Properties file static final public PropertiesFile PropertiesFile() throws ParseException, PrismLangException { - PropertiesFile pf = new PropertiesFile(modulesFile); + PropertiesFile pf = new PropertiesFile(modelInfo); Property prop; Token begin = null; begin = getToken(1); @@ -592,7 +593,7 @@ public class PrismParser implements PrismParserConstants { // Properties file with optional semicolons - beware of potential ambiguities static final public PropertiesFile PropertiesFileSemicolonless() throws ParseException, PrismLangException { - PropertiesFile pf = new PropertiesFile(modulesFile); + PropertiesFile pf = new PropertiesFile(modelInfo); Property prop; Token begin = null; begin = getToken(1); @@ -3502,17 +3503,6 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(17, xla); } } - static private boolean jj_3R_187() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; - return false; - } - - static private boolean jj_3R_48() { - if (jj_scan_token(REG_IDENTPRIME)) return true; - return false; - } - static private boolean jj_3R_164() { if (jj_3R_29()) return true; return false; @@ -5127,6 +5117,17 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_187() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_38()) return true; + return false; + } + + static private boolean jj_3R_48() { + if (jj_scan_token(REG_IDENTPRIME)) return true; + return false; + } + static private boolean jj_initialized_once = false; /** Generated Token Manager. */ static public PrismParserTokenManager token_source; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 50fa48a1..a7850125 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -41,6 +41,7 @@ import jltl2ba.SimpleLTL; import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import prism.ModelInfo; import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; @@ -48,8 +49,8 @@ import prism.PrismLangException; @SuppressWarnings({"unused", "static-access", "serial"}) public class PrismParser { - // The modules file associated with properties file being parsed - private static ModulesFile modulesFile; + // The model associated with the properties file being parsed + private static ModelInfo modelInfo; // List of keyword strings private static ArrayList keywordList = new ArrayList(); @@ -190,16 +191,16 @@ public class PrismParser // Parse properties file (pass ModulesFile in to get at its constants) - public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str) throws PrismLangException - { return parsePropertiesFile(mf, str, false); } + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, InputStream str) throws PrismLangException + { return parsePropertiesFile(modelInfo, str, false); } - public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str, boolean strict) throws PrismLangException + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, InputStream str, boolean strict) throws PrismLangException { PropertiesFile pf = null; // (Re)start parser ReInit(str); - modulesFile = mf; + this.modelInfo = modelInfo; // Parse try { pf = strict ? PropertiesFile() : PropertiesFileSemicolonless(); @@ -586,7 +587,7 @@ ModulesFile ModulesFile() throws PrismLangException : PropertiesFile PropertiesFile() throws PrismLangException : { - PropertiesFile pf = new PropertiesFile(modulesFile); + PropertiesFile pf = new PropertiesFile(modelInfo); Property prop; Token begin = null; } @@ -606,7 +607,7 @@ PropertiesFile PropertiesFile() throws PrismLangException : PropertiesFile PropertiesFileSemicolonless() throws PrismLangException : { - PropertiesFile pf = new PropertiesFile(modulesFile); + PropertiesFile pf = new PropertiesFile(modelInfo); Property prop; Token begin = null; } diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index 190db239..6920535b 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -7,6 +7,7 @@ import jltl2ba.SimpleLTL; import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import prism.ModelInfo; import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 3fc8006a..92301995 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -30,6 +30,7 @@ import java.util.*; import parser.*; import parser.visitor.*; +import prism.ModelInfo; import prism.PrismLangException; import prism.PrismUtils; @@ -39,6 +40,7 @@ public class PropertiesFile extends ASTElement { // Associated ModulesFile (for constants, ...) private ModulesFile modulesFile; + private ModelInfo modelInfo; // Components private FormulaList formulaList; @@ -55,9 +57,9 @@ public class PropertiesFile extends ASTElement // Constructor - public PropertiesFile(ModulesFile mf) + public PropertiesFile(ModelInfo modelInfo) { - setModulesFile(mf); + setModelInfo(modelInfo); formulaList = new FormulaList(); labelList = new LabelList(); combinedLabelList = new LabelList(); @@ -70,9 +72,19 @@ public class PropertiesFile extends ASTElement // Set methods /** Attach to a ModulesFile (so can access labels/constants etc.) */ - public void setModulesFile(ModulesFile mf) - { - this.modulesFile = mf; + public void setModelInfo(ModelInfo modelInfo) + { + // Store ModelInfo + this.modelInfo = modelInfo; + // If the ModelInfo is not a ModulesFile, we need to create a balnk one + if (modelInfo instanceof ModulesFile) { + this.modulesFile = (ModulesFile) modelInfo; + } else { + ModulesFile mf = new ModulesFile(); + mf.setFormulaList(new FormulaList()); + mf.setConstantList(new ConstantList()); + this.modulesFile = mf; + } } public void setFormulaList(FormulaList fl) @@ -447,7 +459,7 @@ public class PropertiesFile extends ASTElement */ private void doSemanticChecks() throws PrismLangException { - PropertiesSemanticCheck visitor = new PropertiesSemanticCheck(this, modulesFile); + PropertiesSemanticCheck visitor = new PropertiesSemanticCheck(this, modelInfo); accept(visitor); } @@ -612,7 +624,7 @@ public class PropertiesFile extends ASTElement public ASTElement deepCopy() { int i, n; - PropertiesFile ret = new PropertiesFile(modulesFile); + PropertiesFile ret = new PropertiesFile(modelInfo); // Copy ASTElement stuff ret.setPosition(this); // Deep copy main components diff --git a/prism/src/parser/visitor/PropertiesSemanticCheck.java b/prism/src/parser/visitor/PropertiesSemanticCheck.java index a3c38bf2..2709fced 100644 --- a/prism/src/parser/visitor/PropertiesSemanticCheck.java +++ b/prism/src/parser/visitor/PropertiesSemanticCheck.java @@ -38,6 +38,7 @@ import parser.ast.FormulaList; import parser.ast.LabelList; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; +import prism.ModelInfo; import prism.PrismLangException; /** @@ -48,6 +49,7 @@ import prism.PrismLangException; public class PropertiesSemanticCheck extends SemanticCheck { private PropertiesFile propertiesFile; + private ModelInfo modelInfo; private ModulesFile modulesFile; public PropertiesSemanticCheck(PropertiesFile propertiesFile) @@ -55,10 +57,10 @@ public class PropertiesSemanticCheck extends SemanticCheck this(propertiesFile, null); } - public PropertiesSemanticCheck(PropertiesFile propertiesFile, ModulesFile modulesFile) + public PropertiesSemanticCheck(PropertiesFile propertiesFile, ModelInfo modelInfo) { setPropertiesFile(propertiesFile); - setModulesFile(modulesFile); + setModelInfo(modelInfo); } public void setPropertiesFile(PropertiesFile propertiesFile) @@ -66,9 +68,14 @@ public class PropertiesSemanticCheck extends SemanticCheck this.propertiesFile = propertiesFile; } - public void setModulesFile(ModulesFile modulesFile) + public void setModelInfo(ModelInfo modelInfo) { - this.modulesFile = modulesFile; + this.modelInfo = modelInfo; + if (modelInfo instanceof ModulesFile) { + this.modulesFile = (ModulesFile) modelInfo; + } else { + this.modulesFile = null; + } } public Object visit(FormulaList e) throws PrismLangException @@ -191,21 +198,20 @@ public class PropertiesSemanticCheck extends SemanticCheck public void visitPost(ExpressionLabel e) throws PrismLangException { - LabelList labelList; - if (propertiesFile != null) - labelList = propertiesFile.getCombinedLabelList(); - else if (modulesFile != null) - labelList = modulesFile.getLabelList(); - else - throw new PrismLangException("Undeclared label", e); String name = e.getName(); // Allow special cases if ("deadlock".equals(name) || "init".equals(name)) return; - // Otherwise check list - if (labelList == null || labelList.getLabelIndex(name) == -1) { - throw new PrismLangException("Undeclared label", e); + // Otherwise check if it exists + if (modelInfo != null && modelInfo.getLabelIndex(name) != -1) { + return; + } else if (propertiesFile != null) { + LabelList labelList = propertiesFile.getCombinedLabelList(); + if (labelList != null && labelList.getLabelIndex(name) != -1) { + return; + } } + throw new PrismLangException("Undeclared label", e); } public void visitPost(ExpressionFilter e) throws PrismLangException diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b842df05..98f82aa5 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -48,10 +48,8 @@ import parser.ExplicitFiles2ModulesFile; import parser.PrismParser; import parser.State; import parser.Values; -import parser.ast.ConstantList; import parser.ast.Expression; import parser.ast.ForLoop; -import parser.ast.FormulaList; import parser.ast.LabelList; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; @@ -248,7 +246,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener //------------------------------------------------------------------------------ private enum ModelSource { - PRISM_MODEL, EXPLICIT_FILES, BUILT_MODEL + PRISM_MODEL, MODEL_GENERATOR, EXPLICIT_FILES, BUILT_MODEL } // Info about currently loaded model, if any @@ -256,8 +254,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener private ModelSource currentModelSource = ModelSource.PRISM_MODEL; // Model type private ModelType currentModelType = null; - // PRISM model (null if none loaded, or built model given directly) + // PRISM model (null if none loaded) private ModulesFile currentModulesFile = null; + // Model generator (null if none loaded) + private ModelGenerator currentModelGenerator = null; // Constants to be defined for PRISM model private Values currentDefinedMFConstants = null; // Built model storage - symbolic or explicit - at most one is non-null @@ -1507,26 +1507,26 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Parse a PRISM properties file. Typically, you need to pass in the corresponding PRISM model - * (for access to constants, etc.) but if left null, a blank one is created automatically. - * @param mf Accompanying ModulesFile (null if not needed) + * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model + * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. + * @param modelInfo Accompanying model info (null if not needed) * @param file File to read in */ - public PropertiesFile parsePropertiesFile(ModulesFile mf, File file) throws FileNotFoundException, PrismLangException + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, File file) throws FileNotFoundException, PrismLangException { - return parsePropertiesFile(mf, file, true); + return parsePropertiesFile(modelInfo, file, true); } /** - * Parse a PRISM properties file. Typically, you need to pass in the corresponding PRISM model - * (for access to constants, etc.) but if left null, a blank one is created automatically. + * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model + * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. * You can also choose whether to do "tidy", i.e. post-parse checks and processing * (this must be done at some point but may want to postpone to allow parsing of files with errors). - * @param mf Accompanying ModulesFile (null if not needed) + * @param modelInfo Accompanying model info (null if not needed) * @param file File to read in * @param tidy Whether or not to do "tidy" (post-parse checks and processing) */ - public PropertiesFile parsePropertiesFile(ModulesFile mf, File file, boolean tidy) throws FileNotFoundException, PrismLangException + public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, File file, boolean tidy) throws FileNotFoundException, PrismLangException { FileInputStream strProperties; PrismParser prismParser; @@ -1535,20 +1535,13 @@ public class Prism extends PrismComponent implements PrismSettingsListener // open file strProperties = new FileInputStream(file); - // if null modules file passed, create a blank one - if (mf == null) { - mf = new ModulesFile(); - mf.setFormulaList(new FormulaList()); - mf.setConstantList(new ConstantList()); - } - try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) prismParser = getPrismParser(); try { // parse file - propertiesFile = prismParser.parsePropertiesFile(mf, strProperties); + propertiesFile = prismParser.parsePropertiesFile(modelInfo, strProperties); } finally { // release prism parser releasePrismParser(); @@ -1564,30 +1557,23 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Parse a PRISM properties file from a string. Typically, you need to pass in the corresponding PRISM model - * (for access to constants, etc.) but if left null, a blank one is created automatically. - * @param mf Accompanying ModulesFile (null if not needed) + * Parse a PRISM properties file form a string. Typically, you need to pass in some info about the corresponding model + * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. + * @param modelInfo Accompanying model info (null if not needed) * @param s String to parse */ - public PropertiesFile parsePropertiesString(ModulesFile mf, String s) throws PrismLangException + public PropertiesFile parsePropertiesString(ModelInfo modelInfo, String s) throws PrismLangException { PrismParser prismParser; PropertiesFile propertiesFile = null; - // if null modules file passed, create a blank one - if (mf == null) { - mf = new ModulesFile(); - mf.setFormulaList(new FormulaList()); - mf.setConstantList(new ConstantList()); - } - try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) prismParser = getPrismParser(); try { // parse string - propertiesFile = prismParser.parsePropertiesFile(mf, new ByteArrayInputStream(s.getBytes())); + propertiesFile = prismParser.parsePropertiesFile(modelInfo, new ByteArrayInputStream(s.getBytes())); } finally { // release prism parser releasePrismParser(); @@ -1661,11 +1647,15 @@ public class Prism extends PrismComponent implements PrismSettingsListener * Pass in null to clear storage of the current PRISM model. * @param modulesFile The PRISM model */ - public void loadPRISMModel(ModulesFile modulesFile) + public void loadPRISMModel(ModulesFile modulesFile) throws PrismException { currentModelSource = ModelSource.PRISM_MODEL; // Store PRISM model currentModulesFile = modulesFile; + // Create a model generator for the PRISM model if appropriate - we will use that where possible + if (currentModulesFile.getModelType() != ModelType.PTA) { + currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this); + } // Clear any existing built model(s) clearBuiltModel(); // Reset dependent info @@ -1701,12 +1691,38 @@ public class Prism extends PrismComponent implements PrismSettingsListener } } + /** + * Load a model generator, which will be stored and used for subsequent model checking etc. + * Some model constants can still be undefined at this stage. + * Pass in null to clear storage of the current model. + * @param modelGen The model generator + */ + public void loadModelGenerator(ModelGenerator modelGen) + { + currentModelSource = ModelSource.MODEL_GENERATOR; + // Store model generator + currentModelGenerator = modelGen; + // Clear any existing built model(s) + clearBuiltModel(); + // Reset dependent info + currentModelType = currentModelGenerator == null ? null : currentModelGenerator.getModelType(); + currentDefinedMFConstants = null; + currentModel = null; + currentModelExpl = null; + + // Print basic model info + mainLog.println("\nGenerator: " + currentModelGenerator.getClass().getName()); + mainLog.println("Type: " + currentModelGenerator.getModelType()); + // TODO: print more info + //mainLog.println(); + } + /** * Set (some or all) undefined constants for the currently loaded PRISM model * (assuming they have changed since the last time this was called). * @param definedMFConstants The constant values */ - public void setPRISMModelConstants(Values definedMFConstants) throws PrismLangException + public void setPRISMModelConstants(Values definedMFConstants) throws PrismException { if (currentDefinedMFConstants == null && definedMFConstants == null) return; @@ -1717,7 +1733,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener clearBuiltModel(); // Store constants here and in ModulesFile currentDefinedMFConstants = definedMFConstants; - currentModulesFile.setSomeUndefinedConstants(definedMFConstants); + if (currentModulesFile != null) { + currentModulesFile.setSomeUndefinedConstants(definedMFConstants); + } + if (currentModelGenerator != null) { + currentModelGenerator.setSomeUndefinedConstants(definedMFConstants); + } // Reset dependent info currentModel = null; currentModelExpl = null; @@ -1897,9 +1918,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener clearBuiltModel(); try { - if (currentModulesFile == null) - throw new PrismException("There is no currently loaded PRISM model to build"); - if (currentModelType == ModelType.PTA) { throw new PrismException("You cannot build a PTA model explicitly, only perform model checking"); } @@ -1912,6 +1930,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener l = System.currentTimeMillis(); switch (currentModelSource) { case PRISM_MODEL: + if (currentModulesFile == null) + throw new PrismException("There is no currently loaded PRISM model to build"); if (!getExplicit()) { Modules2MTBDD mod2mtbdd = new Modules2MTBDD(this, currentModulesFile); currentModel = mod2mtbdd.translate(); @@ -1919,11 +1939,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener } else { ConstructModel constructModel = new ConstructModel(this); constructModel.setFixDeadlocks(getFixDeadlocks()); - currentModelExpl = constructModel.constructModel(new ModulesFileModelGenerator(currentModulesFile, this)); + currentModelExpl = constructModel.constructModel(currentModelGenerator); currentModel = null; } // if (...) ... currentModel = buildModelExplicit(currentModulesFile); break; + case MODEL_GENERATOR: + if (currentModelGenerator == null) + throw new PrismException("There is no currently loaded model generator to build"); + if (!getExplicit()) { + mainLog.printWarning("Switching to explicit engine to use model generator"); + setEngine(Prism.EXPLICIT); + } + ConstructModel constructModel = new ConstructModel(this); + constructModel.setFixDeadlocks(getFixDeadlocks()); + currentModelExpl = constructModel.constructModel(currentModelGenerator); + currentModel = null; + // if (...) ... currentModel = buildModelExplicit(currentModulesFile); + break; case EXPLICIT_FILES: if (!getExplicit()) { expf2mtbdd = new ExplicitFiles2MTBDD(this); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index a72522e5..4f0aa77b 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -605,8 +605,12 @@ public class PrismCL implements PrismModelListener } // Load model into PRISM (if not done already) - if (!importtrans) { - prism.loadPRISMModel(modulesFile); + try { + if (!importtrans) { + prism.loadPRISMModel(modulesFile); + } + } catch (PrismException e) { + errorAndExit(e.getMessage()); } } diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java new file mode 100644 index 00000000..9cc29839 --- /dev/null +++ b/prism/src/prism/TestModelGenerator.java @@ -0,0 +1,201 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.io.File; +import java.io.FileNotFoundException; + +import parser.State; +import parser.VarList; +import parser.ast.Declaration; +import parser.ast.DeclarationInt; +import parser.ast.Expression; +import parser.ast.PropertiesFile; +import explicit.ConstructModel; +import explicit.DTMCModelChecker; + +public class TestModelGenerator extends DefaultModelGenerator +{ + protected State exploreState; + protected int x; + protected int n; + + public TestModelGenerator(int n) + { + this.n = n; + } + + @Override + public ModelType getModelType() + { + return ModelType.DTMC; + } + + @Override + public int getNumLabels() + { + return 1; + } + + @Override + public String getLabelName(int i) throws PrismException + { + if (i == 0) { + return "goal"; + } else { + throw new PrismException("Label number \"" + i + "\" not defined"); + } + } + + @Override + public int getLabelIndex(String label) + { + return ("goal".equals(label)) ? 0 : -1; + } + + @Override + public State getInitialState() throws PrismException + { + State s = new State(1); + s.varValues[0] = n/2; + return s; + } + + @Override + public void exploreState(State exploreState) throws PrismException + { + this.exploreState = exploreState; + x = ((Integer) exploreState.varValues[0]).intValue(); + } + + @Override + public State getExploreState() + { + return exploreState; + } + + @Override + public int getNumChoices() throws PrismException + { + return 1; + } + + @Override + public int getNumTransitions(int i) throws PrismException + { + return x > 0 && x < n ? 2 : 1; + } + + @Override + public Object getTransitionAction(int i) throws PrismException + { + return null; + } + + @Override + public Object getTransitionAction(int i, int offset) throws PrismException + { + return null; + } + + @Override + public double getTransitionProbability(int i, int offset) throws PrismException + { + return x > 0 && x < n ? 0.5 : 1.0; + } + + @Override + public State computeTransitionTarget(int i, int offset) throws PrismException + { + State s = new State(1); + if (x == 0 || x == n) { + s.varValues[i] = x; + } else { + s.varValues[i] = (offset == 0) ? x -1 : x + 1; + } + return s; + } + + @Override + public boolean isLabelTrue(int i) throws PrismException + { + if (i == 0) { + return x == n; + } else { + throw new PrismException("Label number \"" + i + "\" not defined"); + } + } + + @Override + public VarList createVarList() + { + VarList varList = new VarList(); + try { + varList.addVar(new Declaration("x", new DeclarationInt(Expression.Int(0), Expression.Int(n))), 0, null); + } catch (PrismLangException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } + return varList; + } + + public static void main(String args[]) + { + try { + Prism prism = new Prism(new PrismPrintStreamLog(System.out)); + + int test = 2; + + if (test == 1) { + // Direct usage of model constructor/checker + TestModelGenerator modelGen = new TestModelGenerator(10); + ConstructModel constructModel = new ConstructModel(prism); + explicit.Model model = constructModel.constructModel(modelGen); + model.exportToDotFile(new PrismFileLog("test.dot"), null, true); + DTMCModelChecker mc = new DTMCModelChecker(prism); + PropertiesFile pf = prism.parsePropertiesString(modelGen, "P=? [F \"goal\"]"); + Expression expr = pf.getProperty(0); + Result res = mc.check(model, expr); + System.out.println(res); + } else { + // Perform model construction/checking via Prism + TestModelGenerator modelGen2 = new TestModelGenerator(10); + prism.loadModelGenerator(modelGen2); + prism.exportTransToFile(true, Prism.EXPORT_DOT_STATES, new File("test2.dot")); + PropertiesFile pf = prism.parsePropertiesString(modelGen2, "P=? [F \"goal\"]"); + Expression expr = pf.getProperty(0); + Result res = prism.modelCheck(pf, expr); + System.out.println(res); + } + + } catch (PrismException e) { + System.err.println("Error: " + e.getMessage()); + } catch (FileNotFoundException e) { + System.err.println("Error: " + e.getMessage()); + } + } +}