diff --git a/prism/README.txt b/prism/README.txt index 8113f52c..85c03367 100644 --- a/prism/README.txt +++ b/prism/README.txt @@ -36,7 +36,6 @@ For source code distributions: If you have problems check the manual, especially the section "Common Problems And Questions". - ------------- DOCUMENTATION ------------- @@ -54,7 +53,6 @@ For other PRISM-related information, see the website: http://www.prismmodelchecker.org/ - --------- LICENSING --------- @@ -71,42 +69,36 @@ library, see: http://vlsi.colorado.edu/~fabio/CUDD/ - ---------------- ACKNOWLEDGEMENTS ---------------- -Currently, development work on PRISM is primarily carried out in the -Department of Computer Science at the University of Oxford. Previously, PRISM -was based in the School of Computer Science at the University of Birmingham. +PRISM was created and is still actively maintained by: -The core team working on PRISM currently comprises: + * Dave Parker (University of Birmingham) + * Gethin Norman (University of Glasgow) + * Marta Kwiatkowska (University of Oxford) - * Dave Parker (Oxford) - * Gethin Norman (Glasgow) - * Marta Kwiatkowska (Oxford) - -Many others have contributed to PRISM. In approximately reverse chronological order: +We gratefully acknowledge contributions to the PRISM code-base from various sources, +including (in approximately reverse chronological order): - * Vojtech Forejt: "Fox-Glynn" implementation, explicit-state model checking - * Christian von Essen: Contributions to explicit-state model checking library * Vincent Nimal: Approximate (simulation-based) model checking techniques * Mark Kattenbelt: Wide range of enhancements/additions, especially in the GUI - * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM + * Carlos Bederian (working with Pedro D'Argenio): LTL model checking for MDPs + * Gethin Norman: Precomputation algorithms, abstraction * Alistair John Strachan: Port to 64-bit architectures * Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM * Charles Harley and Sebastian Vermehren: GUI enhancements * Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms * Stephen Gilmore: Support for the stochastic process algebra PEPA * Paolo Ballarini & Kenneth Chan: Port to Mac OS X - * Andrew Hinton: Original versions of the GUI, Windows-port and simulator - * Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm - + * Andrew Hinton: Original versions of the GUI, Windows port and simulator + * Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm + For more details see: http://www.prismmodelchecker.org/people.php - ------- CONTACT ------- @@ -118,12 +110,10 @@ If you have problems or questions regarding PRISM, please use the help forum pro Other comments and feedback about any aspect of PRISM are also very welcome. Please contact: Dave Parker - (david.parker@cs.ox.ac.uk) - Department of Computer Science - University of Oxford - Wolfson Building - Parks Road - Oxford - OX1 3QD + (d.a.parker@cs.bham.ac.uk) + School of Computer Science + University of Birmingham + Edgbaston + Birmingham + B15 2TT ENGLAND - diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index c44ecc23..ce65f7c7 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -27,8 +27,17 @@ package prism; import java.io.*; +import java.util.*; + +import mtbdd.PrismMTBDD; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; +import odd.*; import parser.ast.*; +import prism.*; /** * Example class demonstrating how to control PRISM programmatically, @@ -41,6 +50,7 @@ public class PrismTest { public static void main(String args[]) { + new PrismTest().go(args); } @@ -49,9 +59,6 @@ public class PrismTest try { PrismLog mainLog; Prism prism; - ModulesFile modulesFile; - PropertiesFile propertiesFile; - Result result; // Init mainLog = new PrismFileLog("stdout"); @@ -60,28 +67,19 @@ public class PrismTest // Parse/load model 1 // NB: no need to build explicitly - it will be done if/when neeed - modulesFile = prism.parseModelFile(new File(args[0])); - prism.loadPRISMModel(modulesFile); - - // Parse a prop, check on model 1 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); - System.out.println(result.getResult()); + ModulesFile modulesFile = prism.parseModelFile(new File(args[0])); + modulesFile.setModelType(ModelType.DTMC); + prism.buildModel(modulesFile); + ProbModel dtmc = (ProbModel) prism.getBuiltModel(); + PropertiesFile pf = prism.parsePropertiesString(modulesFile, "\"target\""); + dtmc.setReach(JDD.Constant(1)); + ProbModelChecker mc = new ProbModelChecker(prism, dtmc, pf); + JDDNode target = mc.checkExpressionDD(pf.getProperty(0)); + JDD.ExportDDToDotFile(target, "target.dot"); + - // Parse another prop, check on model 1 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); - System.out.println(result.getResult()); - - // Parse/load model 2 - modulesFile = prism.parseModelFile(new File(args[1])); - prism.loadPRISMModel(modulesFile); - - // Parse a prop, check on model 2 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); - System.out.println(result.getResult()); + // Close down prism.closeDown(); } @@ -95,3 +93,4 @@ public class PrismTest } } } +//---------------------------------------------------------------------------- \ No newline at end of file diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index a80305f9..5aef2797 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -71,6 +71,30 @@ public class StateListMTBDD implements StateList // constructor + public StateListMTBDD(JDDNode s, JDDVars _vars, ODDNode _odd, VarList _varList) + { + int i; + + // store states vector mtbdd + states = s; + + // get info from model + vars = _vars; + numVars = vars.n(); + odd = _odd; + varList = _varList; + + // count number of states in list + size = JDD.GetNumMinterms(states, numVars); + + // initialise arrays + varSizes = new int[varList.getNumVars()]; + for (i = 0; i < varList.getNumVars(); i++) { + varSizes[i] = varList.getRangeLogTwo(i); + } + varValues = new int[varList.getNumVars()]; + } + public StateListMTBDD(JDDNode s, Model model) { int i; diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 55227ef9..fb9d6637 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -323,7 +323,14 @@ public class Updater if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) { throw new PrismLangException("Probabilities sum to " + sum + " in state " + state.toString(modulesFile), ups); } - + // Check if empty (e.g. due to all 0 probs/rates) + // Currently, PRISM treats this as an error + if (ch.size() == 0) { + String msg = modelType.probabilityOrRate(); + msg += (ups.getNumUpdates() > 1) ? " values sum to " : " is "; + msg += "zero for update in state " + state.toString(modulesFile); + throw new PrismLangException(msg, ups); + } return ch; }