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

@@ -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");
 						}

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<LocZone> X;
+		IndexedSet<LocZone> 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<LocZone>();
+		X = new LinkedList<LocZone>();
+		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<Integer>();
+		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;

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
 	 */

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);

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

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);
 	}
 
 	/**