From 48a2e4bcc8d84ac0472c250759cd72ec35153ef2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 16:56:34 +0000 Subject: [PATCH] Undo last commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2151 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES-PTAS | 2 - prism/src/explicit/ConstructModel.java | 69 ++------------------------ prism/src/explicit/IndexedSet.java | 8 --- prism/src/sparse/PS_NondetUntil.cc | 2 +- 4 files changed, 6 insertions(+), 75 deletions(-) diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS index 4a583bcd..6b0d94f6 100644 --- a/prism/NOTES-PTAS +++ b/prism/NOTES-PTAS @@ -4,8 +4,6 @@ TODO (before any release) * GUI -* Tidy prism-examples/pta, incl. delete brp - * Clarify semantic/type checks (consistency with games/digital) * Check guards/invariants for convexity (for now, neither can be non-convex, see below) diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 681619eb..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++; - }*/ - } - - //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"); }