Reverse previous commit

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

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
+

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

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;

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