From 915edf43ba0c078a724085f061f92fa8d45cb027 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 30 Jun 2010 09:19:12 +0000 Subject: [PATCH] Option (current enabled) to use FORMATS10 style forwards reach, plus a few zone API tweaks. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1958 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 4 + prism/src/pta/ForwardsReach.java | 148 +++++++++++++++++++++++ prism/src/pta/LocZone.java | 41 ++++--- prism/src/pta/PTAExpected.java | 2 +- prism/src/simulator/PathFull.java | 25 ++++ prism/src/simulator/SimulatorEngine.java | 29 +++-- 6 files changed, 225 insertions(+), 24 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index ec5508c6..09656f52 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -393,6 +393,10 @@ 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/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index 394a7d43..e48506d4 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -76,6 +76,154 @@ public class ForwardsReach */ public ReachabilityGraph buildForwardsGraph(PTA pta, BitSet targetLocs, Constraint targetConstraint) throws PrismException + { + boolean formats10 = true; + + if (formats10) + return buildForwardsGraphFormats10(pta, targetLocs, targetConstraint); + else + return buildForwardsGraphFormats09(pta, targetLocs, targetConstraint); + } + + /** + * Implementation of {@link #buildForwardsGraph} using FORMATS'10 definition. + */ + private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs, Constraint targetConstraint) + throws PrismException + { + Zone z; + LocZone init, lz, lz2; + LinkedList X; + IndexedSet Yset; + //LocZoneSetOld Zset; + ReachabilityGraph graph; + int src, dest, count; + long timer, timerProgress; + boolean progressDisplayed; + + // Store target info + this.targetLocs = targetLocs; + this.targetConstraint = targetConstraint; + + // Starting reachability... + mainLog.println("\nBuilding forwards reachability graph..."); + timer = timerProgress = System.currentTimeMillis(); + progressDisplayed = false; + + // Re-compute max clock constraint value if required + if (targetConstraint != null) + pta.recomputeMaxClockConstraint(targetConstraint); + + // Initialise data structures + graph = new ReachabilityGraph(pta); + Yset = new IndexedSet(); + X = new LinkedList(); + target = new BitSet(); + + // Build initial symbolic state (NB: assume initial location = 0) + z = DBM.createZero(pta); + init = new LocZone(0, z); + + // Reachability loop + Yset.add(init); + X.add(init); + src = -1; + // While there are unexplored symbolic states (in X)... + while (!X.isEmpty()) { + // Pick next state to explore + // X is a list containing states in order found + // (so we know index of lz is src+1) + lz = X.removeFirst(); + src++; + // Compute timed post for this zone (NB: do this before checking if target) + lz = lz.deepCopy(); + lz.tPost(pta); + // Is this a target state? + if (targetLocs.get(lz.loc) && (targetConstraint == null || lz.zone.isSatisfied(targetConstraint))) { + target.set(src); + // Add null for this state (no need to store info) + graph.addState(); + continue; + } + // Otherwise, explore this symbolic state + // First, check there is at least one transition + // (don't want deadlocks in non-target states) + if (pta.getTransitions(lz.loc).size() == 0) { + throw new PrismException("PTA deadlocks in location \"" + pta.getLocationNameString(lz.loc) + "\""); + } + // Add current state to reachability graph + graph.addState(); + // For each outgoing transition... + for (Transition transition : pta.getTransitions(lz.loc)) { + int[] dests = new int[transition.getNumEdges()]; + boolean enabled = false; + boolean unenabled = false; + count = 0; + for (Edge edge : transition.getEdges()) { + // Do "discrete post" for this edge + lz2 = lz.deepCopy(); + lz2.dPost(edge); + // If non-empty, create edge, also adding state to X if new + if (!lz2.zone.isEmpty()) { + if (Yset.add(lz2)) { + X.add(lz2); + } + dest = Yset.getIndexOfLastAdd(); + enabled = true; + dests[count] = dest; + } else { + unenabled = true; + dests[count] = -1; + } + count++; + } + if (enabled) { + if (unenabled) + throw new PrismException("Badly formed PTA: state " + src); + graph.addTransition(src, transition, dests, null); + } + } + // Print some progress info occasionally + if (System.currentTimeMillis() - timerProgress > 3000) { + if (!progressDisplayed) { + mainLog.print("Number of states so far:"); + progressDisplayed = true; + } + mainLog.print(" " + Yset.size()); + mainLog.flush(); + timerProgress = System.currentTimeMillis(); + } + } + + // Tidy up progress display + if (progressDisplayed) + mainLog.println(" " + Yset.size()); + + // Convert state set to ArrayList and store + graph.states = Yset.toArrayList(); + + // Always have a single initial state 0 after this construction + initialStates = new ArrayList(); + initialStates.add(0); + + // Reachability complete + timer = System.currentTimeMillis() - timer; + mainLog.println("Graph constructed in " + (timer / 1000.0) + " secs."); + mainLog.print("Graph: " + graph.states.size() + " symbolic states"); + mainLog.println("), " + target.cardinality() + " target states"); + + // Print a warning if there are no target states + if (target.cardinality() == 0) + mainLog.println("Warning: There are no target states."); + + return graph; + } + + /** + * Implementation of {@link #buildForwardsGraph} using FORMATS'09 definition. + */ + private ReachabilityGraph buildForwardsGraphFormats09(PTA pta, BitSet targetLocs, Constraint targetConstraint) + throws PrismException { Zone z; LocZone init, lz, lz2; diff --git a/prism/src/pta/LocZone.java b/prism/src/pta/LocZone.java index eb51f2be..66e376a0 100644 --- a/prism/src/pta/LocZone.java +++ b/prism/src/pta/LocZone.java @@ -40,9 +40,32 @@ public class LocZone } /** - * dSuc: discrete successor + * Do combined discrete *then* time post operation wrt. an edge. + * Note: time part includes c-closure. */ - public void dSuc(Edge edge) + public void post(Edge edge) + { + PTA pta = edge.getParent().getParent(); + dPost(edge); + tPost(pta); + } + + /** + * Do time part of post operation (including c-closure). + * Note: pta is passed in just for efficiency, could find it if we wanted. + */ + public void tPost(PTA pta) + { + // Time successor (up) + zone.up(pta.getInvariantConstraints(loc)); + // c-Closure + zone.cClosure(pta.getMaxClockConstraint()); + } + + /** + * Do discrete part of post operation (wrt. an edge). + */ + public void dPost(Edge edge) { Transition tr = edge.getParent(); // Intersect this zone with guard of edge's transition's guard @@ -59,20 +82,6 @@ public class LocZone loc = edge.getDestination(); } - /** - * post: combined discrete/time successors + c-closure - */ - public void post(Edge edge) - { - PTA pta = edge.getParent().getParent(); - // Discrete successor - dSuc(edge); - // Time successor (up) - zone.up(pta.getInvariantConstraints(loc)); - // c-Closure - zone.cClosure(pta.getMaxClockConstraint()); - } - /** * dPre: discrete predecessor */ diff --git a/prism/src/pta/PTAExpected.java b/prism/src/pta/PTAExpected.java index 6871dbed..6e1e50b4 100644 --- a/prism/src/pta/PTAExpected.java +++ b/prism/src/pta/PTAExpected.java @@ -369,7 +369,7 @@ public class PTAExpected if (lzRew > 10000) throw new PrismException("stop"); LocZone lz2 = lz.deepCopy(); - lz2.dSuc(edge); + lz2.dPost(edge); mainLog.println("post: " + lz2); rew = getMinMaxForZone(lz2.zone, someClock, min); mainLog.println(rew); diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index 33452056..1fe3359f 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -160,6 +160,31 @@ 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 8ca9d724..92242edc 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -505,16 +505,31 @@ public class SimulatorEngine } /** - * 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. + * 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. */ public void removePrecedingStates(int step) throws PrismException { - //doRemovePrecedingStates(step); + // 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); } /**