Removed extra accidental bits of last commit.

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

prism/CHANGELOG.txt

@@ -10,7 +10,7 @@ Ongoing changes:
 * New simulator
 * Adversary generation
 * Access to action labels. inclusion in export, etc.
-* Filters and property semantics changes/additions
+* Filters and propert semantics changes/additions
 
 Latest changes (reverse chronological):
 [correct wrt svn rev 1610]

prism/NOTES

@@ -1,6 +1,6 @@
 
 Last stable version of PRISM on svn (3.3 plus some fixes) is rev 1405
-(there is a copy of this, e.g. to get working old simulator, in ~/prism-old)
+(there is a copy of this, e.g. to get working simulator, in ~/prism-old)
 
 -----------------------------------------------------------------------
 
@@ -62,13 +62,6 @@ Other notes/ideas:
 -----------------------------------------------------------------------
 
 LTL...
-
-bug:
-
-prism ~/prism-examples/dice/dice.pm \
--pctl '(s=0|s=1)=>P>=1 [ (P>=0.9 [ F<=1 s=3 ])=>(P>=0.5 [ F<=2 s=4 ]) ]'
-time-bounds should be ok in inner pctl but are not
-
 bscc stuff
 - regression testing on ltl stuff with 3 diff options
 

prism/README.txt

@@ -91,7 +91,7 @@ Contributions to the development of PRISM have also been gratefully received fro
  * Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm
  * Alistair John Strachan: Port to 64-bit architectures
  * Stephen Gilmore: Support for the stochastic process algebra PEPA
- * Paolo Ballarini & Kenneth Chan: Port to Mac OS X
+ * Paolo Ballarini & Kenneth Chan: Port of PRISM to Mac OS X
  * Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms
  * Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM
  * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM

prism/src/explicit/CTMCSimple.java

@@ -26,13 +26,7 @@
 
 package explicit;
 
-import java.io.FileWriter;
-import java.io.IOException;
 import java.util.Map;
-import java.util.TreeMap;
-
-import prism.PrismException;
-import prism.PrismUtils;
 
 /**
  * Simple explicit-state representation of a CTMC.
@@ -76,40 +70,6 @@ public class CTMCSimple extends DTMCSimple implements CTMC
 		super(ctmc, permut);
 	}
 
-	// Accessors (for ModelSimple, overriding DTMCSimple)
-	
-	//@Override
-	public void exportToPrismLanguage(String filename) throws PrismException
-	{
-		int i;
-		FileWriter out;
-		TreeMap<Integer, Double> sorted;
-		try {
-			// Output transitions to .tra file
-			out = new FileWriter(filename);
-			out.write(getModelType().keyword() + "\n");
-			out.write("module M\nx : [0.." + (numStates-1) + "];\n");
-			sorted = new TreeMap<Integer, Double>();
-			for (i = 0; i < numStates; i++) {
-				// Extract transitions and sort by destination state index (to match PRISM-exported files)
-				for (Map.Entry<Integer, Double> e : trans.get(i)) {
-					sorted.put(e.getKey(), e.getValue());
-				}
-				// Print out (sorted) transitions
-				for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
-					// Note use of PrismUtils.formatDouble to match PRISM-exported files
-					out.write("[]x=" + i + "->" + PrismUtils.formatDouble(e.getValue()));
-					out.write(":(x'=" + e.getKey() + ");\n");
-				}
-				sorted.clear();
-			}
-			out.write("endmodule\n");
-			out.close();
-		} catch (IOException e) {
-			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
-		}
-	}
-
 	// Accessors (for CTMC)
 	
 	@Override

prism/src/explicit/ConstructModel.java

@@ -57,10 +57,10 @@ public class ConstructModel
 		modelType = modulesFile.getModelType();
 		this.initialState = initialState;
 
+		int i, j, nc, nt, src, dest;
 		IndexedSet<State> states;
 		LinkedList<State> explore;
 		State state, stateNew;
-		LabelList ll;
 
 		ModelSimple model = null;
 		DTMCSimple dtmc = null;
@@ -68,26 +68,8 @@ public class ConstructModel
 		MDPSimple mdp = null;
 		Distribution distr = null;
 
-		int i, j, k, nc, nt, nl, src, dest;
-		boolean progressDisplayed;
-		long timer, timerProgress;
-
-		// Starting reachability...
-		mainLog.println("\nExploring reachable state space...");
-		timer = timerProgress = System.currentTimeMillis();
-		progressDisplayed = false;
-
 		// Initialise simulator for this model
 		engine.createNewOnTheFlyPath(modulesFile);
-		
-		// Go through labels: create Bitsets and add to simulator
-		ll = modulesFile.getLabelList();
-		nl = ll.size();
-		ArrayList<BitSet> labels = new ArrayList<BitSet>(nl);
-		for (i = 0; i < nl; i++) {
-			engine.addLabel(ll.getLabel(i));
-			labels.add(new BitSet());
-		}
 
 		// Create a (simple, mutable) model of the appropriate type
 		switch (modelType) {
@@ -120,12 +102,6 @@ public class ConstructModel
 			// Use simulator to explore all choices/transitions from this state
 			engine.initialisePath(state);
 			nc = engine.getNumChoices();
-			// TODO: remove this deadlock check (nc=0) hack
-			for (k = 0; k < nl; k++) {
-				if (nc == 0 && engine.queryLabel(k)) {
-					labels.get(k).set(src);
-				}
-			}
 			for (i = 0; i < nc; i++) {
 				if (modelType == ModelType.MDP) {
 					distr = new Distribution();
@@ -159,32 +135,14 @@ public class ConstructModel
 					mdp.addChoice(src, distr);
 				}
 			}
-			// Print some progress info occasionally
-			if (System.currentTimeMillis() - timerProgress > 3000) {
-				if (!progressDisplayed) {
-					mainLog.print("Number of states so far:");
-					progressDisplayed = true;
-				}
-				mainLog.print(" " + (src + 1));
-				mainLog.flush();
-				timerProgress = System.currentTimeMillis();
-			}
 		}
 
-		// Tidy up progress display
-		if (progressDisplayed)
-			mainLog.println(" " + (src + 1));
-
-		// Reachability complete
-		mainLog.println("State exploration done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs.");
-		mainLog.println("States: " + (src + 1));
-
 		//graph.states = states.toArrayList();
 
 		int permut[] = states.buildSortingPermutation();
-		//mainLog.println(permut);
+		mainLog.println(permut);
 
-		//mainLog.println("Model: " + model);
+		mainLog.println("Model: " + model);
 
 		switch (modelType) {
 		case DTMC:
@@ -198,31 +156,14 @@ public class ConstructModel
 			break;
 		}
 
-		//mainLog.println(states.size() + " states: " + states);
-		//mainLog.println("Model: " + model);
+		mainLog.println(states.size() + " states: " + states);
+		mainLog.println("Model: " + model);
 
 		BitSet deadlocks = model.findDeadlocks(true);
 		if (deadlocks.cardinality() > 0) {
 			mainLog.println("Adding self-loops in " + deadlocks.cardinality() + " states...");
 		}
 
-		// Model construction complete
-		timer = System.currentTimeMillis() - timer;
-		mainLog.println("Model construction done in " + (timer / 1000.0) + " secs.");
-		
-		// TODO: clean me up
-		for (i = 0; i < nl; i++) {
-			mainLog.println(labels.get(i));
-			/*ll.getLabel(i);
-			j = 0;
-			for (Map.Entry<State, Integer> e : states.getEntrySet()) {
-				mainLog.println(j + ":" + permut[j] + ":" + e.getValue() + " - ");
-				j++;
-			}*/
-		}
-		
-		((CTMCSimple)model).exportToPrismLanguage("ctmc.sm");
-		
 		return model;
 	}
 

prism/src/explicit/IndexedSet.java

@@ -84,14 +84,6 @@ public class IndexedSet<T>
 		return set.size();
 	}
 
-	/**
-	 * Get access to the underlying set of map entries. 
-	 */
-	public Set<Map.Entry<T, Integer>> getEntrySet()
-	{
-		return set.entrySet();
-	}
-	
 	/**
 	 * Create an ArrayList of the states, ordered by index.
 	 */

prism/src/sparse/PS_NondetUntil.cc

@@ -319,7 +319,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				// But only output a choice if it is in the adversary
 				if (j == adv[i]) {
 					for (k = l2; k < h2; k++) {
-						fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]);
+						fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
 						if (actions != NULL) fprintf(fp_adv, " %s", actions[j]>0?action_names[actions[j]-1]:"");
 						fprintf(fp_adv, "\n");
 					}