diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index eac041e1..7c4c9bbe 100644 --- a/prism/CHANGELOG.txt +++ b/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] diff --git a/prism/NOTES b/prism/NOTES index bcade9a5..6c1371db 100644 --- a/prism/NOTES +++ b/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 diff --git a/prism/README.txt b/prism/README.txt index fa0fb4c7..a74cd3c2 100644 --- a/prism/README.txt +++ b/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 diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java index 8c414da1..d08afef9 100644 --- a/prism/src/explicit/CTMCSimple.java +++ b/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 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(); - for (i = 0; i < numStates; i++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : trans.get(i)) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - for (Map.Entry 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 diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index a5454df4..ebfba5e3 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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 states; LinkedList 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 labels = new ArrayList(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 e : states.getEntrySet()) { - mainLog.println(j + ":" + permut[j] + ":" + e.getValue() + " - "); - j++; - }*/ - } - - ((CTMCSimple)model).exportToPrismLanguage("ctmc.sm"); - return model; } diff --git a/prism/src/explicit/IndexedSet.java b/prism/src/explicit/IndexedSet.java index 5a67c1b4..e23530d0 100644 --- a/prism/src/explicit/IndexedSet.java +++ b/prism/src/explicit/IndexedSet.java @@ -84,14 +84,6 @@ public class IndexedSet return set.size(); } - /** - * Get access to the underlying set of map entries. - */ - public Set> getEntrySet() - { - return set.entrySet(); - } - /** * Create an ArrayList of the states, ordered by index. */ diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index 091ba1e6..1c1b0576 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/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"); }