Update README with new contact/people details.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5159 bbc10eb1-c90d-0410-af57-cb519fbb1720

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
-

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
 		}
 	}
 }
+//----------------------------------------------------------------------------

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;

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;
 	}