From f6d794c22c440d843bb17c337f5ba1cf07c2ccfc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 8 May 2012 14:31:32 +0000 Subject: [PATCH] Reverse previous commit git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5160 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/README.txt | 44 +++++++++++++++++----------- prism/src/prism/PrismTest.java | 45 +++++++++++++++-------------- prism/src/prism/StateListMTBDD.java | 24 --------------- prism/src/simulator/Updater.java | 9 +----- 4 files changed, 51 insertions(+), 71 deletions(-) diff --git a/prism/README.txt b/prism/README.txt index 85c03367..8113f52c 100644 --- a/prism/README.txt +++ b/prism/README.txt @@ -36,6 +36,7 @@ For source code distributions: If you have problems check the manual, especially the section "Common Problems And Questions". + ------------- DOCUMENTATION ------------- @@ -53,6 +54,7 @@ For other PRISM-related information, see the website: http://www.prismmodelchecker.org/ + --------- LICENSING --------- @@ -69,36 +71,42 @@ library, see: http://vlsi.colorado.edu/~fabio/CUDD/ + ---------------- ACKNOWLEDGEMENTS ---------------- -PRISM was created and is still actively maintained by: +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. - * Dave Parker (University of Birmingham) - * Gethin Norman (University of Glasgow) - * Marta Kwiatkowska (University of Oxford) +The core team working on PRISM currently comprises: -We gratefully acknowledge contributions to the PRISM code-base from various sources, -including (in approximately reverse chronological order): + * Dave Parker (Oxford) + * Gethin Norman (Glasgow) + * Marta Kwiatkowska (Oxford) + +Many others have contributed to PRISM. 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): LTL model checking for MDPs - * Gethin Norman: Precomputation algorithms, abstraction + * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM * 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 ------- @@ -110,10 +118,12 @@ 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 - (d.a.parker@cs.bham.ac.uk) - School of Computer Science - University of Birmingham - Edgbaston - Birmingham - B15 2TT + (david.parker@cs.ox.ac.uk) + Department of Computer Science + University of Oxford + Wolfson Building + Parks Road + Oxford + OX1 3QD ENGLAND + diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index ce65f7c7..c44ecc23 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -27,17 +27,8 @@ 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, @@ -50,7 +41,6 @@ public class PrismTest { public static void main(String args[]) { - new PrismTest().go(args); } @@ -59,6 +49,9 @@ public class PrismTest try { PrismLog mainLog; Prism prism; + ModulesFile modulesFile; + PropertiesFile propertiesFile; + Result result; // Init mainLog = new PrismFileLog("stdout"); @@ -67,19 +60,28 @@ public class PrismTest // Parse/load model 1 // NB: no need to build explicitly - it will be done if/when neeed - 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"); - + 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()); + + // 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(); } @@ -93,4 +95,3 @@ public class PrismTest } } } -//---------------------------------------------------------------------------- \ No newline at end of file diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index 5aef2797..a80305f9 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -71,30 +71,6 @@ 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 fb9d6637..55227ef9 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -323,14 +323,7 @@ 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; }