From ddb279d4e01b925cb8f6dbc5d33bf9b0f7e7d1d1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 30 Jun 2010 09:23:55 +0000 Subject: [PATCH] Removed accidental parts of last commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1959 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 4 ---- prism/src/simulator/PathFull.java | 25 -------------------- prism/src/simulator/SimulatorEngine.java | 29 ++++++------------------ 3 files changed, 7 insertions(+), 51 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 09656f52..ec5508c6 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -393,10 +393,6 @@ public class PrismCL // store result of model checking try { results[j].setResult(definedMFConstants, definedPFConstants, res.getResult()); - if (res.getCounterexample() != null) { - mainLog.println("\nCounterexample/witness:"); - mainLog.println(res.getCounterexample()); - } } catch (PrismException e) { error("Problem storing results"); } diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index 1fe3359f..33452056 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -160,31 +160,6 @@ public class PathFull extends Path size = step; } - /** - * Remove the prefix of the current path up to the given path step. - * Index step should be >=0 and <= the total path size. - * @param step The step before which state will be removed. - */ - public void removePrecedingStates(int step) - { - int i, n, n2; - - // Ignore trivial case - if (step == 0) - return; - // Move later steps of path 'step' places forward - n = steps.size() - step; - for (i = 0; i < n; i++) { - steps.set(i, steps.get(i + step)); - } - // Remove final steps - n2 = steps.size(); - for (i = n + 1; i < n2; i++) - steps.remove(i); - // Update size too - size = steps.size() - 1; - } - // ACCESSORS (for Path) @Override diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 92242edc..8ca9d724 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -505,31 +505,16 @@ public class SimulatorEngine } /** - * Remove the prefix of the current path up to the given path step. - * Index step should be >=0 and <= the total path size. - * (Not applicable for on-the-fly paths) - * @param step The step before which state will be removed. + * This function removes states of the path that precede those of the given index + * + * @param step + * the index before which the states should be removed. + * @throws PrismException + * if anything goes wrong with the state removal. */ public void removePrecedingStates(int step) throws PrismException { - // Check step is valid - if (step < 0) { - throw new PrismException("Cannot remove states before a negative step index"); - } - if (step > path.size()) { - throw new PrismException("There is no step " + step + " in the path"); - } - // Modify path - ((PathFull) path).removePrecedingStates(step); - // Update previous state info (if required) - // (no need to update curren state info) - if (path.size() == 1) - previousState.clear(); - // Recompute samplers for any loaded properties - recomputeSamplers(); - // Generate updates for new current state - // TODO: NEED TO DO THIS? - updater.calculateTransitions(currentState, transitionList); + //doRemovePrecedingStates(step); } /**